Lemma 14.4: Σ₀ at the single source endpoint

The low-prime part is first recombined at its one endpoint, exactly in source order. Claim 14.5 is then applied once to the resulting T_N; no prime-dependent threshold or uniformity premise is used.

theorem MathlibNt.SieveTheory.suzukiSigmaZero_eq_actualT_single_endpoint (S : BoundingSieve) {N D z : ℕ} {σ : ℝ} (hN : 2 ≤ N) (hz : ↑D ^ (1 / σ) ≤ ↑z) (hOddBoundary : Odd N → ⌈↑D ^ (1 / σ)⌉₊ ^ 3 ≤ D) : suzukiSigmaZero S N D z (↑D ^ (1 / σ)) = suzukiActualT S N D ⌈↑D ^ (1 / σ)⌉₊

At a single real endpoint D^(1/σ), the strict low-prime carrier is exactly the support below its natural ceiling. The actual Case-I recurrence therefore recombines Σ₀ into one value of suzukiActualT.

theorem MathlibNt.SieveTheory.suzukiSigmaZero_sourceSigma_eventually (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d Δ K C145 : ℝ} (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hd : 7 / (1 - Δ) < d) (hK : 0 < K) (hC145 : 0 < C145) (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) : ∃ (D₀ : ℝ), 1 < D₀ ∧ ∀ (D N z : ℕ), D₀ ≤ ↑D → 2 ≤ N → ↑D ^ (1 / SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) ≤ ↑z → (Odd N → ⌈↑D ^ (1 / SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d)⌉₊ ^ 3 ≤ D) → suzukiSigmaZero S N D z (↑D ^ (1 / SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d)) ≤ C145 * SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_5Scale S H N (↑D) d Δ (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) K (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d)

Eventual Σ₀ bound in source order: first use the exact single-endpoint recombination, then invoke Claim 14.5 once at sourceSigma D d.