Pure real algebra for the exponents in §§5.2–5.4. No scale powers are expanded. The printed γβ at line 7441 must be qγ.

theorem AVenhance.Infra.Numeric.gamma_eq_beta_fraction {β : ℝ} (hβ : 1 < β) : gamma β = β * (4 - 3 * β) / (5 * β - 4)

The gamma as a rational function of beta.

theorem AVenhance.Infra.Numeric.delta_eq_beta_fraction {β : ℝ} (hβ : 1 < β) : delta β = (4 - 3 * β) ^ 2 / (16 * (5 * β - 4))

The delta as a rational function of beta.

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

The corrected s6.exponent.8delta: the decrement is eight delta.

theorem AVenhance.Infra.Numeric.four_delta_identity {β : ℝ} (hβ : 1 < β) : q β * (1 - gamma β) - 1 - gamma β / 2 = 4 * delta β

e.put.pipe.smoke.it and the initial-defect exponent.

theorem AVenhance.Infra.Numeric.gamma_ge_four_delta {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) : 4 * delta β ≤ gamma β

Re-export the existing parameter estimate needed by the error bounds.

theorem AVenhance.Infra.Numeric.kill_half_gamma {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) : 0 < q β - 1 - gamma β / 2

The extra derivative is compensated by a strictly positive scale exponent.

theorem AVenhance.Infra.Numeric.Nstar_exponent_budget {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) : 8 * delta β + 4 * (q β - 1) * (β + gamma β) ≤ delta β * ↑(Nstar β)

Nstar supplies the actual exponent budget used in §5.2.