Part I: ‖θTilde_m - T_{m-1}‖_{L^∞((0,1];L²)} ≤ C ε_{m-1}^δ ‖θ₀‖_{L²} (e.tildethetam.to.Tm)

Source: enhance.tex 8882-9133. The theorem section_four_ansatz_bound is the N-normalised form of hSectionFourAnsatz on t ∈ (0,1], with the two inputs the proof in the source quotes:

• hTjet: the first-order T jet ‖∇T_{m-1}(s)‖_{L²} ≤ A_T ‖θ₀‖ ε_{m-1}^{-(1+γ/2)} (e.Tm.reg.upgrade, n = 0);
• hHsup: e.Hm.Linfty, ‖HTilde_m(t)‖_{L²} ≤ C_H ε_{m-1}^δ ‖θ₀‖.

The corrector part is bounded pointwise (ansatz_sub_T_sub_Hm_abs_le) by 4 ‖Χ‖_∞ (|∂₁T| + |∂₂T|) with ‖Χ‖_∞ = a ε_m³ /(2π κ_m), and the scale package left_to_show_scales plus q(1-γ) - 1 - γ/2 = 4δ turn it into K² ε_{m-1}^δ.

theorem AVenhance.Infra.Section5.Integration.section_four_ansatz_bound (β C₀ AT CHs : ℝ) (hAT : 0 ≤ AT) (hCHs : 0 ≤ CHs) : ∃ (Ca : ℝ), 0 ≤ Ca ∧ ∀ (I : Ingredients β), I.Czeta ≤ C₀ → I.Cxi ≤ C₀ → I.Chat ≤ C₀ → ∀ (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I Φ), ∀ κ ∈ permissibleSet β I.Λ, ∀ (M : ℕ), 1 ≤ M → κ ∈ permittedInterval β I.Λ M → ∀ (m : ℕ), 2 ≤ m → m ≤ M → ∀ (θ₀ : Homogenization.Vec 2 → ℝ) (θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ), IsClassicalSol (streamVel (Φ (m - 1))) (I.kappaSeq κ M (m - 1)) (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev → I.IsTIterates hΦ m (I.kappaSeq κ M m) (I.kappaSeq κ M (m - 1)) θ₀ θprev T → FirstOrderSliceJetContract I m T AT √(l2NormSq θ₀) → HmSupContract I hΦ m (I.kappaSeq κ M m) θ₀ T CHs → ∀ t ∈ Set.Ioc 0 1, √(l2NormSq fun (x : Homogenization.Vec 2) => I.ansatz hΦ m (I.kappaSeq κ M m) (T (Nstar β)) t x - T (Nstar β) t x) ≤ Ca * epsilon β I.Λ (m - 1) ^ delta β * √(l2NormSq θ₀)

e.tildethetam.to.Tm (N-normalised): the ansatz is within C ε_{m-1}^δ ‖θ₀‖ of T_{m-1} in L²(𝕋²) for every t ∈ (0,1].