ledger_atom_logic_is_prime
plain-language theorem explainer
ledger_atom_logic_is_prime establishes that a LogicNat satisfying the prime ledger atom predicate forces its recovered natural number to be prime. Number theorists recovering arithmetic inside the Recognition Science framework cite it to transport primality across the logic-to-Nat bridge. The proof is a one-line term that applies the forward direction of the equivalence relating the two predicates.
Claim. Let $p$ be an element of the logic-forced naturals. If $p$ satisfies the prime ledger atom predicate, then the natural number recovered by counting the iteration steps in $p$ is prime.
background
The module introduces logic-native primality statements as the first adapter for the prime-ledger stack. LogicNat is the inductive type whose constructors identity and step generate the orbit of the multiplicative generator, with identity as the zero-cost element. The map toNat reads off the iteration count, sending identity to 0 and each step to a successor, thereby recovering a standard natural number.
proof idea
The proof is the term (primeLedgerAtomLogic_iff_prime p).mp h. It applies the left-to-right direction of the equivalence that identifies PrimeLedgerAtomLogic p with Nat.Prime after toNat.
why it matters
The result is invoked directly by one_not_primeLedgerAtomLogic to show that the recovered 1 fails primality. It anchors the logic-native definition to standard arithmetic, ensuring consistency for the prime-ledger approach in Recognition Science. The module doc positions it as the recovered-number adapter for the RH context.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.