Index and power bookkeeping for §5.4. Constants at the first scale explicitly retain their dependence on Λ; fixing Λ(β) makes them depend only on β.

theorem AVenhance.Infra.Section5.mTheta0_spec {β R : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) (hR : 0 < R) : 2 ≤ mTheta0 β Λ R ∧ epsilon β Λ (mTheta0 β Λ R - 1) ^ (1 + gamma β / 2) ≤ R

Membership in the set defining the minimum.

theorem AVenhance.Infra.Section5.MStar.epsilon_le_inv_128 {β : ℝ} {Λ m : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) (hm : 1 ≤ m) : epsilon β Λ m ≤ 128⁻¹

theorem AVenhance.Infra.Section5.MStar.exponent_product (g t v : ℝ) (hg : 0 < 1 + g / 2) : v / (1 + g / 2) * t = 2 * v * t / (2 + g)