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

LedgerState

show as:
view Lean formalization →

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.

claimA 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  21structure LedgerState where
  22  active_bonds : Finset ℕ
  23  bond_multipliers : ℕ → ℝ
  24  bond_pos : ∀ b ∈ active_bonds, 0 < bond_multipliers b
  25
  26/-- Total recognition cost over active bonds. -/

used by (40)

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

… and 10 more

depends on (6)

Lean names referenced from this declaration's body.