mod6_seventeen_prime
plain-language theorem explainer
The declaration asserts that 17 is prime and satisfies the congruence 17 ≡ 5 mod 6. Number theorists handling arithmetic functions such as the Möbius function cite this when checking concrete prime instances modulo 6 in inversion formulas or distribution arguments. The proof is a one-line term that applies the native_decide tactic to resolve the decidable conjunction by direct computation.
Claim. $17$ is prime and $17 ≡ 5 (mod 6)$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Prime is the transparent alias for the standard predicate Nat.Prime on natural numbers. The local setting keeps statements minimal so that Dirichlet algebra and inversion can be added once the basic interfaces are stable; the present fact supplies one concrete prime obeying the noted congruence.
proof idea
The proof is a one-line term that invokes native_decide on the conjunction of primality and the modular equality, letting the kernel compute both decidable properties directly.
why it matters
This supplies a verified modular property of the prime 17 for use in arithmetic-function calculations inside the Recognition Science framework. It acts as a Möbius foothold for handling specific cases that arise in prime distributions or inversion identities. No downstream theorems are recorded yet, but the fact closes a concrete RS-relevant number-theoretic instance.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.