Genuine periodicity and zero-mean identities for raw cylinder-path witnesses.

theorem EulerPacketCylinderField.Field.raw_periodic {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) : Function.Periodic (fun (θ : ℝ) => raw (↑t, x, θ)) P

theorem EulerPacketCylinderField.Field.raw_angle_continuous {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) : Continuous fun (θ : ℝ) => raw (↑t, x, θ)

theorem EulerPacketCylinderField.Field.raw_angle_hasDerivAt {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : HasDerivAt (fun (s : ℝ) => raw (↑t, x, s)) ((fderiv ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => raw (↑t, y)) (x, θ)) (0, 1)) θ

theorem EulerPacketCylinderField.Field.raw_angle_derivative_continuous {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) : Continuous fun (θ : ℝ) => (fderiv ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => raw (↑t, y)) (x, θ)) (0, 1)

theorem EulerPacketCylinderField.Field.raw_angle_derivative_integral {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) : ∫ (θ : ℝ) in 0..P, (fderiv ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => raw (↑t, y)) (x, θ)) (0, 1) = 0

theorem EulerPacketCylinderField.Field.subtract_mean_integral {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) : ∫ (θ : ℝ) in 0..P, (raw - EulerPacketProfileRecursion.angleMean P raw) (↑t, x, θ) = 0

theorem EulerPacketCylinderField.mean_primary_integral_zero {P T : ℝ} [Fact (0 < P)] {rawB rawA normal : EulerPacketProfileRecursion.VectorField} (N : VectorCoefficient T normal) (A : Field P T rawA) (s : Set ℝ) (hB : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), rawB (↑t, x, θ) = rawB (↑t, x, 0)) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) : ∫ (θ : ℝ) in 0..P, ((EulerPacketPointJets.fastAdvection (normal (↑t, x, θ))) (EulerPacketPointJets.slicedJet s rawB (↑t, x, θ))) (EulerPacketPointJets.slicedJet s rawA (↑t, x, θ)) = 0

A new angle-independent mean cannot contribute angular mean to its primary interaction.