theorem
MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.exists_goldbachComposite_dimensionOne_constant :
∃ (K : ℝ),
2 ≤ K ∧ ∀ (N : ℕ) (hEven : Even N) (ε z : ℝ) (m : ℕ),
SwitchingPrinciple.HasDimensionOneLocalProductBound (goldbachS3BoundingSieve N hEven ε z m) K
One dimension-one constant works for every actual composite-conditioned Goldbach sieve, before N, epsilon, the sieve cutoff, and the outer modulus.
Inspect dependencies
MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.exists_goldbachComposite_dimensionOne_constant · compiled type and proof/definition references.