Case I: source-faithful uniform scalar cutoff #
This proves the literal (14.23) scalar estimate uniformly in K directly
from Suzuki's parameter packet. It uses the exact source margin
2 / Θ + 3 / d < 1 - Δ; in particular it does not replace Δ by
Δ + 2 / Θ in the older sufficient condition 7 / (1 - Δ) < d.
theorem
MathlibNt.SieveTheory.exists_caseI1423_sourceScalar_sourceLargeLog_uniform_of_source
{d Δ Θ : ℝ}
(hsrc : SuzukiClaim145SourceParameters d Δ Θ)
:
∃ (C1min : ℝ),
1 ≤ C1min ∧ ∀ (C1 K D : ℝ),
C1min ≤ C1 →
2 ≤ K →
2 ≤ D →
C1 * K ^ Θ < Real.log D →
K ^ 2 * SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d ^ 3 * Real.log (Real.exp 1 * SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d) * Real.log (Real.log D) / Real.log D ^ (1 - Δ) ≤ 1
Under the source parameter packet, the literal Case-I (14.23) scalar has
one cutoff in the separator C1, chosen before arbitrary K and D.