Direct elimination of Σ₂ in the genuine κ = 1, Case-I range

For D ≥ 4, the corrected branch in the definition of τ is at most 2. Thus 2 ≤ s forces τ = s. Since z is the natural ceiling of the same strict real cutoff, the integer carrier of Σ₂ is empty.

theorem MathlibNt.SieveTheory.lemma144_correctedBranch_le_two {D : ℕ} (hD : 4 ≤ D) : (1 - Real.log 2 / Real.log ↑D)⁻¹ ≤ 2

In the Case-I range D ≥ 4, Suzuki's corrected branch is at most 2.

theorem MathlibNt.SieveTheory.lemma144_realTau_eq_s_of_caseI {D : ℕ} {s : ℝ} (hD : 4 ≤ D) (hs : 2 ≤ s) : lemma144RealTau D s = s

In the genuine κ = 1, β = 2, Case-I range, the literal real splitting parameter is s; the corrected branch cannot dominate.

theorem MathlibNt.SieveTheory.lemma144_nat_lt_z_iff_lt_root {D z p : ℕ} {s : ℝ} (hD : 4 ≤ D) (hz : z = ⌈↑D ^ (1 / s)⌉₊) : p < z ↔ ↑p < ↑D ^ (1 / s)

With the source natural ceiling, the strict upper carrier and the real power cutoff define the same strict inequality on natural numbers.

theorem MathlibNt.SieveTheory.lemma144_sigmaTwo_eq_zero_of_kappaOne_caseI (S : BoundingSieve) {N D z : ℕ} {s : ℝ} (hD : 4 ≤ D) (hs : 2 ≤ s) (hz : z = ⌈↑D ^ (1 / s)⌉₊) : suzukiSigmaTwo S N D z (↑D ^ (1 / lemma144RealTau D s)) = 0

Direct Case-I elimination of the actual Σ₂: no lower_eq_half input and no estimate for Σ₂ are used.