one_not_primeLedgerAtomLogic
plain-language theorem explainer
The theorem establishes that the recovered natural number one fails the prime ledger atom condition. Number theorists adapting the Recognition Science prime-ledger stack to logic-native naturals cite this to enforce the classical exclusion of the unit. The short tactic proof assumes the atom property, applies the equivalence lemma to recover Nat.Prime on toNat(fromNat 1), rewrites via toNat_fromNat, and invokes the standard fact that one is not prime.
Claim. The recovered natural number 1 is not a prime ledger atom: if $p = $fromNat$(1)$ then it is not the case that PrimeLedgerAtomLogic$(p)$, where PrimeLedgerAtomLogic$(p)$ holds precisely when the classical primality predicate applies to the integer recovered by toNat$(p)$.
background
The module introduces logic-native prime ledger atoms by transporting the classical PrimeLedgerAtom predicate through the recovery map toNat on LogicNat. LogicNat is the inductive type with identity and step constructors; fromNat embeds ordinary naturals by iterated stepping while toNat reads off the iteration count. The sibling definition states PrimeLedgerAtomLogic$(p)$ as PrimeLedgerAtom(toNat $p$), and the equivalence PrimeLedgerAtomLogic $p$ ↔ Nat.Prime(toNat $p$) is given by the referenced theorem ledger_atom_logic_is_prime.
proof idea
Assume for contradiction that PrimeLedgerAtomLogic(fromNat 1) holds. Apply ledger_atom_logic_is_prime to obtain Nat.Prime(toNat(fromNat 1)). Rewrite with toNat_fromNat to reach Nat.Prime 1. Conclude by exact application of the classical lemma Nat.not_prime_one.
why it matters
The result supplies the one_not_atom field inside the PrimeLedgerLogicCert record, which certifies that logic-native primality matches the classical notion including exclusion of one. It completes the adapter layer that recovers the RH prime-ledger stack from the logic foundation, ensuring consistency with the T5 J-uniqueness and phi-ladder structure used for mass formulas downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.