theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbach_upperRosserDensity_six (K ρ : ℝ) : 1 < K → 0 < ρ → ∃ (z₀ : ℝ), ∀ (S : BoundingSieve) (z Δ s : ℝ), z₀ ≤ z → 2 ≤ z → 0 < Δ → SwitchingPrinciple.HasDimensionOneLocalProductBound S K → (∀ p ∈ S.prodPrimes.primeFactors, ↑p ≤ z) → s = Real.log Δ / Real.log z → 3 / 2 ≤ s → s ≤ 6 → BoundingSieve.mainSum (LinearSieve.upperRosserWeight S.prodPrimes (⌊Δ⌋₊ + 1)) ≤ (suzukiContinuousUpperFactor s + ρ) * AnalyticNumberTheory.Sieve.sieveProductPrimeFactors S

The genuine source upper factor bounds the actual upper Rosser main sum uniformly on [3/2,6], with no residual analytic source hypothesis.