mod6_twentynine_prime
plain-language theorem explainer
29 is prime and congruent to 5 modulo 6. Number theorists working with arithmetic functions would cite this fact when handling residue classes for primes in Möbius evaluations or squarefree checks. The proof is a direct computational verification via the native_decide tactic on the conjunction.
Claim. 29 is a prime number and satisfies $29 ≡ 5 (mod 6)$.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, starting with the Möbius function μ. Statements remain basic to allow later layering of Dirichlet algebra and inversion once interfaces stabilize. The sole upstream dependency defines Prime n as the transparent alias Nat.Prime n.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate the primality predicate and the modular equality directly.
why it matters
This supplies a concrete prime-residue instance inside the arithmetic-functions module. It supports case handling for Möbius and squarefree properties on primes congruent to 5 mod 6, though no downstream uses are recorded. The fact sits outside the Recognition Science forcing chain and phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.