theorem MathlibNt.SieveTheory.HasDimensionOneLocalProductBound.mono {S : BoundingSieve} {K K' : ℝ} (h : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) (hKK' : K ≤ K') : SwitchingPrinciple.HasDimensionOneLocalProductBound S K'

The dimension-one local-product estimate is monotone in its scalar constant.

theorem MathlibNt.SieveTheory.real_level_to_natCeil_geometry {z Δ s : ℝ} (hz : 2 ≤ z) (hΔ : 0 < Δ) (hs : s = Real.log Δ / Real.log z) (hslo : 3 / 2 ≤ s) : have D := ⌊Δ⌋₊ + 1; 2 ≤ D ∧ Δ < ↑D ∧ z < ↑D ^ (1 / s) ∧ 2 ≤ ⌈↑D ^ (1 / s)⌉₊

Real endpoint geometry for the natural ceiling used by the all-depth Suzuki producer. In particular, every prime at most the requested real cutoff is strictly below the rounded Suzuki cutoff.

theorem MathlibNt.SieveTheory.dimensionOneUpperRosserDensityFundamentalLemma_of_suzuki_allDepth (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d δ Θ : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hsrc : SuzukiClaim145SourceParameters d δ Θ) : SwitchingPrinciple.DimensionOneUpperRosserDensityFundamentalLemma

Direct all-depth closure of the production upper Rosser density endpoint. The constants in the all-depth estimate are selected before S; the adaptive odd depth is chosen only inside the natural-ceiling consumer. The production exact finite Rosser/Suzuki bridge is consumed unconditionally, with no residual bridge or ordered-tail premise.