The relative leading-gradient error e.leadingord

Source: enhance.tex 8114–8269 (e.grad.tildetheta.again and the five displays before e.leadingord). The bound

√κ_m ‖∇θTilde_m - F ∇T_{m-1}‖_{L²_{t,x}} ≤ C ε_{m-1}^{2δ} S, S = √κ_{m-1} ‖∇θ_{m-1}‖_{L²_{t,x}},

is exactly the field RelativeLeaves.hLeadingError. The proof is the exact decomposition (LeadingErrorAlgebra), the pointwise bounds LeadingErrorBoundsFields/...Error, the L² assembly LeadingErrorBoundsAssembly, and the scale package left_to_show_scales. At the terminal scale m = M only the uniform bound a_m² ε_m⁴/κ_m ≤ K κ_{m-1} (valid through m = M) is used, never the printed boundedness of √(κ_m/κ_{m-1}) ε_m^{-γ}; the HTilde_m input is the uniform ε^{4δ} bound.

theorem AVenhance.Infra.Section5.RelativeError.one_le_Nstar {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) : 1 ≤ Nstar β

The number of iterates N_* is positive.

theorem AVenhance.Infra.Section5.RelativeError.relative_leading_error (β C₀ A CH : ℝ) (hA : 1 ≤ A) (hCH : 0 ≤ CH) : ∃ (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 → have S := √(I.kappaSeq κ M (m - 1)) * √(spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θprev s) x); √(I.kappaSeq κ M (m - 1)) * √(spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (T (Nstar β) s) x) ≤ A * S → (∀ (i : Fin 2), √(I.kappaSeq κ M (m - 1)) * √(spaceTimeGradNormSq fun (s : ℝ) => spaceGrad (Section4.iterateSpatialWord [i] (T (Nstar β) s))) ≤ A * (A / epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2)) * S) → √(I.kappaSeq κ M m) * √(spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (I.Hm hΦ m (I.kappaSeq κ M m) (T (Nstar β)) s) x) ≤ CH * epsilon β I.Λ (m - 1) ^ (4 * delta β) * S → √(I.kappaSeq κ M m) * √(spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (I.ansatz hΦ m (I.kappaSeq κ M m) (T (Nstar β)) s) x - LeftToShow.leadingGrad I hΦ m (I.kappaSeq κ M m) (T (Nstar β)) s x) ≤ Ca * epsilon β I.Λ (m - 1) ^ (2 * delta β) * S

e.leadingord: the leading-gradient error of the ansatz, relative to the amplitude S = √κ_{m-1} ‖∇θ_{m-1}‖ (the field RelativeLeaves.hLeadingError).