Prime-plus-at-most-two-primes representation vocabulary

This foundational module defines the second-summand predicate and proves its literal characterization. It does not import any sieve implementation. The unconditional theorem is exposed by Goldbach.

The retained internal name Semiprime means at most two prime factors here; Mathlib's Nat.IsSemiprime means exactly two. The public theorem avoids that terminological ambiguity by stating the disjunction explicitly.

def MathlibNt.ChensTheorem.Semiprime (n : ℕ) : Prop

An integer at least two with at most two prime factors, counted with multiplicity.

Equations

• MathlibNt.ChensTheorem.Semiprime n = (n ≥ 2 ∧ Nat.IsAtMostAlmostPrime 2 n)

theorem MathlibNt.ChensTheorem.prime_semiprime {p : ℕ} (hp : Nat.Prime p) : Semiprime p

A prime has at most two prime factors.

theorem MathlibNt.ChensTheorem.mul_prime_semiprime {p₁ p₂ : ℕ} (hp₁ : Nat.Prime p₁) (hp₂ : Nat.Prime p₂) : Semiprime (p₁ * p₂)

A product of two primes has at most two prime factors; equal factors are allowed.

theorem MathlibNt.ChensTheorem.semiprime_iff {n : ℕ} : Semiprime n ↔ Nat.Prime n ∨ ∃ (p₁ : ℕ) (p₂ : ℕ), Nat.Prime p₁ ∧ Nat.Prime p₂ ∧ n = p₁ * p₂

The internal predicate is exactly a prime or a product of two primes.

theorem MathlibNt.ChensTheorem.semiprime_ge_two {n : ℕ} (h : Semiprime n) : n ≥ 2

The internal predicate excludes zero and one.

theorem MathlibNt.ChensTheorem.isSemiprime_implies_semiprime {n : ℕ} (h : n.IsSemiprime) : Semiprime n

Mathlib's exactly-two-factor predicate implies the at-most-two-factor predicate.