One-sided permitted-interval bounds at the top scale.

theorem AVenhance.Infra.Section3.LRecurseTop.top_exponent_gap {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) : 2 * delta β ≤ q β * (2 - β + gamma β) - (2 - β + 4 * delta β)

theorem AVenhance.Infra.Section3.l_recurse_top {β : ℝ} {Λ M : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) {κ : ℝ} (hκ : 0 < κ) (hpermitted : κ ∈ permittedInterval β Λ M) (hM : 1 ≤ M) : 1 / 2 * a β Λ M * epsilon β Λ M ^ (2 + gamma β) ≤ κ ∧ epsilon β Λ M ^ 2 / (κ * tau β Λ M) ≤ kappaPrimeEndpointExpratConstant β * epsilon β Λ (M - 1) ^ (2 * delta β)

The one-sided facts at the terminal index. The coefficient depends only on β. The ratio estimate includes the exceptional case M = 1.