ledger_entropy
plain-language theorem explainer
Ledger entropy assigns to each ledger state the value of its reciprocity skew, quantifying the absolute logarithmic imbalance across active bonds. Information theorists deriving Landauer bounds from recognition costs would cite this when linking RS-native costs to thermodynamic entropy. The definition is a direct one-line alias to the reciprocity_skew function on the input ledger state.
Claim. For a ledger state $s$ with active bonds having positive real multipliers, the ledger entropy is defined as the absolute log-imbalance of the ledger, realized via the reciprocity skew of $s$.
background
The module formalizes the link between Recognition Science cost and thermodynamic entropy, anchoring the theory in the Landauer limit. LedgerState is the minimal local ledger structure consisting of a Finset of active bonds together with a map from bonds to positive real multipliers. Upstream results supply the fundamental tick as the RS time quantum with value 1, the Energy type alias, and cost functions from multiplicative recognizers and observer forcing that extract the J-cost of recognition events.
proof idea
The definition is a one-line wrapper that directly applies the reciprocity_skew function to the input ledger state.
why it matters
This definition supplies the entropy measure required to relate recognition costs to thermodynamic quantities in the Landauer limit. It supports sibling constructions such as thermal_cost and the eight-tick dissipation limit within the same module. The declaration fills the entropy slot in phase 7.5.2, connecting to the recognition composition law and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.