LedgerState
plain-language theorem explainer
LedgerState packages a finite set of active bond indices with a positivity-constrained multiplier map from naturals to reals. Researchers deriving information-theoretic bounds in Recognition Science cite it when stating the Landauer inequality for recognition cost. The declaration is a plain structure definition whose three fields directly supply the data and axiom needed for downstream thermodynamic statements.
Claim. A ledger state consists of a finite set $B subset mathbb{N}$ of active bonds, a function $m:mathbb{N}to mathbb{R}$ assigning multipliers to bonds, and the condition that $m(b)>0$ for every $b in B$.
background
The Information.Thermodynamics module formalizes the link between Recognition Science cost and thermodynamic entropy, anchoring the theory at the Landauer limit. LedgerState supplies the minimal local state for that derivation. It relies on the cost function from MultiplicativeRecognizerL4 (the derived cost of a comparator on positive ratios) and the J-cost from ObserverForcing (the cost of a recognition event). Upstream structures in VariationalDynamics and InformationIsLedger define ledger states via configurations or lists of events, while the present version restricts to active bonds and multipliers for the thermodynamic bound.
proof idea
The declaration is a structure definition that introduces the three fields active_bonds, bond_multipliers, and the bond_pos axiom. No lemmas or tactics are invoked; the construction is the base data type used by the admissible predicate and the H_ThermodynamicsVerified hypothesis.
why it matters
LedgerState supplies the state type required by H_ThermodynamicsVerified, the hypothesis that recognition cost satisfies the Landauer bound for information erasure. It supports the module's goal of relating Recognition Science cost to thermodynamic entropy and the eight-tick dissipation limit. The definition sits inside the forcing chain that produces D=3 and the alpha band, providing the concrete data structure for the information-to-thermodynamics step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.