Unconditional Chen 1+2, using the proved Liu--Pan distribution source and the existing verified Jurkat--Richert / Selberg counting assembly. This file makes no claim about the separate 1+1.9 contract.

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

The original public good-representation count, with all analytic inputs supplied.

theorem MathlibNt.ChensTheorem.chens_theorem_unconditional : ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Even N → ∃ (p : ℕ) (q : ℕ), Nat.Prime p ∧ Semiprime q ∧ N = p + q

Every sufficiently large even natural is a prime plus a number at least two with at most two prime factors, counted with multiplicity. No hypothesis parameter.