chen_prime_seventeen
plain-language theorem explainer
The theorem asserts that both 17 and 19 are prime numbers. It would be cited by researchers verifying small Chen primes inside the Recognition Science number-theory layer. The proof proceeds as a direct computational check via native decision procedures.
Claim. $17$ and $19$ are both prime numbers.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Prime is the repo-local alias for Nat.Prime. Upstream results supply collision-free structures and algebraic tautologies from foundation modules that keep the surrounding development free of hidden axioms.
proof idea
The proof is a one-line term wrapper that applies native_decide to evaluate the primality statements directly.
why it matters
The declaration supplies a verified small Chen prime pair that the Recognition Science arithmetic-functions layer can reference. It sits inside the primes module whose Möbius footholds prepare Dirichlet inversion steps. No downstream uses are recorded yet, leaving open whether it will feed later mass-formula or phi-ladder constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.