prime_onehundredthirtyseven
plain-language theorem explainer
137 is established as a prime natural number. Recognition Science workers cite this to anchor the prime marker near the inverse fine-structure constant band. The proof reduces to a single decide tactic that evaluates the primality predicate by direct computation.
Claim. $137$ is prime, i.e., the predicate Prime$(137)$ holds where Prime$(n)$ is the standard definition that $n$ is a prime natural number.
background
The module assembles small decidable arithmetic facts about integers that recur in the reality repo, such as the primes 11, 17, 37, 103 and 137 together with cycle integers 8, 45, 360 and 840. These facts function as stable anchors that keep later bridge lemmas readable and avoid repeated arithmetic proofs. The Prime predicate is the local transparent alias for the standard Nat.Prime test on natural numbers.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the decidable proposition Prime 137.
why it matters
This supplies a stable arithmetic anchor for the prime marker 137 that lies inside the Recognition Science alpha inverse band (137.030, 137.039). It belongs to the collection of RS cycle integers and factorizations that support bridge lemmas without re-proving basic primality. No downstream uses are recorded, yet the fact closes a potential gap for constant-related statements in the T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.