primeLedgerAtomLogic_iff_prime
plain-language theorem explainer
The theorem equates the prime ledger atom property on logic-native naturals with ordinary primality after applying the recovery map toNat. Researchers adapting the prime-ledger formulation of the Riemann hypothesis to the logic setting cite it to move classical primality facts across the recovery equivalence. The proof is a one-line wrapper that applies the base equivalence after mapping the input through toNat.
Claim. For a logic-natural number $p$, $p$ satisfies the prime ledger atom property if and only if the recovered value toNat$(p)$ is a prime natural number.
background
LogicNat is the inductive type with constructors identity (the zero-cost element) and step, representing the smallest subset of positive reals closed under multiplication by the generator and containing 1. The function toNat reads off the iteration count, sending identity to 0 and step n to the successor of toNat n. PrimeLedgerAtomLogic p is defined as PrimeLedgerAtom applied to toNat p, where PrimeLedgerAtom is the ledger-atom formulation of primality on ordinary naturals.
proof idea
The proof is a one-line wrapper that invokes the base theorem primeLedgerAtom_iff_prime on the image of p under toNat.
why it matters
This equivalence is the transport lemma that lifts the classical prime characterization into the logic-native setting for the prime-ledger stack. It is used directly to construct the certificate primeLedgerLogicCert and to prove the directional lemmas ledger_atom_logic_is_prime and prime_is_ledger_atom_logic. It supplies the recovered-number adapter required for the RH / prime-ledger development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.