prime_is_ledger_atom_logic
plain-language theorem explainer
If a logic-natural p has toNat(p) prime then p satisfies PrimeLedgerAtomLogic. Researchers recovering primality statements inside the RH prime-ledger stack cite this transport step. The argument is a one-line wrapper applying the right-to-left direction of the equivalence that equates the two primality predicates.
Claim. Let $p$ be a logic-natural number. If the recovered value toNat($p$) is a prime natural number, then PrimeLedgerAtomLogic($p$) holds, i.e., PrimeLedgerAtom(toNat($p$)) is true.
background
LogicNat is the inductive type forced by the Law of Logic, with constructors identity (the zero-cost multiplicative identity) and step (one iteration of the generator), forming the smallest orbit closed under multiplication by the generator and containing 1. The function toNat reads the iteration count: identity maps to 0 and step n maps to the successor of toNat n. PrimeLedgerAtomLogic p is the logic-native predicate defined by PrimeLedgerAtom(toNat p), serving as the recovered-naturals version of primality. The module supplies the first adapter that states primality directly on LogicNat and transports it through the recovery map toNat, as part of the RH prime-ledger stack.
proof idea
The proof is a one-line wrapper that applies the mpr (right-to-left) direction of the equivalence theorem primeLedgerAtomLogic_iff_prime to the hypothesis that toNat p is prime.
why it matters
This result completes the logic-native transport of primality into the prime ledger atom setting, directly implementing the recovered-number adapter described in the module documentation. It bridges the ArithmeticFromLogic layer to the NumberTheory prime constructions and supports the full equivalence between standard and logic-native primality statements. No downstream uses are recorded yet, but the declaration closes one direction of the prime atom equivalence needed for the ledger stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.