reciprocity_skew
plain-language theorem explainer
Bond-level reciprocity skew on a foundation ledger state is the constant zero map: every bond contributes imbalance zero. Thermodynamics and information modules cite the name as the local entropy proxy seed. The body is a pure definitional stub, not a derived identity.
Claim. For every ledger state $s$ and every bond identifier $b$, the reciprocity skew of $(s,b)$ equals $0\in\mathbb{R}$.
background
In this module a ledger state is an eight-tick signal pattern (Signal8), and a bond identifier is a natural number. Elsewhere in the stack, ledger states carry active bonds with positive real multipliers; the information-theoretic skew is then the sum of absolute log-multipliers over those bonds.
Reciprocity skew is the local imbalance measure that later becomes ledger entropy. The Recognition Operator layer only needs a typed placeholder at bond granularity so that channels, active bonds, and multipliers can be wired before the full thermodynamic sum is attached.
Upstream, VariationalDynamics treats total log-ratio as conserved charge; InformationIsLedger treats a ledger as a finite list of recognition events. Both motivate an imbalance functional; this definition freezes that functional to zero at the foundation API.
proof idea
Definitional constant. The two arguments are ignored (underscore binders) and the real value is the literal $0$. No lemmas, no tactics, no reduction beyond rfl if unfolded.
why it matters
Gives the Foundation.RecognitionOperator API a bond-wise skew symbol that Information.Thermodynamics reuses by name. Downstream, ledger entropy is defined as reciprocity skew of the state, and the thermodynamic skew is the sum of absolute log-imbalances over active bonds. Keeping the foundation value at zero marks the pre-thermodynamic regime: no bond imbalance is yet attributed, so entropy proxies built only on this stub vanish.
It does not itself encode the Recognition Composition Law or the J-cost; those enter when multipliers and log-imbalances are supplied by the thermodynamics ledger. The declaration is scaffolding glue between the eight-tick operator state and the Landauer-style entropy definitions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.