mod4_fiftynine_prime
plain-language theorem explainer
59 is a prime congruent to 3 modulo 4. Researchers handling quadratic residues or Dirichlet characters would reference this concrete case when checking residue conditions. The proof reduces to a single native_decide tactic that evaluates both primality and the modular remainder directly.
Claim. $59$ is prime and $59$ satisfies $59 ≡ 3$ (mod 4).
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. This declaration supplies a specific prime in the residue class 3 mod 4 that can support squarefree checks or inversion formulas elsewhere in the file.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate the conjunction of the primality predicate and the remainder condition by direct computation.
why it matters
This theorem populates the Primes submodule with a verified instance usable in arithmetic-function identities. It does not advance core Recognition Science steps such as the forcing chain or Recognition Composition Law. No downstream declarations depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.