theorem MathlibNt.SieveTheory.LiLiuPrereqWF.g9Density_exists_uniform_dimension_one : ∃ (K : ℝ), 1 < K ∧ ∀ (P : Finset ℕ), (∀ p ∈ P, Nat.Prime p ∧ 2 < p) → ∀ (g : ℕ → ℝ), (∀ p ∈ P, g p ≤ 1 / (↑p - 1)) → SmallRosser.DimensionOneProductBound P g K

One existing Mertens constant works uniformly for every finite odd-prime carrier and every local density dominated by the Goldbach local density. Removing factors for primes dividing the changing product does not change K.