Iterates Physical Budget Scales

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_diffusive_radius_square {e γ L F : ℝ} (he : 0 < e) (hF : F = e ^ (1 + γ / 2) * L) : e ^ (2 + γ) * L ^ 2 = F ^ 2

The analytic radius converts the literal diffusivity power to F squared.

theorem AVenhance.Infra.Section4.iterate_stream_ratio_of_literal_lower {a e γ κ c L F : ℝ} (he : 0 < e) (hκ : 0 < κ) (hc : 0 < c) (hL : 0 < L) (hFpos : 0 < F) (hlower : c * (a * e ^ (2 + γ)) ≤ κ) (hF : F = e ^ (1 + γ / 2) * L) : a / (κ * L ^ 2) ≤ 1 / c / F ^ 2

Literal lower diffusivity scaling gives the reciprocal analytic gain.

theorem AVenhance.Infra.Section4.iterate_primitive_radius_scale {a e γ κ τ K Ck H ρ L F : ℝ} (he : 0 < e) (hτ : 0 ≤ τ) (hK : 0 ≤ K) (hCk : 0 ≤ Ck) (hupper : κ ≤ Ck * (a * e ^ (2 + γ))) (htime : τ * a ≤ H * ρ) (hF : F = e ^ (1 + γ / 2) * L) : 2 * τ * K * κ * L ^ 2 ≤ 2 * K * Ck * H * (ρ * F ^ 2)

The explicit primitive has the q gain from upper diffusivity scaling and the proved amplitude-times-period bound.

theorem AVenhance.Infra.Section4.iterate_primitive_amplitude_scale {κ τ K a H ρ : ℝ} (hκ : 0 < κ) (hK : 0 ≤ K) (htime : τ * a ≤ H * ρ) : 2 * τ * K * κ * a / κ ≤ 2 * K * H * ρ

The material primitive factor cancels the diffusivity exactly.

theorem AVenhance.Infra.Section4.iterate_velocity_first_jet_scale {a e : ℝ} (he : e ≠ 0) : 8192 * a * e * (256 * e⁻¹) = 2 ^ 21 * a

Exact positive first-velocity-jet scale supplied by stream-regularity.