prime_three
plain-language theorem explainer
The declaration establishes that 3 satisfies the primality predicate on the natural numbers. Number theorists extending the Recognition monolith cite it when confirming that 3 divides wheel840 in modular constructions. The proof reduces to a single decidable check that confirms the predicate holds.
Claim. The natural number 3 is prime.
background
The module supplies basic prime-number footholds that reuse Mathlib's Nat.Prime without introducing axioms or sorries. Prime is the transparent alias abbrev Prime (n : ℕ) : Prop := Nat.Prime n. The local setting consists of small sanity theorems that verify the algebraic layer before any analytic number theory is added.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the decidable instance of Nat.Prime 3.
why it matters
prime_three feeds the downstream results prime_dvd_wheel840 and wheel840_accepts, which together show that any prime divisor of wheel840 must be 2, 3, 5 or 7. It supplies a verified small prime for the modular arithmetic layer of the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.