net_skew
plain-language theorem explainer
Net skew of any ledger state is fixed at the real value 0. Ledger bookkeeping in the Recognition Operator treats global imbalance as identically cancelled. The body is a constant assignment, not a derived identity from bond data.
Claim. For every ledger state $s$, the net skew equals $0\in\mathbb{R}$.
background
In this module a ledger state is an abbreviation for an eight-component signal (Signal8), the discrete carrier tied to the eight-tick octave. Sibling fields on the same state record time, Z-patterns, global phase, active bonds, bond multipliers, and agent endpoints.
Net skew is the scalar meant to summarize residual imbalance across that ledger. The present declaration does not read those fields; it simply names the quantity and sets it to zero. The surrounding import is complex-structure forcing, so the ledger sits inside the foundation layer that prepares the Recognition Operator, not inside a mass or coupling calculation.
proof idea
Definitional constant: the right-hand side is the real literal 0, independent of the unused state argument. No lemmas, tactics, or algebraic reduction.
why it matters
Gives a named hook for global ledger balance inside Foundation.RecognitionOperator. Downstream consumers can treat net skew as already closed (identically zero) without recomputing bond sums. No used-by edges are recorded yet, so it is scaffolding for operator-level conservation language rather than a step in the T0–T8 forcing chain, the RCL, or the mass ladder. It encodes the modeling choice that the eight-tick ledger is kept balanced by definition at this layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.