The diffusivity scales κ_j = ε_{j+1}^p

Abstract-real facts used to produce the sequence κ_j of the combined main theorem: the exponent p = 2β/(qβ+1) is positive, and 4 ε_{m+1}^p < ε_m^p once Λ ≥ 5^{1/p}.

theorem AVenhance.Infra.FullTheorem.Full.permitted_exponent_pos {β : ℝ} (h1 : 1 < β) (h2 : β < 4 / 3) : 0 < 2 * β / (q β + 1)

The exponent 2β/(qβ+1) is positive for 1 < β < 4/3.

theorem AVenhance.Infra.FullTheorem.Full.five_le_rpow {p L : ℝ} (hp : 0 < p) (hL : 5 ^ (1 / p) ≤ L) : 5 ≤ L ^ p

Λ ≥ 5^{1/p} implies Λ^p ≥ 5.

theorem AVenhance.Infra.FullTheorem.Full.four_mul_epsilon_rpow_lt {β p : ℝ} (I : Ingredients β) (hp : 0 < p) (hΛ : 5 ^ (1 / p) ≤ ↑I.Λ) (m : ℕ) : 4 * epsilon β I.Λ (m + 1) ^ p < epsilon β I.Λ m ^ p

The four-fold gap 4 ε_{m+1}^p < ε_m^p.