Lemma 14.4: Σ₀ at the single source endpoint

The low-prime part is first recombined at its one endpoint, exactly in source order. The strict natural-ceiling carrier makes the odd-depth source condition automatic once the exponent is at least three. 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_strict (S : BoundingSieve) {N D z : ℕ} {σ : ℝ} (hN : 2 ≤ N) (hD : 0 < D) (hσ : 3 ≤ σ) (hz : ↑D ^ (1 / σ) ≤ ↑z) : 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. For σ ≥ 3, the natural-ceiling recurrence therefore recombines Σ₀ into one value of suzukiActualT, without a separate odd-depth cube hypothesis.

theorem MathlibNt.SieveTheory.suzukiSigmaZero_sourceSigma_eventually_strict (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 → 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. Eventual growth of sourceSigma supplies the strict natural-ceiling carrier; the endpoint estimate then invokes Claim 14.5 once.