Iterates Stream Budget Scales

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_quadratic_stream_scale_identity {κ a e L : ℝ} (he : e ≠ 0) (hL : L ≠ 0) (hκ : κ ≠ 0) : 16 / κ * (32 * a * e ^ 2) ^ 2 * (2 * (256 * e⁻¹ / L) ^ 2) ^ 2 / κ = 16 * 32 ^ 2 * 4 * 256 ^ 4 * (a / (κ * L ^ 2)) ^ 2

Cancellation of the microscopic radius in the quadratic stream term. This identifies the fourth-power gain without estimating either factor alone.

theorem AVenhance.Infra.Section4.iterate_quadratic_stream_scale_bound {κ a e L C F : ℝ} (hκ : 0 < κ) (ha : 0 ≤ a) (he : e ≠ 0) (hL : 0 < L) (hC : 0 ≤ C) (hscale : a / (κ * L ^ 2) ≤ C / F ^ 2) : 16 / κ * (32 * a * e ^ 2) ^ 2 * (2 * (256 * e⁻¹ / L) ^ 2) ^ 2 / κ ≤ 16 * 32 ^ 2 * 4 * 256 ^ 4 * C ^ 2 / F ^ 4

The microscopic cancellation gives the F-to-the-minus-four gain.