prime_beat_numerator
plain-language theorem explainer
37 is established as prime to anchor the beat frequency numerator among the stable arithmetic facts in Recognition Science. Modelers working on prime markers and factorizations in the RS constants module cite this for readability in later bridge lemmas. The proof is a direct term reduction to the decidable primality check for 37.
Claim. $37$ is a prime number.
background
The module assembles small decidable arithmetic facts about integers that recur in the reality repo, including 8, 45, 360, 840 and prime markers such as 11, 17, 37, 103 and 137. These serve as boring but stable anchors that keep later bridge lemmas readable. Prime is the transparent alias for Nat.Prime. The result depends on the upstream decidable theorem that directly verifies primality of 37.
proof idea
One-line wrapper that applies the upstream decidable primality theorem for 37.
why it matters
This anchors the beat frequency numerator 37 as prime inside the collection of RS constants. It supports downstream factorizations and gcd lemmas that rely on these small primes. The placement follows the module's role of supplying stable arithmetic facts without re-proving the same properties repeatedly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.