pythagorean_prime_onehundredthirtyseven
plain-language theorem explainer
137 is a prime congruent to 1 modulo 4. Number theorists classifying sums-of-two-squares primes or Recognition Science modelers working on the fine-structure constant band would cite the fact. The verification reduces the conjunction to a decidable proposition and confirms it by direct computation.
Claim. $137$ is prime and $137 ≡ 1 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. The local setting is a collection of small, stable interfaces for Dirichlet algebra that can later support inversion formulas.
proof idea
The proof is a one-line term-mode application of native_decide that reduces both conjuncts to decidable checks and verifies them computationally.
why it matters
The declaration records that 137 is a Pythagorean prime inside the Recognition Science interval for alpha inverse. It supplies a concrete numerical anchor for the alpha band without new hypotheses. No parent theorems are listed among the immediate dependents.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.