chen_prime_five
plain-language theorem explainer
Both 5 and 7 are prime numbers. Number theorists working on Chen primes would cite this as the base case establishing that 5 + 2 yields a prime. The proof executes as a single native_decide call that resolves the primality predicates directly.
Claim. Both $5$ and $7$ are prime numbers.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function, while keeping statements minimal until Dirichlet algebra stabilizes. Prime is the repo-local transparent alias for the standard primality predicate on natural numbers. The local setting is the primes subsection of arithmetic functions, providing concrete instances without deeper inversion machinery.
proof idea
The proof is a term-mode one-liner that applies the native_decide tactic to evaluate the conjunction of the two primality statements.
why it matters
This supplies a verified small-case primality fact supporting Chen prime constructions inside the Recognition Science number theory layer. No downstream uses are recorded. It fills a concrete base instance in the primes section without engaging the full Möbius or forcing-chain apparatus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.