mod6_ninetyseven_prime
plain-language theorem explainer
97 is established as prime with 97 ≡ 1 (mod 6). Number theorists checking arithmetic progressions or applying Möbius inversion to specific primes would reference this fact. The proof reduces to a single native_decide call that computes the conjunction directly.
Claim. $97$ is prime and $97 ≡ 1$ (mod $6$).
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function μ. The local setting keeps statements minimal so that deeper Dirichlet algebra and inversion can be added once basic interfaces stabilize. The sole upstream dependency is the transparent alias Prime n := Nat.Prime n, which imports the standard primality predicate without additional hypotheses.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate the conjunction of primality and the modular condition by direct computation.
why it matters
This supplies a concrete verified prime congruent to 1 modulo 6 inside the arithmetic-functions module. It supports downstream checks on Möbius values at primes, though the used-by count is currently zero. The result sits among the basic number-theoretic footholds required before layering Recognition Science constants or the phi-ladder onto arithmetic functions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.