primeLedgerAtom_iff_prime
plain-language theorem explainer
The theorem equates the PrimeLedgerAtom predicate on a natural number p with ordinary primality in the naturals. Number theorists extending the Recognition Science multiplicative ledger to the RH bridge would cite this equivalence to justify classical primality checks inside the ledger. The proof is a term-mode pairing of the two directional lemmas already established in the same module.
Claim. For any natural number $p$, the structure PrimeLedgerAtom$(p)$ holds if and only if $p$ is prime in the usual sense, where PrimeLedgerAtom$(p)$ requires both that $p$ is a standard prime and that $p$ is multiplicatively irreducible: $p = a b$ implies $a = 1$ or $b = 1$.
background
PrimeLedgerAtom is the structure on a natural number $p$ that packages standard primality together with the irreducibility condition appropriate to the multiplicative positive-integer ledger. The module grounds the arithmetic ledger used by the RH bridge, treating primes as the irreducible postings of that monoid before any weighting into the Euler ledger occurs. The two upstream results in the same file are ledger_atom_is_prime, which extracts Nat.Prime from the structure, and prime_is_ledger_atom, which constructs the structure from a standard prime by verifying the irreducibility condition via divisibility.
proof idea
The proof is a term-mode wrapper that directly supplies the biconditional by pairing the two directional theorems already proved in the module: ledger_atom_is_prime for the forward direction and prime_is_ledger_atom for the reverse.
why it matters
This equivalence populates the atom_iff_prime field of the PrimeLedgerCert definition and is lifted verbatim to the LogicNat setting in primeLedgerAtomLogic_iff_prime. It supplies the classical number-theoretic foundation for the prime ledger atoms before they enter the Euler ledger and the broader Recognition Science forcing chain. The result therefore sits at the interface between ordinary arithmetic and the RS-native ledger used for subsequent phi-ladder and J-cost constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.