PrimeLedgerAtomLogic
PrimeLedgerAtomLogic defines primality for a LogicNat element by transporting the upstream PrimeLedgerAtom predicate through the toNat recovery map. Number theorists working on the Recognition Science prime-ledger stack cite this adapter when bridging logic-native arithmetic to classical primality. The definition is a direct one-line wrapper that applies PrimeLedgerAtom to the recovered natural number.
claimFor an element $p$ of LogicNat, PrimeLedgerAtomLogic($p$) holds precisely when PrimeLedgerAtom(toNat $p$) holds, where toNat recovers the iteration count as a standard natural number and PrimeLedgerAtom requires that number to be prime together with multiplicative irreducibility.
background
LogicNat is the inductive type with constructors identity (the zero-cost multiplicative identity) and step, forming the smallest orbit closed under multiplication by the generator and containing 1, as forced by the Law of Logic. The map toNat sends identity to 0 and each successive step to the successor, recovering the standard natural number value. PrimeLedgerAtom is the structure on a natural number $p$ asserting Nat.Prime $p$ together with the irreducibility condition that $p = a * b$ implies $a = 1$ or $b = 1$. The module provides the first recovered-number adapter for the RH / prime-ledger stack, stating primality directly on LogicNat while transporting through the recovery equivalence.
proof idea
This is a one-line wrapper that applies the PrimeLedgerAtom predicate to the image of $p$ under the toNat recovery map from ArithmeticFromLogic.
why it matters in Recognition Science
The definition anchors the LogicPrimeLedgerAtom module and directly feeds the equivalence primeLedgerAtomLogic_iff_prime, which in turn supports PrimeLedgerLogicCert and the surrounding theorems that tie recovered primes to the classical ledger. It adapts the prime ledger atom concept to logic-native numbers, enabling the multiplicative ledger states to interface with the forced arithmetic. In the Recognition framework this supplies the base predicate for the prime-ledger stack used in number-theoretic foundations.
scope and limits
- Does not assert existence of any prime numbers.
- Does not supply a decision procedure for primality.
- Does not extend beyond the toNat recovery equivalence.
- Does not incorporate J-cost or defectDist measures.
Lean usage
theorem use_example (p : LogicNat) : PrimeLedgerAtomLogic p ↔ Nat.Prime (toNat p) := primeLedgerAtomLogic_iff_prime pformal statement (Lean)
23def PrimeLedgerAtomLogic (p : LogicNat) : Prop :=
proof body
Definition body.
24 PrimeLedgerAtom (toNat p)
25
26/-- A recovered positive integer ledger state. -/