theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.integral_hatTailIntegrand_closedThreshold {H : Section13HatLayers} {β a b : ℝ} (hH : Section13HatContract H β) (sign : ErrorSign) (ha : β + sign.epsilon ≤ a) (hab : a ≤ b) : ∫ (t : ℝ) in a..b, hatTailIntegrand H sign t = weightedHat H sign a - weightedHat H sign b

Finite DDE identity valid also at the closed threshold. The production identity asks for a strict lower-bound hypothesis only because it differentiates at the left endpoint; the FTC needs the DDE only in the open interval.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.lemma13_3_weightedTail_strict_closedRange {H : Section13HatLayers} {β θ s σ : ℝ} (hH : Section13HatContract H β) (sign : ErrorSign) (hθ : 0 ≤ θ) (hs : β + sign.epsilon ≤ s) (hsσ : s ≤ σ) : ∫ (t : ℝ) in s..σ, ((t - 1) / t) ^ θ * hatTailIntegrand H sign t < weightedHat H sign s

Exact κ=1 finite weighted-tail bound required by Claim 14.6(iii). It holds on the full source range β + ε_sign ≤ s ≤ σ. The source's κ=1 condition 0 < θ is more than needed here: 0 ≤ θ suffices because truncation at finite σ leaves the strictly positive value weightedHat H sign σ. The degenerate endpoint s = σ is split off explicitly.