superprime_fiftynine
plain-language theorem explainer
The declaration asserts that both 59 and 17 are prime numbers. Number theorists applying arithmetic functions to Möbius calculations within the Recognition Science framework would cite this for small-prime verification. The proof is a direct computational check via native decision.
Claim. 59 is prime and 17 is prime.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function μ. Local setting is basic prime facts to support later Dirichlet algebra and inversion once interfaces stabilize. The Prime predicate is the transparent alias for the standard Nat.Prime predicate on natural numbers.
proof idea
One-line wrapper that applies native_decide to resolve the conjunction of primality predicates through direct computation.
why it matters
This supplies verified small primes for the arithmetic functions section, supporting Möbius footholds needed for Recognition Composition Law applications. It contributes basic number-theoretic facts to the framework's T0-T8 forcing chain, though no downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.