not_prime_one
plain-language theorem explainer
The natural number 1 is not prime. Ledger-atom constructions in the Recognition monolith cite this to exclude the unit from prime-based states. The proof is a one-line decision procedure that invokes decidability of the primality predicate.
Claim. $1$ is not prime: $¬ Prime(1)$, where $Prime(n)$ is the predicate that $n$ is a prime natural number.
background
The module supplies axiom-free sanity theorems for primes by reusing Mathlib’s Nat.Prime predicate without introducing new axioms or sorries. Prime is the transparent local alias abbrev Prime (n : ℕ) : Prop := Nat.Prime n. The module documentation states the design goal of providing small checks that confirm correct wiring before any growth into analytic number theory.
proof idea
One-line wrapper that applies the decide tactic to the decidable goal ¬ Nat.Prime 1.
why it matters
The result is invoked by one_not_primeLedgerAtom and one_not_primeLedgerAtomLogic to conclude that the unit is not a prime ledger atom. It supplies a basic foothold in the primes layer, ensuring the algebraic setup remains consistent with the axiom-free requirement before any appeal to the forcing chain or phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.