Claim 14.5, source-small-D high-coordinate branch #
Suzuki's Case A assumes 2 ≤ s and log D ≤ C₁ K^ΘK; it then applies
Lemma 14.3 and compares that explicit exponential-tail majorant with (14.6).
The definitions below retain those exact inputs. In particular, no
Claim14_5Bound or final Lemma-14.4 estimate is accepted as a premise.
The scalar comparison in Suzuki Claim 14.5, Case A, after Lemma 14.3. The source-small-D condition is an argument of the comparison rather than being silently replaced by an arbitrary finite-cutoff condition.
Equations
- MathlibNt.SieveTheory.Claim145SmallDCaseAScalarComparison S H d Δ C145 K C1 ΘK = ∀ (n q p : ℕ) (x : ℝ), 2 ≤ q → p = ⌈↑q ^ (1 / x)⌉₊ → 2 ≤ x → Real.log ↑q ≤ C1 * K ^ ΘK → MathlibNt.SieveTheory.suzukiSourceL (↑p) K ^ (⌊x - 2⌋₊ + 1) / ↑(⌊x - 2⌋₊ + 1).factorial * Real.exp (MathlibNt.SieveTheory.suzukiSourceL (↑p) K) ≤ C145 * MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_5Scale S H n (↑q) d Δ (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑q) d) K x
Instances For
The actual Claim14_5Bound in the source-small-D alternative follows from
production Lemma 14.3 and the Case-A scalar comparison.
The moving source cutoff is positive already for every natural q ≥ 2;
no eventual threshold is needed in the finite quotient branch.
The logarithmic side condition used below is not valid for every K > 1,
but it is uniform on the source high-coordinate region once K crosses a fixed
threshold. This isolates exactly the small-K split hidden by ≪: log K is
positive for K > 1, and log log K = o(log K) gives, eventually,
log K ≤ 4 log s for every s ≥ √K / log K.
The first ≪ in Suzuki Claim 14.5, Case A, high-s branch, with
the implicit constant made explicit. Positivity of log K is exactly 1 < K;
log K ≤ 4 log s is the large-K threshold consequence used to square
s ≥ √K / log K. The result is the literal
log D ≪ K^Θ ≪ s^(2Θ) (log s)^(2Θ) chain.
The decisive logarithmic gain in the same source branch. The displayed
hgrowth is the exact threshold inequality hidden by the source O(1); under
it the error can be taken to be zero. No compactness or finite-quotient
maximum is used.
Equation (14.3), namely d - 2Θ > 0, supplies the omitted threshold:
the logarithmic factor in the preceding theorem is eventually dominated by
s^(d-2Θ). This is the source route, via the standard
(log s)^a = o(s^b) estimate, rather than a finite-q maximum.
The complete analytic chain on the source high-s side of Case A. After
one source threshold in s, the hypotheses s ≥ √K/log K and
log K ≤ 4 log s turn the small-D alternative into the logarithmic gain
used between Lemma 14.3 and (14.6). The latter two production interfaces are
then connected by claim14_5Bound_of_smallD_caseA_scalarComparison above.
The statement deliberately retains the threshold relation instead of replacing
it by compactness or a maximum over finitely many quotients.
Scalar normalization from the Claim-14.5 V(q) scale to the predecessor
V(p) error envelope. The only numerical input is the exposed coefficient
inequality C145 ≤ C log(q) σ(q); Euler monotonicity and positivity are proved
here.