reciprocity_skew
plain-language theorem explainer
reciprocity_skew supplies the entropy proxy for a local information ledger by summing absolute log-imbalances of active bond multipliers. Researchers deriving Landauer bounds and dissipation limits in Recognition Science cite this definition when quantifying information imbalance from ledger states. The definition is a direct sum over the Finset of active bonds using the absolute real logarithm of each multiplier.
Claim. For a ledger state $s$ with active bonds $B$ and positive multipliers $m_b$, the reciprocity skew is defined as $s = B.sum (fun b => |log m_b|)$.
background
LedgerState is the minimal local ledger state for the information-theoretic Landauer bound. It consists of a Finset of active bonds, a function from bonds to positive real multipliers, and a proof that all multipliers are positive. The module formalizes the relationship between Recognition Science cost and thermodynamic entropy, anchoring the theory in the Landauer limit.
proof idea
This is a one-line definition that applies the sum operation over the active bonds of the absolute value of the real logarithm of each bond multiplier.
why it matters
This definition supplies the entropy proxy that ledger_entropy directly aliases in the same module. It anchors the Landauer limit and 8-tick dissipation calculations by quantifying log-imbalance in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.