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)
:
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.