pythagorean_prime_sixtyone
plain-language theorem explainer
61 is prime and congruent to 1 modulo 4, qualifying it as a Pythagorean prime. Number theorists handling concrete cases inside the Recognition Science arithmetic functions module would cite the fact when working with sums of squares or prime distributions. The proof is a direct computational check performed by the native_decide tactic.
Claim. $61$ is prime and $61$ satisfies $61 ≡ 1 mod 4$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ, while keeping statements simple until Dirichlet algebra is added. The Prime predicate is the transparent repo-local alias for Nat.Prime. Upstream results include structural 'is' assertions from option-A empirical programs, simplicial ledgers, mechanism design, and mock-theta constructions, each confirming collision-free or tautological status without new axioms.
proof idea
The proof is a one-line term that applies the native_decide tactic to evaluate both the primality predicate and the modular condition directly.
why it matters
The declaration populates the NumberTheory.Primes.ArithmeticFunctions file with a concrete Pythagorean prime example. No downstream uses are recorded. It supplies a specific instance for later arithmetic-function work but does not engage the core Recognition Science landmarks such as the J-uniqueness forcing step, the eight-tick octave, or the RCL identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.