theorem MathlibNt.SieveTheory.errorEnvelope_odd_le_sixteen_on_upper_window (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatContract H 2) {N : ℕ} (hN : Odd N) {D d s : ℝ} (hd : 0 ≤ d) (hD : 1 < D) (hlog : 4 ^ d ≤ Real.log D) (hslo : 3 / 2 ≤ s) (hshi : s ≤ 4) : SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N D d s ≤ 16

On the compact upper-sieve window the odd Suzuki error envelope has a bound independent of the (possibly carrier-adaptive) depth.

theorem MathlibNt.SieveTheory.eventually_all_odd_depth_suzuki_error_upper_window (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatContract H 2) {C K d Δ ρ : ℝ} (hC : 0 ≤ C) (hd : 0 ≤ d) (hΔ : 0 < Δ) (hρ : 0 < ρ) : ∀ᶠ (D : ℝ) in Filter.atTop, ∀ (N : ℕ), Odd N → ∀ (s : ℝ), 3 / 2 ≤ s → s ≤ 4 → 0 ≤ C * Real.exp √K * SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N D d s * Real.log D ^ (-Δ) ∧ C * Real.exp √K * SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N D d s * Real.log D ^ (-Δ) < ρ

Uniform scalar absorption on [3/2,4], simultaneously for every odd adaptive depth. The depth enters the literal error only through its parity.

theorem MathlibNt.SieveTheory.finiteSourceLayer_two_mul_add_one_eq_sum_oddLayers (m : ℕ) (s : ℝ) : SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (2 * m + 1) s = ∑ k ∈ Finset.range (m + 1), SuzukiFiniteContinuousLayers.suzukiLayer 1 2 (2 * k + 1) s

Odd finite source layers are exactly the initial segment used by Suzuki's continuous upper source factor.

theorem MathlibNt.SieveTheory.finiteSourceLayer_odd_le_suzukiContinuousUpperFactor_sub_one (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (m : ℕ) {s : ℝ} (hs : 1 < s) : SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (2 * m + 1) s ≤ suzukiContinuousUpperFactor s - 1

Every carrier-adaptive odd finite source factor lies below the genuine continuous upper source factor.

theorem MathlibNt.SieveTheory.upperRosserDensity_at_natCeil_of_allDepth (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (S : BoundingSieve) {C K d Δ : ℝ} (hall : ∀ (N : ℕ), 1 ≤ N → Lemma144MovingDomainNatCeilAt S H C K d Δ N 2) (D : ℕ) (s : ℝ) (hD : 2 ≤ D) (hslo : 3 / 2 ≤ s) (_hshi : s ≤ 4) (hsSigma : s ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) (hz2 : 2 ≤ ⌈↑D ^ (1 / s)⌉₊) (hcut : ∀ p ∈ S.prodPrimes.primeFactors, p < ⌈↑D ^ (1 / s)⌉₊) : BoundingSieve.mainSum (LinearSieve.upperRosserWeight S.prodPrimes D) ≤ AnalyticNumberTheory.Sieve.sieveProductPrimeFactors S * (suzukiContinuousUpperFactor s + C * Real.exp √K * SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H (2 * S.prodPrimes.primeFactors.card + 1) (↑D) d s * Real.log ↑D ^ (-Δ))

Complete direct consumer at a natural Suzuki coordinate. The exact finite upper-Rosser/Suzuki bridge is invoked internally; no bridge premise or uniform ordered-layer tail is assumed.

theorem MathlibNt.SieveTheory.exists_upperRosserDensity_at_natCeil_of_suzuki_allDepth (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d Δ Θ : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hsrc : SuzukiClaim145SourceParameters d Δ Θ) : ∃ (C1min : ℝ), 0 < C1min ∧ ∀ (C1 : ℝ), C1min ≤ C1 → ∃ (C145 : ℝ) (Clow : ℝ) (C : ℝ), 0 < C145 ∧ 0 ≤ Clow ∧ 3 ≤ C ∧ ∀ (S : BoundingSieve) (K : ℝ), 2 ≤ K → SwitchingPrinciple.HasDimensionOneLocalProductBound S K → ∀ (D : ℕ), 2 ≤ D → ∀ (s : ℝ), 3 / 2 ≤ s → s ≤ 4 → s ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d → 2 ≤ ⌈↑D ^ (1 / s)⌉₊ → (∀ p ∈ S.prodPrimes.primeFactors, p < ⌈↑D ^ (1 / s)⌉₊) → BoundingSieve.mainSum (LinearSieve.upperRosserWeight S.prodPrimes D) ≤ AnalyticNumberTheory.Sieve.sieveProductPrimeFactors S * (suzukiContinuousUpperFactor s + C * Real.exp √K * SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H (2 * S.prodPrimes.primeFactors.card + 1) (↑D) d s * Real.log ↑D ^ (-Δ))

Production wrapper: the all-depth Suzuki producer feeds the direct odd-depth consumer with constants selected before the bounding sieve. The exact bridge is a proved internal dependency, not a proposition-valued premise.