mod6_onehundredthirtyseven_prime
plain-language theorem explainer
137 is prime and satisfies 137 ≡ 5 (mod 6). Number theorists working inside the Recognition Science number-theory layer cite the fact when anchoring modular checks near the inverse fine-structure constant. The proof is a single native_decide invocation that discharges both conjuncts by direct computation.
Claim. $137$ is prime and $137 ≡ 5 (mod 6)$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Primes are introduced via the definition Primes := {n | Nat.Prime n} and the transparent local alias Prime (n : ℕ) := Nat.Prime n. The surrounding file keeps statements minimal while deeper Dirichlet inversion is prepared.
proof idea
The proof is a one-line wrapper that applies native_decide to confirm both primality of 137 and the residue 137 mod 6 = 5 by direct evaluation.
why it matters
The declaration supplies a concrete modular fact for the prime 137, which lies inside the Recognition Science band for α^{-1}. It supports arithmetic checks in the primes section of the number-theory layer and is placed immediately before further 200-range primes. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.