Amplitude-generic leading-energy estimates on the actual datum and T iterates. The quadratic error has amplitude S squared; the base consumes only integrated gradients.

theorem AVenhance.Infra.Section5.RelativeError.relative_leading_energy_of_T_bounds (β C₀ A : ℝ) (hA : 2 ^ 14 ≤ A) : ∃ (C : ℝ), ∀ (I : Ingredients β), I.Czeta ≤ C₀ → I.Cxi ≤ C₀ → I.Chat ≤ C₀ → C ≤ ↑I.Λ → ∀ (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I Φ), ∀ κ ∈ permissibleSet β I.Λ, ∀ (M : ℕ), 1 ≤ M → κ ∈ permittedInterval β I.Λ M → ∀ (m : ℕ), 2 ≤ m → m ≤ M → ∀ (S : ℝ), 0 ≤ S → ∀ (θ₀ : Homogenization.Vec 2 → ℝ) (θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ), I.IsTIterates hΦ m (I.kappaSeq κ M m) (I.kappaSeq κ M (m - 1)) θ₀ θprev T → √(I.kappaSeq κ M (m - 1)) * √(spaceTimeGradNormSq fun (t : ℝ) (x : Homogenization.Vec 2) => spaceGrad (T (Nstar β) t) x) ≤ A * S → √(spaceTimeGradNormSq (LeftToShow.materialGrad (streamVel (Φ (m - 1))) (T (Nstar β)))) ≤ A * epsilon β I.Λ (m - 1) ^ (3 * delta β) * (√(I.kappaSeq κ M (m - 1)))⁻¹ * S * (tauP β I.Λ m)⁻¹ → PositiveTemperatureJets A (epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2)) S (T (Nstar β)) → |I.kappaSeq κ M m * spaceTimeGradNormSq (LeftToShow.leadingGrad I hΦ m (I.kappaSeq κ M m) (T (Nstar β))) - I.kappaSeq κ M (m - 1) * spaceTimeGradNormSq fun (t : ℝ) (x : Homogenization.Vec 2) => spaceGrad (T (Nstar β) t) x| ≤ C * epsilon β I.Λ (m - 1) ^ (2 * delta β) * S ^ 2

e.left.to.show (additive), conditional only on the three T_{m-1} source estimates: e.Tm.reg.upgrade (n = 0 L²_tH¹ part hT0; all orders L∞_tL²_x part hTall) and e.barf.cascade (n = 0, ℓ = 1, hDt), with one constant A ≥ 2^14.