The source deformation symmetries imply the literal parity of the correction coefficients, including the odd differentiated quadratic term.

theorem EulerPacketCorrectionCoefficients.fderiv_neg_of_even {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E → F) (hf : ContDiff ℝ (↑⊤) f) (he : ∀ (x : E), f (-x) = f x) (x : E) : fderiv ℝ f (-x) = -fderiv ℝ f x

theorem EulerPacketCorrectionCoefficients.frameTime_even {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.F.field t) (-x) = (D.F.field t) x) (hM : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.M.field t) (-x) = (D.M.field t) x) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : (D.F₁.field t) (-x) = (D.F₁.field t) x

theorem EulerPacketCorrectionCoefficients.metricTower_even {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.F.field t) (-x) = (D.F.field t) x) (P : ℝ) [Fact (0 < P)] (t : ↑(Set.Icc 0 D.T)) (x : EulerLiftedGradientSpace.LiftDomain P) : ((metricTower D P).coefficient t).coefficient (-x) = ((metricTower D P).coefficient t).coefficient x

theorem EulerPacketCorrectionCoefficients.linearTower_even {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.F.field t) (-x) = (D.F.field t) x) (hM : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.M.field t) (-x) = (D.M.field t) x) (P : ℝ) [Fact (0 < P)] (t : ↑(Set.Icc 0 D.T)) (x : EulerLiftedGradientSpace.LiftDomain P) : ((linearTower D P).coefficient t).coefficient (-x) = ((linearTower D P).coefficient t).coefficient x

theorem EulerPacketCorrectionCoefficients.quadraticTower_odd {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.F.field t) (-x) = (D.F.field t) x) (P : ℝ) [Fact (0 < P)] (κ : ℝ) (t : ↑(Set.Icc 0 D.T)) (i : Fin 3) (x : EulerLiftedGradientSpace.LiftDomain P) : ((quadraticTower D P κ i).coefficient t).coefficient (-x) = -((quadraticTower D P κ i).coefficient t).coefficient x

theorem EulerPacketCorrectionCoefficients.correctionParityData {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.F.field t) (-x) = (D.F.field t) x) (hM : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.M.field t) (-x) = (D.M.field t) x) (P : ℝ) [Fact (0 < P)] (κ : ℝ) (hκ : |κ| ≤ 1) {z r : EulerPacketProfileRecursion.VectorField} (Z : EulerPacketCylinderField.Field P D.T z) (G : EulerPacketCylinderField.Field P D.T r) (hZ : EulerPacketCylinderField.JointOdd D.T z) (hG : EulerPacketCylinderField.JointOdd D.T r) : EulerCorrectionAssembly.ParityData P (correctionDataOfFields D P κ hκ Z G)