theorem MathlibNt.SieveTheory.exists_sourceSigma_one_threshold (d : ℝ) (hd : 0 < d) : ∃ (D0 : ℝ), 1 < D0 ∧ ∀ (D : ℝ), D0 ≤ D → 1 ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d

Beyond an explicit fixed threshold, Suzuki's moving source cutoff is at least one.

theorem MathlibNt.SieveTheory.exists_caseII_endpoint_common_threshold (N : ℕ) (K C d Δ : ℝ) (hF0 : 0 ≤ SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 N 3) (hF1 : 0 ≤ SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (N - 1) 2) (hK : 0 ≤ K) (_hC : 0 ≤ C) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hd : 7 / (1 - Δ) < d) : ∃ (D0 : ℝ), 1 < D0 ∧ ∀ (D : ℝ), D0 ≤ D → caseIISharpPositiveEndpointRelativeCoeff N D d Δ (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d) C K ≤ 4 * ((1 - Δ) / (32 * SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d))

The four positive Case-II endpoint coefficients admit one unconditional large-D threshold after substituting Suzuki's source cutoff. The coefficients a₀, a₁, and aq₀ are fixed by N,K,C,d,Δ; all of the moving D dependence is displayed in the four summands.