Proposition 13.1(iii): quantitative hat-tail decay

Section13HatContract records the DDE, initial values, positivity, and only the qualitative limit weightedHat → 0. The missing publication interface is a quantitative modulus for the adjacent tail ratio. The upstream contract below records the source-strength (M log (eM))⁻² estimate at M; monotonicity from the DDE then compares M with every s ≤ M. Thus this is not the downstream consumer contract (which has already forgotten the logarithmic gain).

def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatAsymptoticContract (H : Section13HatLayers) : Prop

Minimal source-level asymptotic datum: the stronger adjacent-value estimate of Proposition 13.1(iii), retaining its logarithmic gain. It is independent of D, d, Δ, sourceSigma, lambda, and the Claim 14.6 integral.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatAsymptoticContract H = ∃ (C : ℝ), 0 ≤ C ∧ ∀ (sign : MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign) (M : ℝ), 4 ≤ M → MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.weightedHat H sign (M + 2) ≤ C / (M * Real.log (Real.exp 1 * M)) ^ 2 * MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.weightedHat H sign M

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.weightedHat_antitoneOn_Icc_closed {H : Section13HatLayers} (hH : Section13HatContract H 2) (sign : ErrorSign) {s M : ℝ} (hs : 2 + sign.epsilon ≤ s) : AntitoneOn (weightedHat H sign) (Set.Icc s M)

The DDE makes the weighted hat layer antitone even when the left endpoint is exactly the delay threshold. The production strict-endpoint lemma cannot be applied directly there, but its derivative proof works on the interior.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.proposition131_source_strength_tail_decay {H : Section13HatLayers} (hH : Section13HatContract H 2) (hAsymp : Section13HatAsymptoticContract H) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (sign : ErrorSign) (M s : ℝ), 4 ≤ M → 2 + sign.epsilon ≤ s → s ≤ M → weightedHat H sign (M + 2) ≤ C / (M * Real.log (Real.exp 1 * M)) ^ 2 * weightedHat H sign s

Source-strength Proposition 13.1(iii): the adjacent asymptotic estimate plus DDE monotonicity gives the full ratio estimate for every source point s ≤ M.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13HatAsymptoticContract_implies_proposition131TailDecay {H : Section13HatLayers} (hH : Section13HatContract H 2) (hAsymp : Section13HatAsymptoticContract H) : Proposition131TailDecayContract H

Forgetting the logarithmic gain yields exactly the moving proof's Proposition131TailDecayContract.