theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_6_i_ii_for_sufficiently_large_D {H : Section13HatLayers} {β d Δ σ : ℝ} (hH : Section13HatContract H β) (hd : 0 ≤ d) (hΔ : -1 < Δ) (hσ : ∀ (sign : ErrorSign), β + sign.epsilon ≤ σ) : ∃ (D₀ : ℝ), 1 < D₀ ∧ ∀ (D : ℝ), D₀ ≤ D → (∀ (sign : ErrorSign) (ε : ℝ), ε = 0 ∨ ε = 1 → AntitoneOn (lambda H sign D d ε) (Set.Icc (β + sign.epsilon) σ)) ∧ Claim14_6_MonotoneQPremise H D d Δ σ

Claims 14.6(i) and (ii), simultaneously and with no externally supplied margin: under the source range condition -1 < Δ, both conclusions hold for all sufficiently large D.