The literal recursive force preserves joint odd parity from its actual prefix data.

structure EulerPacketCylinderField.PrefixOdd (T : ℝ) (p : ℕ) (a : ℕ → EulerPacketProfileRecursion.Profile) : Prop

Prefix odd data, collecting high, mean, corrector.

• high (i : ℕ) : i < p → JointOdd T (a i).high
• mean (i : ℕ) : i < p → JointOdd T (a i).mean
• corrector (i : ℕ) : i < p → JointOdd T (a i).corrector

theorem EulerPacketCylinderField.JointOdd.convolution {T : ℝ} (M n : ℕ) (f : ℕ → ℕ → EulerPacketProfileRecursion.VectorField) (hf : ∀ (i j : ℕ), JointOdd T (f i j)) : JointOdd T fun (z : EulerPacketPointJets.Domain) => ∑ i ∈ Finset.range (M + 1), ∑ j ∈ Finset.range (M + 1), if i + j = n then f i j z else 0

theorem EulerPacketCylinderField.PrefixOdd.knownJet_value_odd {T : ℝ} {O : EulerPacketProfileRecursion.Operators} {p : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} (H : PrefixOdd T p a) (hp : 1 ≤ p) (i : ℕ) : JointOdd T fun (z : EulerPacketPointJets.Domain) => (EulerPacketProfileRecursion.knownJets O p a z i).1

theorem EulerPacketCylinderField.PrefixFields.nonlinear_odd {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {p : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} (F : PrefixFields P T p a) (H : PrefixOdd T p a) (hp : 1 ≤ p) (hI : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), O.inverseFrame (↑t, -x, -θ) = O.inverseFrame (↑t, x, θ)) (hN : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), O.normal (↑t, -x, -θ) = O.normal (↑t, x, θ)) : JointOdd T fun (z : EulerPacketPointJets.Domain) => EulerPacketPointJets.nonlinearGrade (p + 1) p (O.inverseFrame z) (O.normal z) (EulerPacketProfileRecursion.knownJets O p a z)

theorem EulerPacketCylinderField.PrefixFields.knownForce_odd {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {p : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} (F : PrefixFields P T p a) (H : PrefixOdd T p a) (C : CoefficientData P T O) (hp : 1 ≤ p) (hT : 0 < T) {correctorT : EulerPacketProfileRecursion.VectorField} (Ct : Field P T correctorT) (hCt : TimeDerivative ⋯ (F.corrector (p - 1) ⋯) Ct) (hpressure : JointOdd T (pressureGradient (a (p - 1)).highPressure)) (hI : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), O.inverseFrame (↑t, -x, -θ) = O.inverseFrame (↑t, x, θ)) (hM : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), O.strain (↑t, -x, -θ) = O.strain (↑t, x, θ)) (hN : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), O.normal (↑t, -x, -θ) = O.normal (↑t, x, θ)) : JointOdd T (EulerPacketProfileRecursion.knownForce O p a)