pythagorean_prime_twentynine
plain-language theorem explainer
29 is a prime congruent to 1 modulo 4. Number theorists classifying primes that arise as sums of two squares would cite this arithmetic fact. The proof proceeds by direct computational verification through native decision procedures.
Claim. $29$ is prime and $29 ≡ 1 mod 4$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The local theoretical setting keeps statements minimal before adding Dirichlet inversion layers. The Prime predicate is the transparent alias for the standard Nat.Prime predicate on natural numbers.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the conjunction of primality and the modular condition by direct computation.
why it matters
This supplies a concrete instance of a prime congruent to 1 mod 4 inside the primes arithmetic-functions file. It supports basic number-theoretic scaffolding that may later feed into Recognition Science calculations involving prime distributions on the phi-ladder. No downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.