theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.qDClamp_conditions_of_claim14_6_ii_closed {H : Section13HatLayers} {β D d Δ τ σ : ℝ} (hH : Section13HatContract H β) (sign : ErrorSign) (hD : 1 < D) (hτ : H.betaHat + sign.epsilon ≤ τ) (_hτσ : τ ≤ σ) (hii : Claim14_6_MonotoneQPremise H D d Δ σ) : Continuous (qDClamp H sign.opposite D d Δ τ) ∧ (∀ t ∈ Set.Icc τ σ, 0 ≤ qDClamp H sign.opposite D d Δ τ t) ∧ AntitoneOn (fun (t : ℝ) => qDClamp H sign.opposite D d Δ τ t * t) (Set.Icc τ σ)

Closed-endpoint form of the qD clamp conditions. The only extra case relative to the legacy strict theorem is the lower endpoint itself; continuity extends weighted antitonicity from Ioc to that endpoint.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.lemma8_7_qD_of_claim14_6_ii_closed {S : BoundingSieve} {H : Section13HatLayers} {β D z v w s τ σ K d Δ : ℝ} (sign : ErrorSign) (hH : Section13HatContract H β) (hD : 1 < D) (hz2 : 2 ≤ z) (hv2 : 2 ≤ v) (hw2 : 2 ≤ w) (hwv : w ≤ v) (hvz : v ≤ z) (hz : z = D ^ (1 / s)) (hv : v = D ^ (1 / τ)) (hw : w = D ^ (1 / σ)) (hτ : H.betaHat + sign.epsilon ≤ τ) (hτσ : τ ≤ σ) (hK : 2 ≤ K) (hlocal : HasDimensionOneLocalProductBound S K) (hii : Claim14_6_MonotoneQPremise H D d Δ σ) : suzukiLemmaEightSevenPrimeSum S D w v z (qD H sign.opposite D d Δ) ≤ (1 / s * ∫ (t : ℝ) in τ..σ, qD H sign.opposite D d Δ t) + 6 * K ^ 2 * qD H sign.opposite D d Δ τ / Real.log w * (τ / s)

Lemma 8.7 for qD at the source-faithful closed lower endpoint.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sigma12_middle_le_qD_lemma8_7_closed {S : BoundingSieve} {H : Section13HatLayers} {β D z v w s τ σ K d Δ : ℝ} (sign : ErrorSign) (R : ℝ → ℝ) (hmajorant : ∀ p ∈ S.prodPrimes.primeFactors, w ≤ ↑p → ↑p < v → R (Real.log D / Real.log ↑p) ≤ qD H sign.opposite D d Δ (Real.log D / Real.log ↑p)) (hH : Section13HatContract H β) (hD : 1 < D) (hz2 : 2 ≤ z) (hv2 : 2 ≤ v) (hw2 : 2 ≤ w) (hwv : w ≤ v) (hvz : v ≤ z) (hz : z = D ^ (1 / s)) (hv : v = D ^ (1 / τ)) (hw : w = D ^ (1 / σ)) (hτ : H.betaHat + sign.epsilon ≤ τ) (hτσ : τ ≤ σ) (hK : 2 ≤ K) (hlocal : HasDimensionOneLocalProductBound S K) (hii : Claim14_6_MonotoneQPremise H D d Δ σ) : suzukiLemmaEightSevenPrimeSum S D w v z R ≤ (1 / s * ∫ (t : ℝ) in τ..σ, qD H sign.opposite D d Δ t) + 6 * K ^ 2 * qD H sign.opposite D d Δ τ / Real.log w * (τ / s)

Closed-endpoint Σ₁₂ middle-range assembly.

theorem MathlibNt.SieveTheory.sigmaTwelve_suzukiVProduct_le_qD_lemma8_7_natCeil_closed {S : BoundingSieve} {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} {β C K d Δ w v s τ σ : ℝ} {N D znat : ℕ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatContract H β) (hD : 1 < ↑D) (hv2 : 2 ≤ v) (hw2 : 2 ≤ w) (hwv : w ≤ v) (hvz : v ≤ ↑D ^ (1 / s)) (hz : znat = ⌈↑D ^ (1 / s)⌉₊) (hv : v = ↑D ^ (1 / τ)) (hw : w = ↑D ^ (1 / σ)) (hτ : H.betaHat + (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N).epsilon ≤ τ) (hτσ : τ ≤ σ) (hK : 2 ≤ K) (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) (hii : SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_6_MonotoneQPremise H (↑D) d Δ σ) (hC : 0 ≤ C) (hΔ : 0 ≤ Δ) (hCeil : ∀ p ∈ S.prodPrimes.primeFactors, w ≤ ↑p → ↑p < v → 2 ≤ p ∧ 2 * p ≤ D) (hT : ∀ p ∈ S.prodPrimes.primeFactors, w ≤ ↑p → ↑p < v → 0 ≤ H.T (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth (N - 1)) (SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate D p)) (h1413 : ∀ p ∈ S.prodPrimes.primeFactors, w ≤ ↑p → ↑p < v → SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_13PointwisePremise H N (↑D) d Δ (Real.log ↑D / Real.log ↑p) (↑D / ↑p)) : SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaTwelve S.prodPrimes.primeFactors (⇑S.nu) (fun (p : ℕ) => SwitchingPrinciple.suzukiVProduct S ↑p) (fun (n D' : ℕ) (x : ℝ) => SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H n (↑D') d x) (SwitchingPrinciple.suzukiVProduct S ↑znat) C K Δ N D σ τ ≤ C * Real.exp √K * SwitchingPrinciple.suzukiVProduct S ↑znat * (Real.log ↑D ^ (-Δ) * ((1 / s * ∫ (t : ℝ) in τ..σ, SwitchingPrinciple.SuzukiLemma144KappaOne.qD H (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N).opposite (↑D) d Δ t) + 6 * K ^ 2 * SwitchingPrinciple.SuzukiLemma144KappaOne.qD H (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N).opposite (↑D) d Δ τ / Real.log w * (τ / s)))

Natural-ceiling Σ₁₂ estimate at the closed lower endpoint.