A uniform dimension-one constant for the actual progression density. This is only an exact finite-product adapter to the proved Goldbach interval bound. No Mertens estimate is reproved here.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.exists_progressionDensity_dimensionOneProductBound : ∃ (K : ℝ), 1 < K ∧ ∀ (v : ℕ) (P : Finset ℕ), (∀ p ∈ P, Nat.Prime p ∧ 2 < p) → SmallRosser.DimensionOneProductBound P (⇑(progressionDensity v)) K

One constant works simultaneously for every progression parameter and every finite carrier of odd primes. The interval retains its closed left and strict right endpoints.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.exists_progressionOmega_dimensionOneProductBound : ∃ (K : ℝ), 1 < K ∧ ∀ (v : ℕ) (P : Finset ℕ), (∀ p ∈ P, Nat.Prime p ∧ 2 < p) → SmallRosser.DimensionOneProductBound P (⇑(SmallRosser.primeDensity (progressionOmega v))) K

The precise form consumed by exists_externalFamilyDensity_ff.