Iterates Physical Coefficient Bundle

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_physical_coefficient_bundle {a e γ κ c Ck τ K H ρ L F Cflow Cmean : ℝ} (ha : 0 ≤ a) (he : 0 < e) (hκ : 0 < κ) (hc : 0 < c) (hCk : 0 ≤ Ck) (hτ : 0 ≤ τ) (hK : 0 ≤ K) (hH : 0 ≤ H) (hρ : 0 ≤ ρ) (hL : 0 < L) (hF1 : 1 ≤ F) (hlower : c * (a * e ^ (2 + γ)) ≤ κ) (hupper : κ ≤ Ck * (a * e ^ (2 + γ))) (htime : τ * a ≤ H * ρ) (hF : F = e ^ (1 + γ / 2) * L) : have Cs := iterateBudgetScaleConstant K Ck c H; have C := iterateBudgetUniversalConstant K Ck c H Cflow Cmean; 2 * τ * K * κ * L ^ 2 ≤ Cs * (ρ * F ^ 2) ∧ 2 ^ 21 * a ≤ Cs * κ * L ^ 2 ∧ 2 * τ * K * κ * (2 ^ 21 * a) ≤ Cs * κ * ρ ∧ 24 * (2 * (2 ^ 19 * a) / L ^ 2) / κ ≤ C / F ^ 2 ∧ 24 * (16 / κ * (32 * a * e ^ 2) ^ 2 * (2 * (256 * e⁻¹ / L) ^ 2) ^ 2) / κ ≤ C / F ^ 4 ∧ 24 * (8 * (2 * τ * K * κ) * (8192 * a * e) * (256 * e⁻¹)) / κ ≤ C * ρ

Every scalar scale required by the actual induction follows from literal pointwise diffusivity bounds and the amplitude-times-period estimate.