The corrected 4δ exprat estimate for the auxiliary κ′ chain.

theorem AVenhance.Infra.Section3.KappaPrimeExprat.epsilon_le_one_over_128 {β : ℝ} {Λ n : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) (hn : 1 ≤ n) : epsilon β Λ n ≤ 1 / 128

theorem AVenhance.Infra.Section3.two_sub_beta_gamma_nonneg {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) : 0 ≤ 2 - β - gamma β

The exponent of the normalized diffusivity factor is nonnegative.

theorem AVenhance.Infra.Section3.kappaPrimeUniformConstant_pos {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) : 0 < kappaPrimeUniformConstant β

Positivity of the normalization constant used in the uniform κ′ bounds.

theorem AVenhance.Infra.Section3.kappaPrimeAt_exprat_bounds {β : ℝ} {Λ M : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) {κ : ℝ} (hκ : 0 < κ) (hpermitted : κ ∈ permittedInterval β Λ M) {m : ℕ} (hm : 2 ≤ m) (hmM : m < M) : have U := kappaPrimeUniformConstant β; have clo := (1 / 2) ^ (2 - β - gamma β) / (U * 2 ^ (-28)); have chi := (1 + Ingredients.supergeoConstant β / 128) ^ (2 - β - gamma β) / (9 / 80 / U * 2 ^ (-33)); clo * epsilon β Λ (m - 1) ^ (4 * delta β) ≤ epsilon β Λ m ^ 2 / (kappaPrimeAt β Λ κ m (M - m) * tau β Λ m) ∧ epsilon β Λ m ^ 2 / (kappaPrimeAt β Λ κ m (M - m) * tau β Λ m) ≤ chi * epsilon β Λ (m - 1) ^ (4 * delta β)

Uniform corrected 4δ bounds for the κ′ exprat on 2 ≤ m < M. The constants depend only on β.