pythagorean_prime_thirtyseven
plain-language theorem explainer
37 is prime and satisfies 37 ≡ 1 (mod 4), confirming it as a Pythagorean prime expressible as a sum of two squares. Number theorists checking small cases in quadratic forms or Recognition Science arithmetic layers would cite the fact for explicit verification. The proof is a one-line native decision procedure that directly evaluates primality and the congruence.
Claim. $37$ is prime and $37 ≡ 1 (mod 4)$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, starting with the Möbius function μ. Prime is the repo-local alias for Nat.Prime. Upstream results include structural 'is' declarations from Foundation.OptionAEmpiricalProgram, SimplicialLedger.EdgeLengthFromPsi, GameTheory.MechanismDesignFromSigma, and RamanujanBridge.MockThetaPhantom that supply collision-free or tautological contexts for empirical claims.
proof idea
One-line wrapper that applies native_decide to verify the conjunction of primality and the modular arithmetic condition.
why it matters
The declaration supplies a concrete Pythagorean prime instance inside the NumberTheory.Primes.ArithmeticFunctions layer. It fills a basic fact slot that can feed arithmetic function applications such as Möbius evaluations on small primes, though no downstream uses are recorded yet. It aligns with the framework's pattern of explicit small-case checks before layering Dirichlet algebra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.