prime_five
plain-language theorem explainer
The theorem asserts that 5 is a prime natural number. Modular lemmas in the Recognition Science framework cite it when restricting the prime divisors of wheel840 to the set 2, 3, 5, 7. The proof reduces to a single decision procedure that evaluates the primality predicate on the concrete value.
Claim. The natural number $5$ satisfies the primality predicate, i.e., $5$ is prime.
background
The module gathers small decidable arithmetic facts about integers that recur in the reality repo, including factorizations involving 8, 45, 360, and 840 together with prime markers such as 11, 17, 37, 103, and 137. These serve as stable anchors that keep later bridge lemmas readable. The predicate Prime is supplied by the Basic module as a transparent alias for Mathlib's Nat.Prime.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the concrete primality check for 5.
why it matters
The result feeds directly into prime_dvd_wheel840, which states that any prime divisor of wheel840 equals 2, 3, 5, or 7, and into wheel840_accepts, which shows that integers coprime to wheel840 avoid these four primes. These anchors prevent repeated arithmetic proofs in modular arguments that connect to the Recognition Science constants. The module doc describes them as intentionally boring but stable reference points.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.