mod6_sixtyseven_prime
plain-language theorem explainer
67 is established as prime and congruent to 1 modulo 6. Number theorists checking residue classes for primes greater than 3, or preparing inputs for arithmetic functions such as the Möbius function, would cite this fact. The proof is a direct one-line application of native_decide that evaluates both conjuncts by computation.
Claim. $67$ is prime and $67 ≡ 1 (mod 6)$.
background
The declaration sits inside the module on arithmetic functions that supplies lightweight wrappers around Mathlib’s Möbius function μ. The module keeps statements minimal so that Dirichlet inversion and related algebra can be added once the basic interfaces are stable. It imports the Prime abbreviation from the Basic submodule, where Prime n is defined as the transparent alias Nat.Prime n.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to the conjunction Prime 67 ∧ 67 % 6 = 1.
why it matters
The result supplies a verified concrete instance of a prime lying in the residue class 1 mod 6. Such instances are the raw material for later statements about squarefree numbers and the Möbius function at specific arguments inside the same module. No downstream uses are recorded yet, so the declaration functions as a building block for future arithmetic-function lemmas rather than a direct link to the Recognition Science forcing chain or phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.