sigmaClosed
plain-language theorem explainer
Predicate on an eight-tick cadence: the moral-state skew at the last tick equals zero. Anyone wiring σ=0 hard constraints into the RS→RL bridge cites it as the end-of-window closure check. The body is a one-line definition reading skew on window index 7.
Claim. An eight-tick cadence $c$ is $\sigma$-closed when the skew of its moral state at tick $7$ (the final slot of the window) satisfies $\mathrm{skew}(c_7)=0$.
background
The RS→RL bridge treats Recognition Science as control theory: moral states carry ledger, bonds, skew, and energy; admissible moves are fourteen virtue generators; hard feasibility is the $\sigma=0$ set enforced by a propose-then-project completion. Temporal aggregation is not discounted: T6/T7 force an undiscounted eight-tick octave, so trajectories are scored in atomic windows of length $2^3$.
An eight-tick cadence packages eight moral states (ticks $0..7$) and the virtue actions taken at each tick. Skew is the $\sigma$ imbalance on the moral state; the module's hard constraint is that feasible trajectories return $\sigma$ to zero. This definition is exactly that end-of-window check: does $\sigma$ close by tick 8?
proof idea
Definition, not a derived theorem. It unfolds to equality of the skew field on the window state at $\langle 7,_\rangle$ with $0$. The Fin-8 bound is discharged by omega; no lemmas about dynamics or virtues are invoked.
why it matters
Closes the vocabulary for the module's hard constraint layer: feasible RL trajectories must be $\sigma$-closed over each eight-tick block. That matches the design rule "no arbitrary discount" and the T7 eight-tick octave (period $2^3$) from the forcing chain. Downstream machinery (feasible-set projection, lexicographic selectors, Gibbs policies) is meant to keep or restore this predicate; the definition itself is the boolean gate those pieces target. No used-by edges are recorded yet, so it currently stands as the named interface for end-of-window $\sigma$ audit rather than a proved conservation law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.