strong_prime_seventeen
plain-language theorem explainer
Verification that 17 is prime, 13 is prime, and 19 is prime, together with the inequality 17 exceeding their average, establishes a concrete strong-prime instance. Researchers checking specific prime placements on the phi-ladder cite this for anchoring arithmetic calculations in the Recognition Science number-theory layer. The proof is a single native_decide step that reduces the entire conjunction by direct computation.
Claim. The integer 17 is prime, the integer 13 is prime, the integer 19 is prime, and $17 > (13 + 19)/2$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function, while keeping statements minimal until deeper Dirichlet inversion stabilizes. Prime is the transparent alias for the standard natural-number primality predicate. Upstream results supply the basic Prime definition together with structural guarantees from foundation modules that enforce collision-free algebraic consistency across the Recognition Science setup.
proof idea
The proof is a term-mode one-line wrapper that invokes native_decide on the full conjunction, letting the computational evaluator confirm primality of each listed integer and the numerical inequality in a single reduction step.
why it matters
The declaration supplies a verified strong-prime instance at 17 that the module comment flags as RS-relevant. It occupies a slot in the arithmetic-functions file but carries no downstream citations. The result fills a concrete check inside the prime-theory scaffolding without engaging open questions or the Möbius machinery that forms the module's primary focus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.