mod6_fiftythree_prime
plain-language theorem explainer
The declaration asserts that 53 is prime and congruent to 5 modulo 6. Number theorists building arithmetic functions or checking residue classes for Möbius inversion might cite this explicit fact. The proof is a one-line computational verification that directly evaluates both conjuncts.
Claim. $53$ is prime and $53 ≡ 5$ (mod $6$).
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ, and keeps statements minimal until Dirichlet algebra stabilizes. The Prime predicate is the transparent alias for the standard definition of primality on natural numbers. This specific fact supplies an explicit prime in the residue class 5 mod 6, a class often needed when evaluating arithmetic functions on squarefree integers.
proof idea
The proof is a one-line wrapper that applies native_decide to the conjunction of primality and the modular arithmetic condition.
why it matters
The result supplies a concrete prime instance inside the arithmetic-functions module that supports later handling of squarefree numbers and Möbius values. No downstream theorems are recorded yet, so it functions as a basic building block rather than a direct link to the Recognition Science forcing chain or phi-ladder. It remains available for any future classification of primes modulo small integers required by the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.