def MathlibNt.SieveTheory.UpperRosserSuzukiExactBridge : Prop

The exact finite upper-Rosser/Suzuki bridge. The integer z exhausts the finite prime support, while every supported prime lies below the Rosser level. No local-product hypothesis or approximation occurs in this interface.

Equations

• MathlibNt.SieveTheory.UpperRosserSuzukiExactBridge = ∀ (S : BoundingSieve) (D z : ℕ), 1 < D → (∀ p ∈ S.prodPrimes.primeFactors, p < D) → (∀ p ∈ S.prodPrimes.primeFactors, p < z) → BoundingSieve.mainSum (MathlibNt.SieveTheory.LinearSieve.upperRosserWeight S.prodPrimes D) ≤ AnalyticNumberTheory.Sieve.sieveProductPrimeFactors S + MathlibNt.SieveTheory.suzukiActualT S (2 * S.prodPrimes.primeFactors.card + 1) D z

theorem MathlibNt.SieveTheory.mainSum_upperRosserWeight_eq_sieveProduct_add_suzukiActualT (S : BoundingSieve) (D z : ℕ) (hD : 1 < D) (hlevel : ∀ p ∈ S.prodPrimes.primeFactors, p < D) (hz : ∀ p ∈ S.prodPrimes.primeFactors, p < z) : BoundingSieve.mainSum (LinearSieve.upperRosserWeight S.prodPrimes D) = AnalyticNumberTheory.Sieve.sieveProductPrimeFactors S + suzukiActualT S (2 * S.prodPrimes.primeFactors.card + 1) D z

Exact equality behind UpperRosserSuzukiExactBridge: after restoring the full Euler product, each relative boundary path becomes its terminal nu(q) * sourceDiscreteEuler(q) times the selected-chain density. The common finite depth range is then exactly the odd Suzuki aggregate.

theorem MathlibNt.SieveTheory.upperRosserSuzukiExactBridge : UpperRosserSuzukiExactBridge

The finite exact bridge is inhabited unconditionally from the defining upper-Rosser path expansion and Suzuki's odd-layer identity.