Actual residual cancellation for the constructed all-order correction

The drift-aware budget constructs the correction. A separate, explicit input below identifies the prescribed residual with the residual of the actual approximation and its pressure. Only after supplying that identity do we assert that the corrected field solves the zero-residual lifted equation.

These results concern the genuine Sobolev paths and coefficients of Data. They neither construct the approximate packet nor identify arbitrary coefficients with the physical Euler equation in parent-flow coordinates.

structure EulerAllOrderDriftCorrection.ApproximationResidual (period : ℝ) [Fact (0 < period)] {T : ℝ} (hT : 0 < T) (A : EulerAllOrderCorrectionData.Data period T) : Type

The prescribed residual is the actual residual of the approximation with this genuine all-order pressure. This is a condition on the input approximation, not an existence or equation assumption about the constructed correction.

• pressure : EulerAllOrderCorrectionData.FieldTower period T

  The actual approximate pressure gradient, with coherent Sobolev realizations.

• gradient (t : ↑(Set.Icc 0 T)) : self.pressure.field t ∈ EulerLiftedGradientSpace.gradientSpace period A.κ A.direction

  The approximate pressure belongs to the same lifted gradient space.

• equation (q : ℕ) (hq : 6 ≤ q) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) : HasDerivAt (EulerVolterraConvolution.extendPath T ⋯ (A.approximation.realization q)) ((A.residual.realization q) ⟨t, ⋯⟩ - EulerCorrectionResidualCancellation.nonlinearity period (EulerAllOrderCorrectionData.Data.atOrder period A q) hq ⟨t, ⋯⟩ ((A.approximation.realization (q + 1)) ⟨t, ⋯⟩) - (EulerSobolevCoefficientPressure.coefficientSobolevOperator period (A.metric.jet q ⟨t, ⋯⟩)) ((self.pressure.realization q) ⟨t, ⋯⟩)) t

  The literal residual identity holds at every finite construction order.

noncomputable def EulerAllOrderDriftCorrection.Budget.correctedFieldTower (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) : EulerAllOrderCorrectionData.FieldTower period T

