reciprocity_skew_abs
plain-language theorem explainer
Absolute reciprocity skew is defined as the constant zero functional on ledger states. Anyone wiring balance or skew terms into the recognition operator would cite it as the current stub. The body is a one-line constant definition, not a derived identity.
Claim. For every ledger state $s$, the absolute reciprocity skew is defined by $\mathrm{skew}_{\mathrm{abs}}(s) := 0$.
background
In this module a ledger state is an abbreviation for an eight-channel signal (Signal8), the discrete carrier used by the recognition operator. Sibling fields on that state include time, Z-patterns, global phase, channels, and active bonds.
Related modules carry richer ledger structures: variational dynamics uses an $N$-entry configuration with a tick and a conserved total log-ratio (the ledger charge); the information-ledger view is a finite list of recognition events with a total information cost; the thermodynamic ledger tracks active bonds and positive bond multipliers for a Landauer-style bound.
No module-level doc is supplied here. The name points at a scalar that would measure departure from reciprocity (pair balance under the Recognition Composition Law), but the present declaration does not yet compute one.
proof idea
There is no proof. The declaration is a definition whose right-hand side is the real constant $0$, ignoring the ledger-state argument. No lemmas are applied.
why it matters
It reserves a named hook for absolute reciprocity skew inside the foundation recognition-operator layer. Downstream use sites are empty in the graph, so nothing yet depends on a nontrivial value.
In the broader framework, reciprocity is tied to the Recognition Composition Law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$ and to J-uniqueness (forcing step T5). A future nonzero skew would quantify imbalance relative to that law on eight-tick ledger states; the constant-zero stub keeps the API stable until that measure is specified.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.