Lemma 14.4, Case I successor: real-τ / Σ₂ frontier

This file keeps Suzuki's literal τ = max s ((1 - log 2 / log D)⁻¹). In particular it does not use the incorrect simplification τ = s to erase Σ₂.

The exact finite recurrence, the global-IH instantiation, the internal Σ₀ endpoint, the natural-ceiling Σ₁₂ theorem, and Claim (14.13) all compile in the current import cone. The theorem below closes the elementary carrier part of the genuine Σ₂ dichotomy: the sum is either in the even, nonempty narrow branch, or is literally zero.

noncomputable def MathlibNt.SieveTheory.lemma144RealTau (D : ℕ) (s : ℝ) : ℝ

The source correction occurring in the upper splitting point of (14.9).

Equations

• MathlibNt.SieveTheory.lemma144RealTau D s = max s (1 - Real.log 2 / Real.log ↑D)⁻¹

structure MathlibNt.SieveTheory.Lemma144SigmaTwoEvenNarrow (N D z : ℕ) (s : ℝ) : Prop

A source-faithful description of the only branch in which Σ₂ still requires (14.22). upper_lt_z says that the upper split point lies strictly below the sieve endpoint; even_depth records the source parity conclusion.

• even_depth : Even N
• upper_lt_z : ↑D ^ (1 / lemma144RealTau D s) < ↑z

theorem MathlibNt.SieveTheory.lemma144_sigmaTwo_evenNarrow_or_zero (S : BoundingSieve) {N D z : ℕ} {s : ℝ} (hoddEmpty : ¬Even N → ↑z ≤ ↑D ^ (1 / lemma144RealTau D s)) : Lemma144SigmaTwoEvenNarrow N D z s ∨ suzukiSigmaTwo S N D z (↑D ^ (1 / lemma144RealTau D s)) = 0

If source geometry rules out a nonempty upper carrier at odd depth, then with the real τ the actual Σ₂ is either the genuine even narrow branch or zero. No estimate for Σ₂ is assumed here.