Chen's 1+2 endpoint after the verified sieve and distribution inputs

The Jurkat--Richert weighted lower bound already pays the valuation-weighted prime-power penalty. Only the genuine triple upper bound remains conditional. The Liu--Pan specialization below uses the existing Selberg-square-to-triple producer, including its endpoint and paper-modulus corrections.

These are conditional Chen theorems, not unconditional analytic producers. The quantitative statement counts the existing chenGoodRepresentations; neither the historical counting bridge nor a weakened counting object is used.

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

The original public representation count has coefficient 0.67, conditional only on the actual triple penalty estimate. All sieve and BV inputs are internal.

theorem MathlibNt.SieveTheory.ChenVerifiedPrerequisites.chens_theorem_of_triple_penalty (hTriple : SwitchingPrinciple.ChenJurkatRichertTriplePenaltyUpperBound) : ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Even N → ∃ (p : ℕ) (q : ℕ), Nat.Prime p ∧ ChensTheorem.Semiprime q ∧ N = p + q

The existing prime-plus-at-most-two-primes endpoint with only the triple upper bound explicit; the verified Richert certificate supplies the lower bound.

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

The canonical switched-source theorem supplies the sole remaining triple estimate, preserving the full public 0.67 count.

theorem MathlibNt.SieveTheory.ChenVerifiedPrerequisites.chens_theorem_of_liu_coprime (hLiu : LiuWeight.LiuPanCanonicalCoprimeTheorem) : ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Even N → ∃ (p : ℕ) (q : ℕ), Nat.Prime p ∧ ChensTheorem.Semiprime q ∧ N = p + q

The actual existing public Chen assembly with every sieve and BV premise discharged. The canonical Liu switched-source bound is still an explicit input.

theorem MathlibNt.SieveTheory.ChenVerifiedPrerequisites.chens_theorem_of_corollary230 (hPan : LiuWeight.LiuPanWangDingCorollary230) : ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Even N → ∃ (p : ℕ) (q : ℕ), Nat.Prime p ∧ ChensTheorem.Semiprime q ∧ N = p + q

The existing source-interval and logarithmic-integral normalization transport connects Corollary (2.30) without any new analytic assumption.