Iterates First Forcing Gain

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_first_remainder_forcing_gain {κ D L C Ccoef ρ q E g gF : ℝ} (hκ : 0 < κ) (hD : 0 ≤ D) (hC : 0 ≤ C) (hρ : 0 ≤ ρ) (hq : 0 < q) (hE : 0 ≤ E) (hscale : D * L ^ 2 ≤ C * q) (hρq : ρ ≤ q) (hprevious : κ * g ≤ E) (hforcing : gF ≤ 128 * κ * Ccoef ^ 2 * ρ ^ 2 * L ^ 4 * E) : κ * q ^ 2 * g + D ^ 2 / (κ * q ^ 2) * gF ≤ (1 + 128 * C ^ 2 * Ccoef ^ 2) * q ^ 2 * E

The small first-step forcing remainder uses the q-squared Young budget; the centered forcing is treated separately by its half-square cancellation.