Exact mean and high forcing sums. Periodic BA/BC terms are absent from the mean force, and the angle-constant BB term is absent from the high force. Every summand is the genuine continuous cylinder L² path already constructed.

theorem EulerPacketCylinderField.angleMean_congr_at (P : ℝ) (f g : EulerPacketProfileRecursion.VectorField) (t : ℝ) (x : EulerSmoothLimit.Space) (h : ∀ (θ : ℝ), f (t, x, θ) = g (t, x, θ)) (θ : ℝ) : EulerPacketProfileRecursion.angleMean P f (t, x, θ) = EulerPacketProfileRecursion.angleMean P g (t, x, θ)

theorem EulerPacketCylinderField.angleMean_neg_finsetSum {P T : ℝ} [Fact (0 < P)] {ι : Type u_1} (s : Finset ι) (raw : ι → EulerPacketProfileRecursion.VectorField) (G : (i : ι) → Field P T (raw i)) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : EulerPacketProfileRecursion.angleMean P (fun (z : EulerPacketPointJets.Domain) => -∑ i ∈ s, raw i z) (↑t, x, θ) = -∑ i ∈ s, EulerPacketProfileRecursion.angleMean P (raw i) (↑t, x, θ)

theorem EulerPacketCylinderField.PrefixFields.knownForce_decomposition {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {p : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} (F : PrefixFields P T p a) (hp : 2 ≤ p) (hc : (a 0).corrector = 0) (hB₁ : (a 1).mean = 0) (hA : ∀ i < p, ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), inner ℝ (O.normal (↑t, x, θ)) ((a i).high (↑t, x, θ)) = 0) (hB : ∀ i < p, ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), (a i).mean (↑t, x, θ) = (a i).mean (↑t, x, 0)) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : EulerPacketProfileRecursion.knownForce O p a (↑t, x, θ) = -∑ q ∈ knownTermIndices p, q.1.raw O p a q.2.1 q.2.2 (↑t, x, θ)

theorem EulerPacketCylinderField.PrefixFields.meanForce_decomposition {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {p : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} (F : PrefixFields P T p a) (C : CoefficientData P T O) (hp : 2 ≤ p) (hT : 0 < T) {correctorT : EulerPacketProfileRecursion.VectorField} (Ct : Field P T correctorT) (hCt : TimeDerivative ⋯ (F.corrector (p - 1) ⋯) Ct) (pressure : Field P T (pressureGradient (a (p - 1)).highPressure)) (hc : (a 0).corrector = 0) (hB₁ : (a 1).mean = 0) (hA : ∀ i < p, ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), inner ℝ (O.normal (↑t, x, θ)) ((a i).high (↑t, x, θ)) = 0) (hB : ∀ i < p, ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), (a i).mean (↑t, x, θ) = (a i).mean (↑t, x, 0)) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : EulerPacketProfileRecursion.meanForce O p a (↑t, x, θ) = -∑ q ∈ knownTermIndices p, q.1.meanRaw O p a q.2.1 q.2.2 (↑t, x, θ)

theorem EulerPacketCylinderField.PrefixFields.highForce_decomposition {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {p : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} (F : PrefixFields P T p a) (C : CoefficientData P T O) (hp : 2 ≤ p) (hT : 0 < T) {correctorT : EulerPacketProfileRecursion.VectorField} (Ct : Field P T correctorT) (hCt : TimeDerivative ⋯ (F.corrector (p - 1) ⋯) Ct) (pressure : Field P T (pressureGradient (a (p - 1)).highPressure)) (hc : (a 0).corrector = 0) (hB₁ : (a 1).mean = 0) (hA : ∀ i < p, ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), inner ℝ (O.normal (↑t, x, θ)) ((a i).high (↑t, x, θ)) = 0) (hB : ∀ i < p, ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), (a i).mean (↑t, x, θ) = (a i).mean (↑t, x, 0)) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : EulerPacketProfileRecursion.highForce O p a (↑t, x, θ) = -∑ q ∈ knownTermIndices p, q.1.highRaw O p a q.2.1 q.2.2 (↑t, x, θ) - ((EulerPacketPointJets.fastAdvection (O.normal (↑t, x, θ))) (EulerPacketPointJets.slicedJet O.interval (EulerPacketProfileRecursion.meanResult O p a).1 (↑t, x, θ))) (EulerPacketPointJets.slicedJet O.interval (a 1).high (↑t, x, θ))

