theorem MathlibNt.SieveTheory.sigmaEleven_add_sigmaTwelve_suzukiVProduct_le_finiteSourceLayer_add_qD_natCeil_closed {S : BoundingSieve} {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} {β C K d Δ s τ σ : ℝ} {N D z : ℕ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatContract H β) (hsdom : s ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain β N) (hτdom : τ - 1 ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain β (N - 1)) (hsτ : s ≤ τ) (hτσ : τ ≤ σ) (hD : 1 < ↑D) (_hz2 : 2 ≤ ↑z) (hroot2 : 2 ≤ ↑D ^ (1 / s)) (hv2 : 2 ≤ ↑D ^ (1 / τ)) (hw2 : 2 ≤ ↑D ^ (1 / σ)) (hwv : ↑D ^ (1 / σ) ≤ ↑D ^ (1 / τ)) (hvroot : ↑D ^ (1 / τ) ≤ ↑D ^ (1 / s)) (hzceil : z = ⌈↑D ^ (1 / s)⌉₊) (hτerr : H.betaHat + (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N).epsilon ≤ τ) (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, ↑D ^ (1 / σ) ≤ ↑p → ↑p < ↑D ^ (1 / τ) → 2 ≤ p ∧ 2 * p ≤ D) (hT : ∀ p ∈ S.prodPrimes.primeFactors, ↑D ^ (1 / σ) ≤ ↑p → ↑p < ↑D ^ (1 / τ) → 0 ≤ H.T (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth (N - 1)) (SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate D p)) (h1413 : ∀ p ∈ S.prodPrimes.primeFactors, ↑D ^ (1 / σ) ≤ ↑p → ↑p < ↑D ^ (1 / τ) → SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_13PointwisePremise H N (↑D) d Δ (Real.log ↑D / Real.log ↑p) (↑D / ↑p)) : SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaEleven (SwitchingPrinciple.suzukiSupportedBelow S z) (⇑S.nu) (fun (p : ℕ) => SwitchingPrinciple.suzukiVProduct S ↑p) (SwitchingPrinciple.suzukiVProduct S ↑z) β N D σ τ + 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 ↑z) C K Δ N D σ τ ≤ SwitchingPrinciple.suzukiVProduct S ↑z * (SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β N s + 6 * K ^ 2 * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β (N - 1) (τ - 1) / Real.log (↑D ^ (1 / σ)) * (τ / s)) + C * Real.exp √K * SwitchingPrinciple.suzukiVProduct S ↑z * 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 (↑D ^ (1 / σ)) * (τ / s))

Closed-endpoint rounded version of the concrete middle provider. The natural ceiling transports the strict carrier exactly, while the Σ₁₂ input allows equality at its lower endpoint.