theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.exists_goldbachB10BoundingSieve_dimensionOneLocalProductBound : ∃ (K : ℝ), 1 < K ∧ ∀ (N : ℕ) (hEven : Even N) (ε b c Z X : ℝ), SwitchingPrinciple.HasDimensionOneLocalProductBound (goldbachB10BoundingSieve N hEven ε b c Z X) K

A single Mertens constant works for every finite B10 pushforward sieve, because evenness of N removes the exceptional prime 2 from the actual sifting product.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachProdPrimes_upperRosserCertificate {N : ℕ} {Z Δ s : ℝ} (hZ : 2 ≤ Z) (hΔ : 0 < Δ) (hs : s = Real.log Δ / Real.log Z) (hslo : 3 / 2 ≤ s) : LinearSieve.IsUpperRosserCertificate (goldbachB10ProdPrimes N Z) (⌊Δ⌋₊ + 1)

Upper Rosser certification depends only on the shared prime product and logarithmic cutoff, not on the surrounding B8, B10 or linked-sieve weights.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftedCount_le_rosserFactor_add_upperErrSum (ρ : ℝ) (hρ : 0 < ρ) : ∃ (z₀ : ℝ), ∀ (N : ℕ) (hEven : Even N) (ε b c Z Δ s X : ℝ), z₀ ≤ Z → 2 ≤ Z → 0 < Δ → s = Real.log Δ / Real.log Z → 3 / 2 ≤ s → s ≤ 4 → 0 ≤ X → have S := goldbachB10BoundingSieve N hEven ε b c Z X; have P := goldbachB10ProdPrimes N Z; ↑(goldbachB10SiftedCount N ε b c Z) ≤ X * (SwitchingPrinciple.jurkatRichertUpperLinearSieveFactor s + ρ) * AnalyticNumberTheory.Sieve.sieveProductPrimeFactors S + LinearSieve.upperErrSum S (⌊Δ⌋₊ + 1) (LinearSieve.upperRosserWeight P (⌊Δ⌋₊ + 1))

The actual B10 sifted count is bounded by the genuine Jurkat--Richert upper Rosser factor, while retaining the exact finite upper remainder sum.