Iterates Previous Material Scale

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_previous_material_scale_bound (n a b : ℕ) {κ D V r L Cs Cv Cc Gc Gp q : ℝ} (hκ : 0 < κ) (hD : 0 ≤ D) (hV : 0 ≤ V) (hr : 0 ≤ r) (hL : 0 < L) (hCs : 0 ≤ Cs) (hCv : 0 ≤ Cv) (hq : 0 ≤ q) (hQ : D * L ^ 2 ≤ Cs * q) (hvel : V * r ≤ Cv * κ * L ^ 2) : 24 * D ^ 2 / κ * (8 * κ ^ 2 * Gc ^ 2 * (↑(n + 2 + a).factorial * L ^ (n + 2)) ^ 2 + 512 * κ ^ 2 * Cc ^ 2 * Gp ^ 2 * (↑(n + 2 + b).factorial * L ^ (n + 2)) ^ 2 + 544 * V ^ 2 * r ^ 2 * Gc ^ 2 * (↑(n + 1 + a).factorial * L ^ n) ^ 2) ≤ Cs ^ 2 * q ^ 2 * κ * ((192 + 13056 * Cv ^ 2) * Gc ^ 2 * (↑(n + 2 + a).factorial * L ^ n) ^ 2 + 12288 * Cc ^ 2 * Gp ^ 2 * (↑(n + 2 + b).factorial * L ^ n) ^ 2)

Normalize the previous-material energy without discarding its two preceding amplitudes. Both contributions retain the squared oscillatory gain.