Iterates Material Budget Normalized

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_higher_material_budget_normalized {κ Ccoef Cs Cv Cf N ρ q C₀ W Wprev : ℝ} {i : ℕ} (hκ : 0 < κ) (hρ : 0 ≤ ρ) (hρq : ρ ≤ q) (hC₀ : 0 < C₀) (hq : 0 < q) (hsmall : C₀ * q ≤ 1) (hi : 1 ≤ i) (hW : 0 ≤ Wprev) (hWle : Wprev ≤ W) : 24 * iterateHigherMaterialBudget κ Ccoef Cs Cv Cf (N * iterateAmplitude (C₀ * q) i / √κ) (N * iterateAmplitude (C₀ * q) (i - 1) / √κ) (N * iterateAmplitude (C₀ * q) i) ρ q W Wprev ≤ (24 * amnrMaterialMajorantConstant Ccoef Cs Cv Cf / C₀ + 2 * (24 * amnrMaterialMajorantConstant Ccoef Cs Cv Cf) / C₀ ^ 2) * N ^ 2 * iterateAmplitude (C₀ * q) (i + 1) ^ 2 * W ^ 2

The explicit higher material budget closes with the corrected C/C0 term. Only scalar coefficient scales and amplitudes enter this algebraic lemma.