chen_prime_two
plain-language theorem explainer
The declaration verifies that 2 is a Chen prime because 2 is prime and 4 equals 2 squared, hence semiprime. Number theorists examining prime pairs or Chen's theorem on bounded gaps would cite this as the explicit base case. The proof reduces to a single native decision procedure that evaluates the primality and big-Omega conditions directly.
Claim. $2$ is prime and $4$ is semiprime, where semiprime means the total number of prime factors counted with multiplicity equals two.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and extending to semiprimality checks via big-Omega. Prime is the repo-local alias for the standard primality predicate on natural numbers. isSemiprime n holds precisely when bigOmega n equals 2, as defined in the sibling declaration that records the two-prime-factor condition for 4.
proof idea
The proof is a one-line wrapper that applies native_decide to the conjunction of Prime 2 and isSemiprime 4.
why it matters
This supplies the initial Chen-prime instance inside the arithmetic-functions module. It anchors the primes section without feeding any listed downstream theorems and remains separate from the forcing chain, recognition composition law, or phi-ladder constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.