The literal recursively constructed high forcing has zero angular mean.

theorem EulerPacketCylinderField.Field.average_zero_of_raw_integral {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (h : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), ∫ (θ : ℝ) in 0..P, raw (↑t, x, θ) = 0) (t : ↑(Set.Icc 0 T)) : (EulerCylinderAngleAverage.average P) (G.path t) = 0

theorem EulerPacketCylinderField.PrefixFields.highForce_mean_zero {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)) (newMean : Field P T (EulerPacketProfileRecursion.meanResult O p a).1) (hB : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), (EulerPacketProfileRecursion.meanResult O p a).1 (↑t, x, θ) = (EulerPacketProfileRecursion.meanResult O p a).1 (↑t, x, 0)) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) : ∫ (θ : ℝ) in 0..P, EulerPacketProfileRecursion.highForce O p a (↑t, x, θ) = 0