mod6_seventyone_prime
plain-language theorem explainer
71 is prime and congruent to 5 modulo 6. Number theorists using arithmetic functions on primes in specific residue classes would cite this auxiliary fact. The proof is a one-line wrapper that applies native_decide to verify both primality and the modular arithmetic condition at once.
Claim. $71$ is a prime number and $71 ≡ 5$ (mod $6$).
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, starting with the Möbius function μ. This theorem supplies a concrete modular fact about the integer 71 for use in prime-related calculations. It depends on the transparent alias Prime n := Nat.Prime n, which asserts that n has no positive divisors other than 1 and itself.
proof idea
The proof is a one-line wrapper that invokes native_decide to evaluate the conjunction of the primality predicate and the congruence 71 % 6 = 5.
why it matters
This supplies a verified prime fact inside the arithmetic-functions module that can support later Möbius applications on primes ≡5 mod 6. It sits downstream of the Basic module's Prime alias and contributes a small concrete instance to the number-theoretic scaffolding of the Recognition Science framework, though it does not invoke the forcing chain or phi-ladder directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.