Chen's theorem

The public theorem is stated in the independent, literal specification from Goldbach.Statement. Its proof supplies the complete sieve and distribution chain and expands the internal almost-prime predicate.

theorem Goldbach.chen_theorem : ChenTheorem

The unconditional prime-plus-at-most-two-primes theorem.

theorem Goldbach.representation_lower_bound : ∀ᶠ (N : ℕ) in Filter.atTop, Even N → 0.67 * MathlibNt.SieveTheory.SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2 ≤ ↑(MathlibNt.SieveTheory.SwitchingPrinciple.chenGoodRepresentations N).card

The number of actual representations has the stated eventual lower bound. liuSingularSeries is the normalization used throughout the sieve assembly.