1 The public proof boundary

Chen’s theorem asserts that every sufficiently large even natural number is a prime plus either a prime or a product of two primes. The proof establishes the existence of a threshold with this property.

This blueprint shows seven selected declarations and six displayed edges inferred by LeanArchitect from the compiled endpoint declarations. The first three input nodes form the boundary of the displayed graph; each retains its complete upstream dependencies in Lean. Prose summaries and links to exact Lean statements accompany the nodes. The existence and quantitative endpoints use separate implementation declarations with a shared proved distribution input.

1.1 Distribution and conditional assembly

Theorem 1 Proved Liu-Pan distribution input

✓

The canonical coprime switched-source distribution estimate holds with all analytic inputs supplied.

Proof ▼

Theorem 2 Conditional representation bound

✓

The canonical Liu-Pan input supplies the triple penalty estimate required for the eventual representation lower bound.

Proof ▼

Theorem 3 Conditional Chen assembly

✓

The proved weighted lower sieve and canonical Liu-Pan input yield the prime-plus-at-most-two-primes conclusion.

Proof ▼

1.2 Unconditional endpoints

Theorem 4 Unconditional representation bound

✓

Supplying the proved distribution input discharges the remaining premise of the quantitative assembly.

Proof ▼

Theorem 5 Unconditional Chen endpoint

✓

Supplying the proved distribution input discharges the remaining premise of the qualitative assembly.

Proof ▼

1.3 Public results

Theorem 6 Public representation lower bound

✓

For sufficiently large even natural numbers, the actual representation count has lower bound \(0.67\) times the normalized singular series scale \(N / (\log N)^2\).

Proof ▼

Theorem 7 Chen’s theorem

✓

Every sufficiently large even natural number is the sum of a prime and either a prime or a product of two primes. The two factors may be equal.

Proof ▼