theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_6_iii_for_sufficiently_large_D_no_extra_premise {H : Section13HatLayers} {β d Δ s σ : ℝ} (hH : Section13HatContract H β) (sign : ErrorSign) (hd : 0 ≤ d) (hΔ : Δ < 1) (hs : β + sign.epsilon ≤ s) (hsσ : s ≤ σ) : ∃ (D₀ : ℝ), 1 < D₀ ∧ ∀ (D : ℝ), D₀ ≤ D → ∫ (t : ℝ) in s..σ, qD H sign.opposite D d Δ t < (1 - 1 / σ) ^ (1 - Δ) * lambda H sign D d 0 s

Claim 14.6(iii), at κ = 1 and on a fixed compact source interval, with no auxiliary distortion or weighted-tail hypothesis. The exponent controlling the limit integrand is 1 - Δ (positive when Δ < 1); this is distinct from the positive exponent in Suzuki's Lemma 13.3.