prime_fortyseven
plain-language theorem explainer
47 is a prime natural number. Number theorists working with arithmetic functions such as the Möbius function in the Recognition Science mirror cite this when specializing proofs to the prime 47. The proof consists of a single decide tactic invocation that computes the primality predicate directly.
Claim. The natural number $47$ is prime.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function μ. Statements remain preparatory pending stabilization of basic interfaces for deeper Dirichlet algebra. Upstream, Prime is the transparent alias for Nat.Prime, the standard primality predicate on natural numbers.
proof idea
The proof is a one-line wrapper that applies the decide tactic to confirm that 47 satisfies the Prime predicate.
why it matters
This supplies a concrete prime instance inside the arithmetic functions module. It supports potential prime-specific cases in Möbius inversions or squarefree checks, though no downstream uses are recorded. The declaration remains a basic number-theoretic fact without linkage to the T0-T8 forcing chain, J-uniqueness, or phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.