The approximation plus the actually constructed correction, in every order.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def EulerAllOrderDriftCorrection.Budget.correctedPressureTower (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (R : ApproximationResidual period hT A) : EulerAllOrderCorrectionData.FieldTower period T

The total pressure is the given approximate pressure plus the constructed signed correction pressure, with no independent choice at different orders.

Equations

• One or more equations did not get rendered due to their size.

theorem EulerAllOrderDriftCorrection.Budget.correctedFieldTower_initial (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (q : ℕ) : ((correctedFieldTower period B).realization q) ⟨0, ⋯⟩ = (A.approximation.realization q) ⟨0, ⋯⟩

The corrected field has exactly the prescribed initial field at every order.

theorem EulerAllOrderDriftCorrection.Budget.correctedFieldTower_divergence (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (t : ↑(Set.Icc 0 T)) : (correctedFieldTower period B).field t ∈ EulerLiftedGradientSpace.divergenceFreeSpace period A.κ A.direction

Addition preserves the actual closed lifted divergence constraint.

theorem EulerAllOrderDriftCorrection.Budget.correctedPressureTower_gradient (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (R : ApproximationResidual period hT A) (t : ↑(Set.Icc 0 T)) : (correctedPressureTower period B R).field t ∈ EulerLiftedGradientSpace.gradientSpace period A.κ A.direction

The total pressure remains an actual lifted gradient.

theorem EulerAllOrderDriftCorrection.Budget.correctedFieldTower_error_energy (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (P : ℕ) (t : ↑(Set.Icc 0 T)) : EulerGevreyMetricEstimate.energyNorm period P ⋯ (B.radius t) ((EulerCorrectionEnergyData.MetricBudget.operatorPath period B.metric) t) (((correctedFieldTower period B).realization (P + 6 + 1)) t - (A.approximation.realization (P + 6 + 1)) t) ≤ 2 * (B.spatial (P + 6) ⋯).full.residual * Real.exp (3 * B.growthCoefficient * ↑t) ∧ EulerGevreyMetricEstimate.energyNorm period P ⋯ (B.radius t) ((EulerCorrectionEnergyData.MetricBudget.operatorPath period B.metric) t) (((correctedFieldTower period B).realization (P + 6 + 1)) t - (A.approximation.realization (P + 6 + 1)) t) ≤ B.delta / 2

The exact solution differs from the approximation by precisely the small correction, retaining both proved energy bounds at every external cutoff.

theorem EulerAllOrderDriftCorrection.Budget.correctedFieldTower_hasDerivAt (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (R : ApproximationResidual period hT A) (q : ℕ) (hq : 6 ≤ q) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) : HasDerivAt (EulerVolterraConvolution.extendPath T ⋯ ((correctedFieldTower period B).realization q)) (-EulerCorrectionResidualCancellation.nonlinearity period (EulerAllOrderCorrectionData.Data.atOrder period A q) hq ⟨t, ⋯⟩ (((correctedFieldTower period B).realization (q + 1)) ⟨t, ⋯⟩) - (EulerSobolevCoefficientPressure.coefficientSobolevOperator period (A.metric.jet q ⟨t, ⋯⟩)) (((correctedPressureTower period B R).realization q) ⟨t, ⋯⟩)) t

The input residual identity and the proved correction equation give the actual zero-residual nonlinear equation, with the actual total pressure. There is no assumption of existence or an energy bound for the correction.

theorem EulerAllOrderDriftCorrection.exists_exact_lifted_solution (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (R : ApproximationResidual period hT A) : ∃ (Z : EulerAllOrderCorrectionData.FieldTower period T) (Q : EulerAllOrderCorrectionData.FieldTower period T), (∀ (q : ℕ), (Z.realization q) ⟨0, ⋯⟩ = (A.approximation.realization q) ⟨0, ⋯⟩) ∧ (∀ (t : ↑(Set.Icc 0 T)), Z.field t ∈ EulerLiftedGradientSpace.divergenceFreeSpace period A.κ A.direction) ∧ (∀ (t : ↑(Set.Icc 0 T)), Q.field t ∈ EulerLiftedGradientSpace.gradientSpace period A.κ A.direction) ∧ (∀ (P : ℕ) (t : ↑(Set.Icc 0 T)), EulerGevreyMetricEstimate.energyNorm period P ⋯ (B.radius t) ((EulerCorrectionEnergyData.MetricBudget.operatorPath period B.metric) t) ((Z.realization (P + 6 + 1)) t - (A.approximation.realization (P + 6 + 1)) t) ≤ 2 * (B.spatial (P + 6) ⋯).full.residual * Real.exp (3 * B.growthCoefficient * ↑t) ∧ EulerGevreyMetricEstimate.energyNorm period P ⋯ (B.radius t) ((EulerCorrectionEnergyData.MetricBudget.operatorPath period B.metric) t) ((Z.realization (P + 6 + 1)) t - (A.approximation.realization (P + 6 + 1)) t) ≤ B.delta / 2) ∧ ∀ (q : ℕ) (hq : 6 ≤ q) (t : ℝ) (ht : t ∈ Set.Ioo 0 T), HasDerivAt (EulerVolterraConvolution.extendPath T ⋯ (Z.realization q)) (-EulerCorrectionResidualCancellation.nonlinearity period (EulerAllOrderCorrectionData.Data.atOrder period A q) hq ⟨t, ⋯⟩ ((Z.realization (q + 1)) ⟨t, ⋯⟩) - (EulerSobolevCoefficientPressure.coefficientSobolevOperator period (A.metric.jet q ⟨t, ⋯⟩)) ((Q.realization q) ⟨t, ⋯⟩)) t

A single coherent exact lifted solution and total pressure are constructed from the drift budget and the literal approximate residual identity.