TUpgrade Consumers Scales

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_contract_scales (β D : ℝ) (hD : 1 ≤ D) : ∃ (C₁ : ℝ), ∀ (I : Ingredients β), C₁ ≤ ↑I.Λ → ∀ (R : ℝ), 0 < R → ∀ (m : ℕ), mTheta0 β I.Λ R ≤ m → 2 ≤ m ∧ epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2) ≤ R ∧ epsilon β I.Λ (m - 1) ^ (2 * delta β) ≤ (4 * D ^ 3)⁻¹

A threshold chosen before ingredients enforces the T-upgrade smallness; the starting index supplies its radius premise.