IntegerLedgerStateLogic
IntegerLedgerStateLogic n asserts positivity for a logic-natural number n in the recovered arithmetic setting. It is cited by certificates that transport primality from LogicNat to classical Nat in the prime-ledger stack. The definition is a direct one-line abbreviation equating the state to the strict inequality 0 < n.
claimFor a logic-natural number $n$, the predicate IntegerLedgerStateLogic($n$) is defined to hold precisely when $0 < n$.
background
The module introduces logic-native prime ledger atoms as the first recovered-number adapter for the RH and prime-ledger stack, with primality stated on LogicNat and transported through the equivalence LogicNat.toNat. LogicNat is the inductive type forced by the Law of Logic whose constructors identity (zero-cost multiplicative identity) and step (one iteration of the generator) mirror the orbit {1, γ, γ², ...} as the smallest subset of positive reals closed under multiplication by γ containing 1.
proof idea
One-line definition that directly unfolds IntegerLedgerStateLogic n to the proposition 0 < n on the LogicNat type.
why it matters in Recognition Science
This definition supplies the positive ledger state required by the PrimeLedgerLogicCert structure, which certifies the transport PrimeLedgerAtomLogic p ↔ Nat.Prime (toNat p) and includes the field prime_positive : ∀ {p : LogicNat}, Nat.Prime (toNat p) → IntegerLedgerStateLogic p. It is invoked directly in the theorem prime_logic_is_positive_ledger_state to recover positivity from classical primality. In the Recognition framework it closes the recovery step for positive integers, enabling the logic-native prime ledger to interface with the ArithmeticFromLogic foundation.
scope and limits
- Does not assert any primality properties on its own.
- Does not compute or expose the value of toNat n.
- Does not extend the state to zero or negative elements of LogicNat.
- Does not provide an explicit embedding or isomorphism to classical naturals.
Lean usage
example {p : LogicNat} (hp : Nat.Prime (toNat p)) : IntegerLedgerStateLogic p := prime_logic_is_positive_ledger_state hpformal statement (Lean)
27def IntegerLedgerStateLogic (n : LogicNat) : Prop :=
proof body
Definition body.
28 0 < n
29