prime_thirtyseven
plain-language theorem explainer
37 is established as a prime natural number. Researchers referencing beat frequency numerators in Recognition Science calculations cite this fact to anchor arithmetic steps. The proof is a one-line decision procedure that resolves the primality predicate by direct computation.
Claim. The natural number 37 is prime.
background
The RSConstants module gathers small decidable arithmetic facts on integers that recur in the reality repo, including prime markers 11, 17, 37, 103, and 137. These serve as stable anchors that keep later bridge lemmas readable without repeated arithmetic proofs. Prime is the repo-local alias for the standard primality predicate on natural numbers.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the decidable primality statement.
why it matters
This supplies the primality of 37 used directly by the theorem establishing that the beat frequency numerator 37 is prime. It belongs to the set of prime facts collected for constants in the framework, including those near the inverse fine structure constant band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.