Corrected quantitative current-material allocation.

theorem AVenhance.Infra.Section4.iterate_current_material_corrected_remainder_gain {κ D C H q L E g gLap gF : ℝ} (hκ : 0 < κ) (hD : 0 ≤ D) (hC : 0 ≤ C) (hH : 0 ≤ H) (hq : 0 < q) (hE : 0 ≤ E) (hscale : D * L ^ 2 ≤ C * q) (hprevious : κ * g ≤ E) (hLap : κ * gLap ≤ L ^ 4 * E) (hforcing : gF ≤ κ * H * L ^ 4 * E) : 24 * κ * D ^ 2 * gLap + κ * q * g + D ^ 2 / (κ * q) * gF ≤ (24 * C ^ 2 * q ^ 2 + (1 + C ^ 2 * H) * q) * E

Allocate the current forcing with κq. The forcing and preceding-gradient contributions retain q, while transferred diffusion contributes q squared. This is scalar budget algebra; the actual forcing bound is proved separately.