Iterates Energy Budget Split

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_higher_energy_budget_split (n i : ℕ) (κ D a e L Ccoef Cs Cv Cf Gcur Gprev Gprevprev Nprev ρ q : ℝ) (d : ℕ → ℝ) : iterateHigherEnergyBudget n i κ D a e L Ccoef Cs Cv Cf Gcur Gprev Gprevprev Nprev ρ q d = iterateHigherMaterialBudget κ Ccoef Cs Cv Cf Gprev Gprevprev Nprev ρ q (iterateAnalyticWeight n (i + 1) L) (iterateAnalyticWeight n i L) + iterateStreamEnergyBudget n (2 * (2 ^ 19 * a) * Gcur ^ 2 / L ^ 2) (16 / κ * (32 * a * e ^ 2) ^ 2 * Gcur ^ 2 * (2 * (256 * e⁻¹ / L) ^ 2) ^ 2) (8 * D * (8192 * a * e) * Gprev * Gcur * (256 * e⁻¹)) (iterateAnalyticWeight n (i + 1) L) d

The explicit higher remainder separates into its material contribution and the three exact current-order kernels.

theorem AVenhance.Infra.Section4.iterate_first_energy_budget_split (n : ℕ) (κ D a e r L C Ccoef B Gcur N ρ q : ℝ) (d : ℕ → ℝ) : iterateFirstEnergyBudget n κ D a e r L C Ccoef B Gcur N ρ q d = iterateFirstMaterialBudget C Ccoef ρ q N (iterateAnalyticWeight n 1 L) (iterateAnalyticWeight n 0 L) + iterateStreamEnergyBudget n (2 * (2 ^ 19 * a) * Gcur ^ 2 / L ^ 2) (16 / κ * (32 * a * e ^ 2) ^ 2 * Gcur ^ 2 * (2 * (256 * e⁻¹ / L) ^ 2) ^ 2) (8 * D * B * (N / √κ) * Gcur * r) (iterateAnalyticWeight n 1 L) d

The exceptional first remainder has the same current-order kernels.