The actual initialized correction data have all the joint parities required by the drift-aware correction and pressure construction.

theorem EulerPacketTerminalDatum.initializedCorrectionParityData (M : EulerMeanPacketProvider.Data) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (hTime : M.T = D.T) (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (α : ℝ) (eM : EulerMeanPacketProvider.EvenData M) (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) (hDM : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.M.field t) (-x) = (D.M.field t) x) (hBH : ∀ (t : ↑(Set.Icc 0 (D.initial τ hτ ⋯).T)) (x : EulerSmoothLimit.Space), (B.H.field t) (-x) = (B.H.field t) x) (Cagree : EulerPacketCylinderField.SourceCoefficientAgreement M D) (N : ℕ) (hN : 1 ≤ N) (k : ℝ) (hk : 4 ≤ k) : EulerCorrectionAssembly.ParityData period (initializedCorrectionData M D hTime τ hτ hτT B δ hδ ξ hs α Cagree N hN k hk)