theorem EulerPacketCylinderField.PrefixFields.knownForce_term_path {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {p : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} (F : PrefixFields P T p a) (C : CoefficientData P T O) (hp : 2 ≤ p) (hT : 0 < T) {correctorT : EulerPacketProfileRecursion.VectorField} (Ct : Field P T correctorT) (hCt : TimeDerivative ⋯ (F.corrector (p - 1) ⋯) Ct) (pressure : Field P T (pressureGradient (a (p - 1)).highPressure)) (hc : (a 0).corrector = 0) (hB₁ : (a 1).mean = 0) (hA : ∀ i < p, ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), inner ℝ (O.normal (↑t, x, θ)) ((a i).high (↑t, x, θ)) = 0) (hB : ∀ i < p, ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), (a i).mean (↑t, x, θ) = (a i).mean (↑t, x, 0)) : (F.knownForce C ⋯ hT Ct hCt pressure).path = -∑ q ∈ knownTermIndices p, (F.termField C ⋯ hT Ct hCt pressure q.1 q.2.1 q.2.2).path

theorem EulerPacketCylinderField.PrefixFields.meanForce_term_path {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {p : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} (F : PrefixFields P T p a) (C : CoefficientData P T O) (hp : 2 ≤ p) (hT : 0 < T) {correctorT : EulerPacketProfileRecursion.VectorField} (Ct : Field P T correctorT) (hCt : TimeDerivative ⋯ (F.corrector (p - 1) ⋯) Ct) (pressure : Field P T (pressureGradient (a (p - 1)).highPressure)) (hc : (a 0).corrector = 0) (hB₁ : (a 1).mean = 0) (hA : ∀ i < p, ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), inner ℝ (O.normal (↑t, x, θ)) ((a i).high (↑t, x, θ)) = 0) (hB : ∀ i < p, ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), (a i).mean (↑t, x, θ) = (a i).mean (↑t, x, 0)) : (F.meanForce C ⋯ hT Ct hCt pressure).path = -∑ q ∈ knownTermIndices p, (F.meanTermField C ⋯ hT Ct hCt pressure q.1 q.2.1 q.2.2).path

theorem EulerPacketCylinderField.PrefixFields.highForce_term_path {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {p : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} (F : PrefixFields P T p a) (C : CoefficientData P T O) (hp : 2 ≤ p) (hT : 0 < T) {correctorT : EulerPacketProfileRecursion.VectorField} (Ct : Field P T correctorT) (hCt : TimeDerivative ⋯ (F.corrector (p - 1) ⋯) Ct) (pressure : Field P T (pressureGradient (a (p - 1)).highPressure)) (hc : (a 0).corrector = 0) (hB₁ : (a 1).mean = 0) (hA : ∀ i < p, ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), inner ℝ (O.normal (↑t, x, θ)) ((a i).high (↑t, x, θ)) = 0) (hB : ∀ i < p, ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), (a i).mean (↑t, x, θ) = (a i).mean (↑t, x, 0)) (newMean : Field P T (EulerPacketProfileRecursion.meanResult O p a).1) : (F.highForce C hp hT Ct hCt pressure newMean).path = -∑ q ∈ knownTermIndices p, (F.highTermField C ⋯ hT Ct hCt pressure q.1 q.2.1 q.2.2).path - (SpatialJetField.fastAdvection C.normal (SpatialJetField.ofField O.interval newMean) (SpatialJetField.ofField O.interval (F.high 1 ⋯))).path