chen_prime_thirteen
plain-language theorem explainer
The declaration verifies that 13 is prime while 15 factors as 3 times 5, confirming 13 as a Chen prime. Number theorists building arithmetic examples for Recognition Science would reference this concrete case. The proof is a one-line native decision procedure that directly evaluates the conjunction.
Claim. $13$ is a prime number and $15$ is a semiprime number, meaning the total number of its prime factors counted with multiplicity equals two.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, starting with the Möbius function and extending to semiprimality. Prime is the transparent alias for the standard primality predicate on natural numbers. isSemiprime is defined via the equality bigOmega n = 2, where bigOmega counts prime factors with multiplicity. The upstream definition states: 'A number is semiprime if Ω(n) = 2.'
proof idea
The proof is a one-line term that applies native_decide to evaluate the conjunction of the primality predicate on 13 and the semiprimality predicate on 15.
why it matters
This supplies a concrete Chen prime instance inside the primes arithmetic module, as the declaration comment explicitly links the semiprime check to RS-relevance. It contributes to the lightweight number-theoretic scaffolding that may later support Dirichlet inversion or prime-gap statements, though no downstream theorems currently depend on it. The result remains isolated from the core forcing chain and phi-ladder constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.