Numerical relations among the §2.1 parameters.

theorem AVenhance.Infra.Ingredients.q_eq_beta_div_four_sub_one {β : ℝ} (hβ : 1 < β) : q β = β / (4 * (β - 1))

e.q.def.0 (986-989): the definition simplifies to q = β / (4(β - 1)).

theorem AVenhance.Infra.Ingredients.one_lt_q {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) : 1 < q β

e.q.def (999-1001): q > 1 on the β range.

theorem AVenhance.Infra.Ingredients.delta_eq_q_fraction {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) : delta β = (q β - 1) ^ 2 / (4 * (q β + 1) * (4 * q β - 1))

e.delta (1008): an algebraically simplified expression for δ.

theorem AVenhance.Infra.Ingredients.delta_pos {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) : 0 < delta β

e.delta (1008): the chosen δ is positive.

theorem AVenhance.Infra.Ingredients.delta_le_one_sixteenth {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) : delta β ≤ 1 / 16

e.delta (1004-1009): δ ≤ 1/16 throughout the allowed β range.

theorem AVenhance.Infra.Ingredients.gamma_pos {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) : 0 < gamma β

e.gamma (1025): γ is positive on the β range.

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

e.delta and e.gamma (1008, 1025): γ ≥ 4δ.

theorem AVenhance.Infra.Ingredients.Nstar_corrections_nonneg {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) : 0 ≤ 8 + 4 * (q β - 1) * (β + (q β - 1) * β / (q β + 1)) / delta β ∧ 0 ≤ 8 + 128 * q β ^ 2 / (q β - 1) ∧ 0 ≤ 8 + 128 * q β ^ 2 * (q β - 1)

The three correction terms of N_* are nonnegative.

theorem AVenhance.Infra.Ingredients.Nstar_eq_ceil (β : ℝ) : Nstar β = ⌈1 / delta β ^ 2 + 500 / delta β + (8 + 4 * (q β - 1) * (β + (q β - 1) * β / (q β + 1)) / delta β) + (8 + 128 * q β ^ 2 / (q β - 1)) + (8 + 128 * q β ^ 2 * (q β - 1))⌉₊

The real number whose ceiling is N_*.

theorem AVenhance.Infra.Ingredients.Nstar_ge_defining_real {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) : 1 / delta β ^ 2 + 500 / delta β ≤ ↑(Nstar β)

e.N (1018): N_* dominates its source defining quantity 1/δ² + 500/δ.

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

Correction: N_* ≥ 8 + 4(q-1)(β+γ)/δ (the requirement used at line 7850).

theorem AVenhance.Infra.Ingredients.Nstar_ge_eight_add_div {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) : 8 + 128 * q β ^ 2 / (q β - 1) ≤ ↑(Nstar β)

Correction: N_* ≥ 8 + 128q²/(q-1) (line 7850).

theorem AVenhance.Infra.Ingredients.Nstar_ge_eight_add_mul {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) : 8 + 128 * q β ^ 2 * (q β - 1) ≤ ↑(Nstar β)

Correction: N_* ≥ 8 + 128q²(q-1) (line 7883).

theorem AVenhance.Infra.Ingredients.Nstar_ge_256 {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) : 256 ≤ Nstar β

e.N (1018) and e.delta (1008): the integer satisfies N_* ≥ 256.