The actual nonlinear viscous correction closes its shrinking-radius Gevrey bootstrap from the constructed mild equation.

theorem EulerCorrectionEnergyBootstrap.raise_energy_constant (C0 C X Y r b R B : ℝ) (hC : C0 ≤ C) (hX : 0 ≤ X) (hY : 0 ≤ Y) (hr : 0 ≤ r) (hR : 0 ≤ R) (hB : 0 ≤ B) : C0 * (X + X ^ 2 + r) + (b + C0 * R * (B + X)) * Y ≤ C * (X + X ^ 2 + r) + (b + C * R * (B + X)) * Y

Increasing the single scalar coefficient preserves the signed radius term in the genuine energy estimate.

theorem EulerCorrectionEnergyBootstrap.correction_mild_bootstrap (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (T : ℝ) (hT : 0 ≤ T) (D : EulerCorrectionOperators.CorrectionData period (q + 1) ↑(Set.Icc 0 T)) (KG : (t : ↑(Set.Icc 0 T)) → EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q (D.metric.coefficient t)) (KL : (t : ↑(Set.Icc 0 T)) → EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q (D.linear.coefficient t)) (KQ : (i : Fin 3) → (t : ↑(Set.Icc 0 T)) → EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q ((D.quadratic i).coefficient t)) (hGq : Continuous fun (t : ↑(Set.Icc 0 T)) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (KG t)) (hLq : Continuous fun (t : ↑(Set.Icc 0 T)) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (KL t)) (hQq : ∀ (i : Fin 3), Continuous fun (t : ↑(Set.Icc 0 T)) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (KQ i t)) (hG : Continuous fun (t : ↑(Set.Icc 0 T)) => (D.metric.coefficient t).operator) (N : ℕ) (hN : N + 6 ≤ q + 1) (R Rdot : C(↑(Set.Icc 0 T), ℝ)) (S : EulerCorrectionEnergyData.SpatialBudget period ⋯ D N R) (K : EulerCorrectionEnergyData.MetricBudget period T hT D) (C Δ ρ0 : ℝ) (hC : EulerCorrectionEnergyMajorants.combinedConstant period S K ≤ C) (hΔ : 0 < Δ) (hΔ1 : Δ ≤ 1) (hρ0 : 0 < ρ0) (hdecay : 2 * C * (S.B0 + Δ) * T ≤ ρ0 / 2) (hscale : ρ0 * S.Rc ≤ 1) (hsmall : 2 * S.residual * Real.exp (3 * C * T) ≤ Δ / 2) (hR : ∀ (t : ↑(Set.Icc 0 T)), R t = ρ0 - 2 * C * (S.B0 + Δ) * ↑t) (hRdot : ∀ (t : ↑(Set.Icc 0 T)), Rdot t = -2 * C * (S.B0 + Δ)) (ν : ℝ) (hν : 0 < ν) (hν1 : ν ≤ 1) (e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (hsol : ∀ (t : ↑(Set.Icc 0 T)), e t = (EulerSobolevHeat.heatOperator period (q + 1) (2 * ν * ↑t).toNNReal) 0 + ∫ (r : ℝ) in 0..↑t, (EulerSobolevHeat.heatKernel period q ν hν r) (EulerVolterraConvolution.extendPath T hT (EulerCorrectionLowerData.forcingPath period hq (EulerCorrectionLowerData.lowerData period D KG KL KQ hGq hLq hQq) e) (↑t - r))) (hz : ∀ (t : ↑(Set.Icc 0 T)), EulerCylinderSobolevSpace.value period (D.approximation t) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period D.κ D.direction) (he : ∀ (t : ↑(Set.Icc 0 T)), EulerCylinderSobolevSpace.value period (e t) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period D.κ D.direction) (t : ↑(Set.Icc 0 T)) : EulerGevreyMetricEstimate.energyNorm period N hN (R t) ((EulerCorrectionEnergyData.MetricBudget.operatorPath period K) t) (e t) ≤ 2 * S.residual * Real.exp (3 * C * ↑t) ∧ EulerGevreyMetricEstimate.energyNorm period N hN (R t) ((EulerCorrectionEnergyData.MetricBudget.operatorPath period K) t) (e t) ≤ Δ / 2

Every actual zero-initial nonlinear correction mild solution satisfies the closed Gevrey estimate. The proof derives its full-order all-subinterval energy inequality, source bound, pressure cancellation, and maximal regularity rather than assuming them.