Iterates TSource Scale

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_T_source_scale {e γ R C₀ ρ : ℝ} (he : 0 < e) (hR : 0 < R) (hC : 1 ≤ C₀) (hscale : e ^ (1 + γ / 2) ≤ R) (hsmall : ρ ≤ (4 * C₀ ^ 3)⁻¹) : max 1 (e ^ (2 + γ) * R ^ (-2)) = 1 ∧ max (C₀ * e ^ (-1 - γ / 2)) (C₀ / R) = C₀ * e ^ (-1 - γ / 2) ∧ C₀ ^ 3 * ρ ≤ 1 / 4

The original T radius condition collapses both maxima to the coarse scale.

theorem AVenhance.Infra.Section4.iterate_T_frequency_bound {C₀ E : ℝ} (hC : 1 ≤ C₀) (hE : 0 ≤ E) : 4 * (C₀ * E) ≤ 4 * C₀ ^ 3 * E

The printed enlarged T frequency dominates the finite-sum frequency.