prime_eleven
plain-language theorem explainer
The declaration asserts that 11 is a prime natural number. Recognition Science modelers cite it as one of the stable arithmetic anchors for derivations that reference the phi-ladder and the alpha band near 137. The proof reduces the claim to a single decidable computation.
Claim. $11$ is a prime natural number.
background
The module collects small decidable arithmetic facts about integers that recur in Recognition Science, such as the primes 11, 17, 37, 103 and 137 together with factorizations of 8, 45, 360 and 840. These serve as fixed reference points so that later bridge lemmas remain readable without re-proving elementary arithmetic. Prime is the transparent alias for the standard predicate that a natural number has no divisors other than 1 and itself.
proof idea
The proof is a one-line wrapper that invokes the decidable instance for the primality predicate on the concrete value 11.
why it matters
It supplies a verified fact that stabilizes arithmetic steps inside the RSConstants module and any downstream number-theoretic bridges. In the broader framework the result supports concrete prime markers that appear in the alpha band and the phi-ladder mass formula. No open questions or scaffolding are involved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.