Iterates First Budget Small

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_first_energy_budget_small (n : ℕ) {κ D a e r L Ccoef Cs B N ρ F C₀ C : ℝ} (hκ : 0 < κ) (hD : 0 ≤ D) (ha : 0 ≤ a) (_he : 0 ≤ e) (hB : 0 ≤ B) (hr : 0 ≤ r) (hL : 0 < L) (hρ : 0 < ρ) (hρq : ρ ≤ ρ * F ^ 2) (hC : 0 ≤ C) (hC₀ : 1 ≤ C₀) (hF : C₀ ≤ F) (hlarge : 32 * C ≤ C₀) (hsmall : C₀ * (ρ * F ^ 2) ≤ 1) (hmat : 24 * (iterateFirstMaterialCoefficient Cs Ccoef + 384 * Cs ^ 2 + 32 * Ccoef ^ 2) ≤ C) (hu : 24 * (2 * (2 ^ 19 * a) / L ^ 2) / κ ≤ C / F ^ 2) (hv : 24 * (16 / κ * (32 * a * e ^ 2) ^ 2 * (2 * (256 * e⁻¹ / L) ^ 2) ^ 2) / κ ≤ C / F ^ 4) (hc : 24 * (8 * D * B * r) / κ ≤ C * ρ) : (24 * iterateFirstEnergyBudget n κ D a e r L Cs Ccoef B (N * iterateAmplitude (C₀ * (ρ * F ^ 2)) 1 / √κ) N ρ (ρ * F ^ 2) fun (x : ℕ) => 1) ≤ N ^ 2 * iterateAmplitude (C₀ * (ρ * F ^ 2)) 1 ^ 2 * iterateAnalyticWeight n 1 L ^ 2 / 4

The complete explicit higher-increment remainder closes under scalar coefficient scales. The PDE energy inequality is not an assumption here.