pith. machine review for the scientific record. sign in
abbrev definition def or abbrev high

LedgerState

show as:
view Lean formalization →

LedgerState for a parameter d is the recognition ledger instantiated over the d-account carrier with trivial recognition relation. Researchers modeling information costs, thermodynamic bounds, or variational dynamics cite it to specialize general ledgers to finite posting accounts. The definition is a direct type abbreviation with no proof obligations or computational content.

claimFor each natural number $d$, the ledger state is the recognition ledger whose underlying universe is the finite set of $d$ accounts equipped with the trivial recognition relation.

background

The module develops posting-style ledger updates that induce one-bit parity adjacency. A ledger state here tracks debit-credit pairs across accounts, with each tick posting exactly one unit to one account. AccountRS d supplies the minimal carrier: its universe is the finite set Fin d and its recognition relation is the constant true predicate, making the structure available for any d without further constraints. Upstream ledger structures in VariationalDynamics, InformationIsLedger, and Thermodynamics supply the general pattern of configurations or event lists indexed by ticks, which this abbreviation specializes to the account posting model.

proof idea

This is a one-line abbreviation that directly instantiates the Recognition.Ledger type constructor on the AccountRS d carrier.

why it matters in Recognition Science

The definition supplies the concrete ledger type used by diagonalHamiltonian in HamiltonianEmergence, by ledger_identity and totalInfoCost in InformationIsLedger, and by admissible states in Thermodynamics. It closes the modeling gap between general recognition ledgers and the parity one-bit adjacency lemma, supporting the transition from T5 J-uniqueness through the eight-tick octave to information-theoretic bounds. The module documentation notes that deriving why nature adopts this posting model remains a separate bridge step.

scope and limits

formal statement (Lean)

  58abbrev LedgerState (d : Nat) : Type := Recognition.Ledger (AccountRS d)

proof body

Definition body.

  59

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (5)

Lean names referenced from this declaration's body.