theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3RosserMain_upper_six (ρ : ℝ) (hρ : 0 < ρ) : ∃ (z₀ : ℝ), 2 ≤ z₀ ∧ ∀ (N : ℕ) (hEven : Even N) (ε z Δ s : ℝ), z₀ ≤ z → 0 < Δ → s = Real.log Δ / Real.log z → 3 / 2 ≤ s → s ≤ 6 → ∑ d ∈ (goldbachS1ProdPrimes N z).divisors, LinearSieve.upperRosserWeight (goldbachS1ProdPrimes N z) (⌊Δ⌋₊ + 1) d / ↑d.totient ≤ (suzukiContinuousUpperFactor s + ρ) * AnalyticNumberTheory.Sieve.sieveProductPrimeFactors (goldbachS1BoundingSieve N hEven ε z)

The actual finite S3 Rosser main sum, with the genuine local-product witness supplied internally; the threshold is uniform in every sieve parameter.