Compact high profiles and angle-independent means make the exterior nonlinear forcing constant in angle.

structure EulerPacketCylinderField.PrefixLocality (T : ℝ) (p : ℕ) (a : ℕ → EulerPacketProfileRecursion.Profile) (S : Set EulerSmoothLimit.Space) : Prop

Prefix locality data, collecting high_zero, corrector_zero, mean_angle.

• high_zero (i : ℕ) : i < p → ∀ (t : ↑(Set.Icc 0 T)), ∀ x ∉ S, ∀ (θ : ℝ), (a i).high (↑t, x, θ) = 0
• corrector_zero (i : ℕ) : i < p → ∀ (t : ↑(Set.Icc 0 T)), ∀ x ∉ S, ∀ (θ : ℝ), (a i).corrector (↑t, x, θ) = 0
• mean_angle (i : ℕ) : i < p → ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), (a i).mean (↑t, x, θ) = (a i).mean (↑t, x, 0)

theorem EulerPacketCylinderField.PrefixFields.knownJet_angleIndependent {P T : ℝ} [Fact (0 < P)] {p : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} (F : PrefixFields P T p a) (O : EulerPacketProfileRecursion.Operators) (hp : 1 ≤ p) (S : Set EulerSmoothLimit.Space) (hS : IsClosed S) (L : PrefixLocality T p a S) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (hx : x ∉ S) (i : ℕ) : AngleIndependentJet fun (θ : ℝ) => EulerPacketProfileRecursion.knownJets O p a (↑t, x, θ) i

theorem EulerPacketCylinderField.AngleIndependentJet.slowAdvection {J K : ℝ → EulerPacketPointJets.VectorJet} (hJ : AngleIndependentJet J) (hK : AngleIndependentJet K) (A : ℝ → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (hA : ∀ (θ : ℝ), A θ = A 0) (θ : ℝ) : ((EulerPacketPointJets.slowAdvection (A θ)) (J θ)) (K θ) = ((EulerPacketPointJets.slowAdvection (A 0)) (J 0)) (K 0)

theorem EulerPacketCylinderField.AngleIndependentJet.fastAdvection_zero {K : ℝ → EulerPacketPointJets.VectorJet} (hK : AngleIndependentJet K) (m : EulerSmoothLimit.Space) (J : EulerPacketPointJets.VectorJet) (θ : ℝ) : ((EulerPacketPointJets.fastAdvection m) J) (K θ) = 0

theorem EulerPacketCylinderField.PrefixFields.nonlinear_angleIndependent {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {p : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} (F : PrefixFields P T p a) (C : CoefficientData P T O) (hp : 1 ≤ p) (S : Set EulerSmoothLimit.Space) (hS : IsClosed S) (L : PrefixLocality T p a S) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (hx : x ∉ S) (θ : ℝ) : EulerPacketPointJets.nonlinearGrade (p + 1) p (O.inverseFrame (↑t, x, θ)) (O.normal (↑t, x, θ)) (EulerPacketProfileRecursion.knownJets O p a (↑t, x, θ)) = EulerPacketPointJets.nonlinearGrade (p + 1) p (O.inverseFrame (↑t, x, 0)) (O.normal (↑t, x, 0)) (EulerPacketProfileRecursion.knownJets O p a (↑t, x, 0))