Suzuki Claim 14.5, Case A: the low-s source branch #
For κ = κ̂ = 1 and β = 2, Suzuki applies Lemma 14.3 and the factorial
estimate used in (14.7), first obtaining
L^M / M! * exp L ≤ exp (-s log s + s log log (3K) + O (log K + s)).
The uniform target below is exactly that first big-O step. It precedes the subsequent comparison with
exp (-s log s - s log log (3s) + sqrt K / 2)
and therefore must be discharged before the latter comparison can be used. No Claim-14.5 conclusion is assumed here.
The first missing scalar inequality in Claim 14.5, Case A, low-s range.
A is the absolute big-O coefficient and K₀ is the source choice that K is
sufficiently large. The quantifiers are uniform in K, D, the natural
ceiling cutoff, and s; in particular this is not a finite-D maximum or an
eventual-D statement.
Equations
- MathlibNt.SieveTheory.Claim145CaseALowSBigOScalarTarget C1 ΘK = ∃ (A : ℝ) (K₀ : ℝ), 0 ≤ A ∧ 2 ≤ K₀ ∧ ∀ (D z : ℕ) (K s : ℝ), K₀ ≤ K → 2 ≤ D → z = ⌈↑D ^ (1 / s)⌉₊ → 2 ≤ s → s ≤ √K / Real.log K → Real.log ↑D ≤ C1 * K ^ ΘK → MathlibNt.SieveTheory.suzukiSourceL (↑z) K ^ (⌊s - 2⌋₊ + 1) / ↑(⌊s - 2⌋₊ + 1).factorial * Real.exp (MathlibNt.SieveTheory.suzukiSourceL (↑z) K) ≤ Real.exp (-s * Real.log s + s * Real.log (Real.log (3 * K)) + A * (Real.log K + s))
Instances For
Suzuki (14.7), with the factorial estimated by the elementary Stirling lower
bound, gives the first scalar big-O target in the low-s branch.
Lemma 14.3 reaches the left side of the frozen low-s scalar target with
no dependence on the depth N.
Proposition 13.1(ii) supplies the lower side of (14.6), uniformly in the
parity/depth. This is the target-scale edge used after the two scalar
exponential comparisons in Suzuki's low-s branch.
Final pointwise assembly of the high-s half of Claim 14.5, Case A.
The two hypotheses hsourceLarge and hexponent are the explicit large-K
threshold hidden in the first O(log K + s) on pp. 82--83. The hypothesis
habsorb is the second, final O(s) absorption (including all harmless Euler
and logarithmic prefactors). They are deliberately exposed: the source only
asserts the result after choosing K sufficiently large, and replacing them by
a finite-D maximum or compactness would not formalize that assertion.
Everything between these threshold inequalities is closed here: Lemma 14.3,
the already proved high-coordinate logarithmic gain, the production lower form
of (14.6), and the literal Claim14_5Bound.
Source-contract form of the preceding assembly. It chooses the uniform
Proposition-13.1(ii) constants supplied by (14.6); once the displayed source
large-K thresholds hold for those constants, the conclusion is the final
Claim-14.5 bound, not an intermediate scalar comparison.
Suzuki's second displayed comparison in Case A, uniformly throughout
2 ≤ s ≤ √K / log K. Above one source threshold the multiplicative constant
can in fact be chosen to be one.