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