Compatibility of independently supplied actual finite-order corrections, proved from their equations.

theorem EulerCorrectionAssembly.FiniteFamily.compatible (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (F : FiniteFamily period hT A) (C : ComparisonData period hT A) (q : ℕ) (hq : 6 ≤ q) : (ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerCylinderSobolevSpace.truncateOperator period (q + 1))) (F.solution (q + 1) ⋯) = F.solution q hq

Adjacent supplied finite corrections coincide after restriction, by actual inviscid uniqueness.

theorem EulerCorrectionAssembly.FiniteFamily.value_succ (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (F : FiniteFamily period hT A) (C : ComparisonData period hT A) (q : ℕ) (hq : 6 ≤ q) (t : ↑(Set.Icc 0 T)) : EulerCylinderSobolevSpace.value period ((F.solution (q + 1) ⋯) t) = EulerCylinderSobolevSpace.value period ((F.solution q hq) t)

Adjacent actual finite corrections have the same underlying L² field.

theorem EulerCorrectionAssembly.FiniteFamily.value_base (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (F : FiniteFamily period hT A) (C : ComparisonData period hT A) (q : ℕ) (hq : 6 ≤ q) (t : ↑(Set.Icc 0 T)) : EulerCylinderSobolevSpace.value period ((F.solution q hq) t) = EulerCylinderSobolevSpace.value period ((F.solution 6 ⋯) t)

All supplied finite corrections have the same actual base L² field.

theorem EulerCorrectionAssembly.FiniteFamily.unique_at_order (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (F : FiniteFamily period hT A) (C : ComparisonData period hT A) (q : ℕ) (hq : 6 ≤ q) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (hi : u ⟨0, ⋯⟩ = 0) (hd : ∀ (t : ↑(Set.Icc 0 T)), EulerCylinderSobolevSpace.value period (u t) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period A.κ A.direction) (hu : ∀ (t : ℝ) (ht : t ∈ Set.Ioo 0 T), HasDerivAt (fun (r : ℝ) => EulerCylinderSobolevSpace.value period (EulerVolterraConvolution.extendPath T ⋯ u r)) (EulerCylinderSobolevSpace.value period ((EulerCorrectionOperators.CorrectionData.coefficients period (EulerAllOrderCorrectionData.Data.atOrder period A q) hq).apply ⟨t, ⋯⟩ (u ⟨t, ⋯⟩))) t) : u = F.solution q hq

Every other actual finite-order correction with zero trace and the same genuine PDE and divergence condition equals the supplied finite correction. No comparison estimate or compatibility is assumed.