Algebraic scale conversion for the corrected 4δ exponent in the diffusivity-recursion estimate.

theorem AVenhance.Infra.Section3.exprat_source_exponent_eq_eight_delta {β : ℝ} (hβ : 1 < β) : (2 - β) * (q β - 1) - q β * gamma β = 8 * delta β

The exponent identity in the source proof is 8δ.

theorem AVenhance.Infra.Section3.exprat_normalized_exponent_eq_four_delta {β : ℝ} (hβ : 1 < β) : q β * (2 - β - gamma β) - (2 - β + 4 * delta β) = 4 * delta β

The corrected scale exponent after using τ_m ≍ ε_{m-1}^{2-β+4δ}.

theorem AVenhance.Infra.Section3.exprat_factorization {β e τ κm : ℝ} (he : 0 < e) (hτ : 0 < τ) (hκm : 0 < κm) : e ^ 2 / (κm * τ) = e ^ (2 - β - gamma β) / τ * (e ^ (β + gamma β) / κm)

Factor the quotient so that the 4δ contribution from the time scale and the normalized diffusivity contribution can be bounded independently.

theorem AVenhance.Infra.Section3.ExpratScaling.rpow_scale_ratio_bounds {x y A B τ lo hi p q r : ℝ} (hy : 0 < y) (hA : 0 < A) (hB : 0 < B) (hp : 0 ≤ p) (hτ : 0 < τ) (hlo : 0 < lo) (hhi : 0 < hi) (hscaleLo : A * y ^ q ≤ x) (hscaleHi : x ≤ B * y ^ q) (hτLo : lo * y ^ r ≤ τ) (hτHi : τ ≤ hi * y ^ r) : A ^ p / hi * y ^ (q * p - r) ≤ x ^ p / τ ∧ x ^ p / τ ≤ B ^ p / lo * y ^ (q * p - r)

theorem AVenhance.Infra.Section3.exprat_bounds_of_normalized_kappa {β e eprev τ κm aLo aHi tauLo tauHi kappaLo kappaHi : ℝ} (hβ : 1 < β) (he : 0 < e) (heprev : 0 < eprev) (hτ : 0 < τ) (hκm : 0 < κm) (haLo : 0 < aLo) (haHi : 0 < aHi) (htauLo : 0 < tauLo) (htauHi : 0 < tauHi) (hkappaLo : 0 < kappaLo) (hkappaHi : 0 < kappaHi) (hp : 0 ≤ 2 - β - gamma β) (hscaleLo : aLo * eprev ^ q β ≤ e) (hscaleHi : e ≤ aHi * eprev ^ q β) (htimeLo : tauLo * eprev ^ (2 - β + 4 * delta β) ≤ τ) (htimeHi : τ ≤ tauHi * eprev ^ (2 - β + 4 * delta β)) (hkappaLoBound : kappaLo * e ^ (β + gamma β) ≤ κm) (hkappaHiBound : κm ≤ kappaHi * e ^ (β + gamma β)) : aLo ^ (2 - β - gamma β) / (kappaHi * tauHi) * eprev ^ (4 * delta β) ≤ e ^ 2 / (κm * τ) ∧ e ^ 2 / (κm * τ) ≤ aHi ^ (2 - β - gamma β) / (kappaLo * tauLo) * eprev ^ (4 * delta β)

The normalized κ_m estimate and the corrected time-scale exponent imply the two-sided e.exprat.bound with exponent 4δ. The scale-ratio and time-scale hypotheses are stated explicitly so this lemma does not conceal the separate proof of the κ_m recurrence estimate.