Abstract-real scale arithmetic for the flux source contracts

Pure real lemmas combining the scale package left_to_show_scales with the pointwise flux bounds (source e.monster.est.7, .10, .11). The key facts are

• κ_m + a_m ε_m² ≤ (1 + √K) √κ_m √κ_{m-1} (the source's κ_m + a_m ε_m² ≲ √(κ_m κ_{m-1}));
• ε_m (a_m ε_m²/κ_m) ε_{m-1}^{-(1+γ/2)} ≤ 2π K² ε_{m-1}^δ.

theorem AVenhance.Infra.Section5.Contracts.sa_mu_le {a ε κ κp K : ℝ} (ha : 0 ≤ a) (hκ : 0 < κ) (hκκp : κ ≤ κp) (hK : 0 ≤ K) (h : a ^ 2 * ε ^ 4 / κ ≤ K * κp) : κ + a * ε ^ 2 ≤ (1 + √K) * √κ * √κp

κ + a ε² ≤ (1 + √K) √κ √κ'.

theorem AVenhance.Infra.Section5.Contracts.sa_chi_ratio {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) {K e em c : ℝ} (hK : 1 ≤ K) (he : 0 < e) (he1 : e ≤ 1) (hem : 0 < em) (hc0 : 0 ≤ c) (hc : c ≤ K * em ^ (-gamma β)) (hemK : em ≤ K * e ^ q β) : em * c * (e ^ (1 + gamma β / 2))⁻¹ ≤ 2 * Real.pi * K ^ 2 * e ^ delta β

ε_m c ρ⁻¹ ≤ 2π K² ε^δ for c = a ε_m²/κ_m.

theorem AVenhance.Infra.Section5.Contracts.sa_twistie3_arith {μ e sT sp sm A B K : ℝ} (hμ : μ ≤ (1 + √K) * sm * sp) (hsT : 0 ≤ sT) (he : 0 ≤ e) (hsm : 0 ≤ sm) (hT : sp * sT ≤ A * B) : 6 * (μ * e) * sT ≤ 6 * (1 + √K) * A * e * sm * B

Final arithmetic for twistie3.

theorem AVenhance.Infra.Section5.Contracts.sa_normie2_arith {μ sH sp sm CH E B K : ℝ} (hμ : μ ≤ (1 + √K) * sm * sp) (hsH : 0 ≤ sH) (hsm : 0 ≤ sm) (hH : sp * sH ≤ CH * E * B) : 3 * μ * sH ≤ 3 * (1 + √K) * sm * (CH * E * B)

Final arithmetic for normie2.

theorem AVenhance.Infra.Section5.Contracts.sa_normie1_arith {μ cχ D ρ sT s0 s1 sp sm A B K e : ℝ} (hK : 1 ≤ K) (he : 0 ≤ e) (hμ0 : 0 ≤ μ) (hc0 : 0 ≤ cχ) (hρ : 0 < ρ) (hsp : 0 < sp) (hsm : 0 ≤ sm) (hD : D ≤ 2 ^ 16 * ρ⁻¹) (hsT : 0 ≤ sT) (hs0 : 0 ≤ s0) (hs1 : 0 ≤ s1) (hμ : μ ≤ (1 + √K) * sm * sp) (hcρ : cχ * ρ⁻¹ ≤ 2 * Real.pi * K ^ 2 * e) (hT : sp * sT ≤ A * B) (h0 : sp * s0 ≤ A * (A / ρ) * B) (h1 : sp * s1 ≤ A * (A / ρ) * B) : 40 * (2 * (μ * cχ) * D) * sT + 10 * (2 * (μ * cχ)) * s0 + 10 * (2 * (μ * cχ)) * s1 ≤ (80 * 2 ^ 16 * A + 40 * A ^ 2) * ((1 + √K) * (2 * Real.pi * K ^ 2)) * e * sm * B

Final arithmetic for normie1.