mod4_sixtyseven_prime
plain-language theorem explainer
67 is established as a prime congruent to 3 modulo 4. Number theorists checking small cases for quadratic residues or Möbius evaluations at primes would cite this auxiliary fact. The verification proceeds by direct computation through a native decision tactic.
Claim. $67$ is prime and $67 ≡ 3 mod 4$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function for later Dirichlet inversion work. Prime is the local transparent alias for the standard predicate Nat.Prime on natural numbers. This theorem records a concrete instance of a prime in the residue class 3 mod 4, useful for basic checks on squarefree integers or small Möbius values.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate both the primality predicate and the remainder operation modulo 4 by direct computation.
why it matters
The result supplies a verified small prime in the 3 mod 4 class inside the arithmetic functions library, supporting downstream Möbius and big-Omega calculations. It fills a basic fact in the primes submodule but does not engage the Recognition Science forcing chain, J-uniqueness, or phi-ladder. No open questions or scaffolding are attached.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.