theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.continuousOn_qD_Icc_of_contract {H : Section13HatLayers} {β D d Δ s σ : ℝ} (hH : Section13HatContract H β) (sign : ErrorSign) (hD : 1 < D) (hs : 1 < s) : ContinuousOn (qD H sign D d Δ) (Set.Icc s σ)

Local continuity of qD, using only the Section 13 contract on the positive axis.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_6_iii_of_lemma13_3_style_bound {H : Section13HatLayers} {β D d Δ θ s σ : ℝ} (hH : Section13HatContract H β) (sign : ErrorSign) (hD : 1 < D) (hσ : 1 < σ) (hs : β + sign.epsilon < s) (hsσ : s ≤ σ) (hDlarge : ∀ t ∈ Set.Icc s σ, (1 + t ^ d / Real.log D) ^ (t - 1) * (t / (t - 1)) ^ Δ ≤ (1 - 1 / σ) ^ (1 - Δ) * (1 + s ^ d / Real.log D) ^ s * (((t - 1) / t) ^ θ * (t / (t - 1)))) (hlemma13_3 : ∫ (t : ℝ) in s..σ, ((t - 1) / t) ^ θ * hatTailIntegrand H sign t < weightedHat H sign s) : ∫ (t : ℝ) in s..σ, qD H sign.opposite D d Δ t < (1 - 1 / σ) ^ (1 - Δ) * lambda H sign D d 0 s

Source-faithful replacement for the invalid closed-interval local reduction. The first premise is the elementary large-D distortion estimate; the second is exactly the finite-interval consequence of the Lemma 13.3 strict weighted-tail bound. Together they imply Claim 14.6(iii) directly.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_6_iii_at_endpoint {H : Section13HatLayers} {β D d Δ σ : ℝ} (hH : Section13HatContract H β) (sign : ErrorSign) (hD : 1 < D) (hσ : 1 < σ) : ∫ (t : ℝ) in σ..σ, qD H sign.opposite D d Δ t < (1 - 1 / σ) ^ (1 - Δ) * lambda H sign D d 0 σ

Although the local predicate fails when s = σ, Claim 14.6(iii) itself is immediate there because its right-hand side is strictly positive.