IntegerLedgerStateLogic
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.