The actual homogeneous primary solution initializes the profile parity induction.

theorem EulerPacketCylinderField.ProfileParity.primary {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (I : EulerTransversePacketProvider.InitialData P D) (O : EulerPacketProfileRecursion.Operators) (hcorrector : O.curlCorrector = D.curlCorrector P) (hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ D.support ↔ x ∈ D.support) (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) (hraw : JointOdd D.T raw) (hI : (EulerCylinderFieldReflection.reflection P) ↑I.value = -↑I.value) : ProfileParity D.T (EulerPacketProfileRecursion.primaryProfile O (G.vector I) (G.scalar I))

theorem EulerPacketCylinderField.homogeneousPrimaryParity {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (I : EulerTransversePacketProvider.InitialData P D) (O : EulerPacketProfileRecursion.Operators) (hcorrector : O.curlCorrector = D.curlCorrector P) (hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ D.support ↔ x ∈ D.support) (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) (hI : (EulerCylinderFieldReflection.reflection P) ↑I.value = -↑I.value) : ProfileParity D.T (homogeneousPrimary D I O)