pythagorean_prime_eightynine
plain-language theorem explainer
89 is a prime congruent to 1 modulo 4. Researchers enumerating small Pythagorean primes for sums-of-squares work cite this explicit case. The verification is a direct numerical check performed by native_decide on the conjunction.
Claim. 89 is prime and $89 ≡ 1 mod 4$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function as a foothold. The Prime abbreviation is the transparent alias for the standard natural-number primality predicate. The local theoretical setting keeps statements minimal until deeper Dirichlet algebra is layered on.
proof idea
One-line wrapper that applies native_decide to confirm both primality and the residue class by direct evaluation.
why it matters
This populates the arithmetic-functions module with a concrete Pythagorean prime instance. No parent theorems or downstream uses are recorded. It supplies a verified numerical fact for the number-theory component without invoking the forcing chain, phi-ladder, or Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.