LedgerState
plain-language theorem explainer
This abbreviation supplies the ledger state type for a d-account posting model by instantiating the general recognition ledger over the minimal AccountRS carrier. Modelers of information thermodynamics and variational dynamics cite it to link single-account debit-credit updates to one-bit parity shifts. The definition is a direct type alias with no additional axioms or computations.
Claim. For natural number $d$, a ledger state is the recognition ledger whose carrier is the minimal $d$-account structure with underlying set Fin($d$) and trivial recognition relation.
background
The module upgrades vector lemmas to an explicit ledger model in which a state consists of debit-credit pairs and each tick posts one unit to exactly one account. AccountRS($d$) is defined as the recognition structure with $U :=$ Fin $d$ and $R$ always true, providing the concrete carrier for atomic ticks. Upstream ledger-state structures appear in VariationalDynamics as configurations indexed by tick with conserved log-ratio charge, in InformationIsLedger as finite lists of recognition events, and in Thermodynamics as active bonds with positive multipliers.
proof idea
One-line type abbreviation that directly applies the Recognition.Ledger constructor to the AccountRS($d$) structure.
why it matters
Supplies the ledger state type consumed by diagonalHamiltonian in HamiltonianEmergence and by ledger_identity plus totalInfoCost in InformationIsLedger. It supplies the missing glue between ledger posting language and the parity one-bit adjacency lemma, supporting the Recognition Composition Law and the eight-tick octave. The module doc notes that deriving why nature adopts this posting model remains a separate bridge step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.