mod6_seventynine_prime
plain-language theorem explainer
79 is prime and lies in the residue class 1 mod 6. Number theorists verifying small cases for Dirichlet characters or sieve applications would cite the fact. The proof is a one-line native_decide that evaluates the conjunction of the standard primality predicate and the modular arithmetic condition by direct computation.
Claim. $79$ is prime and $79 ≡ 1 mod 6$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ and its basic properties on squarefree integers. The local setting keeps statements minimal to allow later layering of Dirichlet inversion once interfaces stabilize. The declaration depends on the transparent alias Prime for the standard Nat.Prime predicate on natural numbers.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to the conjunction, which computes both primality and the residue directly from the definitions without further lemmas.
why it matters
The result supplies a concrete verified prime in the 1 mod 6 class inside the arithmetic-functions module. It supports basic prime-specific calculations that may later connect to Möbius evaluations or related identities in the Recognition Science formalization. No downstream uses are recorded and no open questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.