Tail of Suzuki's genuine upper source #
The two nonnegative parity source tails are dominated by their sum Q, whose
exponential decay was already obtained from the Section 13 source contract.
Consequently the genuine upper source tends to 2.
The genuine source sum Q=T⁺+T⁻ tends to zero.
Inspect dependencies
MathlibNt.SieveTheory.tendsto_suzukiProposition118SourceQ_zero · compiled type and proof/definition references.
Each parity source tail tends to zero separately.
Inspect dependencies
MathlibNt.SieveTheory.tendsto_suzukiProposition118Source_parity_zero · compiled type and proof/definition references.
The genuine upper source satisfies its forward integral DDE on every
2 ≤ x ≤ y, including both the switching endpoint and intervals crossing
s=3.
Inspect dependencies
MathlibNt.SieveTheory.suzukiUpperSourceP_weighted_sub · compiled type and proof/definition references.
Closed production integral-DDE package for the genuine upper source.
Inspect dependencies
MathlibNt.SieveTheory.suzukiUpperSourceP_integralDDE_of_sourceContract · compiled type and proof/definition references.
The actual upper source tends to its Proposition 11.8 terminal value 2.
Inspect dependencies
MathlibNt.SieveTheory.suzukiUpperSourceP_tail_of_sourceContract · compiled type and proof/definition references.
The genuine moving-window tail follows without any additional analytic premise.
Inspect dependencies
MathlibNt.SieveTheory.suzukiUpperSourcePairingWindowTail_of_sourceContract · compiled type and proof/definition references.
The Section-13 source contract now supplies every source-side input to the
upper pairing, so the pairing is identically 2 on its legal range.
Inspect dependencies
MathlibNt.SieveTheory.suzukiUpperSourcePairing_eq_two_of_sourceContract · compiled type and proof/definition references.
Final amplitude normalization for Suzuki's genuine production source.
Inspect dependencies
MathlibNt.SieveTheory.suzukiLowerSieveAmplitude_eq_two_mul_exp_eulerMascheroni_of_sourceContract · compiled type and proof/definition references.
On 4 ≤ s ≤ 6, the normalized source formula is exactly the standard
Jurkat--Richert dimension-one lower sieve factor.
Inspect dependencies
MathlibNt.SieveTheory.suzukiContinuousLowerFactor_eq_dimensionOne_of_sourceContract · compiled type and proof/definition references.