mod6_seven_prime
plain-language theorem explainer
7 is prime and congruent to 1 modulo 6. Number theorists using arithmetic functions or Möbius inversion in the Recognition Science setup cite this for explicit small-prime checks. The proof applies a native decision procedure to confirm the conjunction in one step.
Claim. The integer 7 is prime and satisfies $7 ≡ 1 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 primality predicate on natural numbers. The declaration supplies a concrete small-prime instance within this arithmetic-functions interface.
proof idea
It is a one-line wrapper that applies native_decide to evaluate the primality predicate and the modular equality directly.
why it matters
The result supplies a basic prime fact needed for arithmetic-function calculations in the Recognition framework. It aligns with the module's goal of stabilizing basic interfaces before layering Dirichlet algebra, though no downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.