Exact finite bridge from Suzuki densities to BoundingSieve

This module identifies the finite carriers and products used on the Suzuki side with the corresponding Jurkat--Richert BoundingSieve objects. No analytic estimate or limiting argument enters these identities.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.suzukiSupportedBelow_eq_primeFactors_of_all_lt (S : BoundingSieve) {z : ℕ} (hz : ∀ p ∈ S.prodPrimes.primeFactors, p < z) : suzukiSupportedBelow S z = S.prodPrimes.primeFactors

If every supported prime is below the natural cutoff, Suzuki's filtered carrier is exactly the complete prime-factor carrier of the sieve.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.suzukiVProduct_eq_sieveProductPrimeFactors_of_all_lt (S : BoundingSieve) {z : ℝ} (hz : ∀ p ∈ S.prodPrimes.primeFactors, ↑p < z) : suzukiVProduct S z = AnalyticNumberTheory.Sieve.sieveProductPrimeFactors S

Under the corresponding real cutoff hypothesis, Suzuki's V(z) is exactly the Euler product used by BoundingSieve.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.mainSum_lowerRosserWeight_eq_suzukiLowerDensity_of_all_lt (S : BoundingSieve) (D : ℕ) {z : ℕ} (hz : ∀ p ∈ S.prodPrimes.primeFactors, p < z) : BoundingSieve.mainSum (LinearSieve.lowerRosserWeight S.prodPrimes D) = LinearSieve.lowerRosserSetDensitySum (⇑S.nu) D (suzukiSupportedBelow S z)

The existing divisor/powerset identity for lower Rosser weights, transported to Suzuki's supported-below carrier.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.suzukiDensityProduct_lowerRosserWeight_exact_bridge (S : BoundingSieve) (D z : ℕ) (hz : ∀ p ∈ S.prodPrimes.primeFactors, p < z) (hD : ∀ p ∈ S.prodPrimes.primeFactors, p < D) : BoundingSieve.mainSum (LinearSieve.lowerRosserWeight S.prodPrimes D) = LinearSieve.lowerRosserSetDensitySum (⇑S.nu) D (suzukiSupportedBelow S z) ∧ suzukiVProduct S ↑z = AnalyticNumberTheory.Sieve.sieveProductPrimeFactors S ∧ LinearSieve.IsLowerRosserCertificate S.prodPrimes D

Production bundle: when all prime factors lie both below Suzuki's cutoff and below the Rosser level, the Suzuki density and Euler product are literally the BoundingSieve main sum and sieve product, and the same finite coefficient has the required lower-Möbius certificate.