mod6_fortyseven_prime
plain-language theorem explainer
47 is shown to be prime with residue 5 modulo 6. Researchers handling modular arithmetic on small primes or preparing inputs for arithmetic function calculations would cite this result. The verification relies on a single native_decide invocation that resolves both the primality predicate and the modular equality simultaneously.
Claim. $47$ is prime and $47 ≡ 5 (mod 6)$.
background
The module supplies lightweight wrappers around Mathlib's arithmetic functions, beginning with the Möbius function. This theorem supplies a basic modular fact about the prime 47. The upstream definition of Prime is a transparent alias for the standard natural number primality predicate.
proof idea
The proof is a one-line term that invokes native_decide to confirm the conjunction of primality and the congruence.
why it matters
This fact supplies a verified instance of a prime congruent to 5 mod 6 for use in the arithmetic functions module. It fills a concrete modular constraint needed for prime-related calculations. No direct link to the Recognition Science forcing chain or constants appears.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.