superprime_seventeen
plain-language theorem explainer
17 and 7 are both prime. Number theorists working with arithmetic functions in Recognition Science cite this to anchor Möbius-function calculations on small primes. The proof is a one-line term proof that invokes native_decide to settle the conjunction computationally.
Claim. $17$ is prime and $7$ is prime, where primality is the standard predicate on natural numbers.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The local setting is a collection of basic interfaces that later support Dirichlet inversion and prime-related identities. Upstream, Prime is the transparent alias for the standard Nat.Prime predicate; the remaining depends_on edges supply collision-free and algebraic-tautology interfaces from the foundation and game-theory layers that keep the arithmetic layer free of hidden axioms.
proof idea
One-line wrapper that applies the native_decide tactic to the conjunction of the two primality statements.
why it matters
The declaration supplies a verified primality fact that the module uses when instantiating arithmetic functions at small primes; the doc-comment flags it as RS-relevant for the superprime notion tied to the seventh prime. It sits inside the NumberTheory.Primes layer that feeds the phi-ladder constructions and mass formulas of the broader framework. No downstream uses are recorded, so the result functions as a self-contained anchor rather than a lemma in a longer chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.