Iterates Corrected Quarter Budget

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_corrected_scalar_budget_quarter {C C₀ F c d : ℝ} (hC : 0 ≤ C) (hC₀ : 1 ≤ C₀) (hF : C₀ ≤ F) (hlarge : 32 * C ≤ C₀) (hc : c ≤ C / C₀ ^ 3) (hd : d ≤ C / C₀ + 2 * C / C₀ ^ 2) : C / F ^ 2 + 2 * (C / F ^ 4) + 2 * c + d ≤ 1 / 4

Additional constant room controls independently maximized scalar and coordinate-gradient norms while retaining the C/C0 contribution.