prime_onehundredthree
plain-language theorem explainer
103 is prime. Recognition Science modelers cite this fact as one of the stable prime anchors alongside 11, 17, 37, and 137 to keep later arithmetic lemmas readable. The proof succeeds by a one-line decision procedure that verifies the predicate directly for this small integer.
Claim. $103$ is a prime number.
background
The RSConstants module assembles small decidable arithmetic facts about integers that recur in the reality repo, such as the primes 11, 17, 37, 103, and 137. These serve as fixed anchors that prevent repeated proofs of the same elementary statements in bridge lemmas. Prime is the transparent alias for Nat.Prime, the standard predicate asserting that a natural number has no divisors other than 1 and itself.
proof idea
The proof is a one-line wrapper that invokes the decide tactic. This tactic computes the decidable instance of Nat.Prime for the concrete value 103 and confirms the predicate holds by direct evaluation.
why it matters
The declaration supplies a base arithmetic fact that stabilizes the collection of prime markers used throughout Recognition Science derivations. It sits alongside the marker 137 that lies inside the documented alpha inverse band (137.030, 137.039). No downstream theorems are recorded yet, but the fact supports the overall scaffolding of RS constants that later connect to the forcing chain and J-cost definitions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.