Iterates Half Square Scale

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_half_square_scale_bound (n : ℕ) {D L C q N R : ℝ} (hD : 0 ≤ D) (hL : 0 < L) (hC : 0 ≤ C) (hq : 0 ≤ q) (hR : 0 ≤ R) (hscale : D * L ^ 2 ≤ C * q) : 8 * D ^ 2 * (N * ↑(n + 2).factorial * L ^ (n + 2)) ^ 2 + 16 * D ^ 2 * R * N ^ 2 * ↑(n + 1).factorial * ↑(n + 3).factorial * L ^ (n + 1) * L ^ (n + 3) ≤ (8 + 32 * R) * C ^ 2 * q ^ 2 * (N * ↑(n + 2).factorial * L ^ n) ^ 2

The retained terminal term and material product both have the first-step q-squared scale. No factorial gain or initial-data division is used.