SigmaFeasible
plain-language theorem explainer
A moral state is σ-feasible exactly when its reciprocity skew vanishes. This is the hard conservation constraint used by the RS-to-RL bridge: policies may propose freely, then least-action completion projects onto the σ=0 manifold before evaluation. Anyone citing LACompletion, the lexicographic selector, or the RL audit goals needs this predicate. The body is a one-line definitional equality with the skew field.
Claim. A moral state $s$ is $\sigma$-feasible if and only if its reciprocity skew vanishes: $\sigma(s) = 0$. Equivalently, the ledger is globally balanced under the conservation law.
background
The RS→RL bridge treats Recognition Science as control theory: states, admissible generators, hard constraints, and a thermodynamic policy. The lightweight moral state carries the essential RS quantities for training: reciprocity skew $\sigma$ (log-multiplier imbalance), available energy budget, value functional $V$, maximum externalized harm $\Delta S$, and a spectral-gap robustness measure.
Skew is the global reciprocity imbalance. Conservation forces $\sigma = 0$ as a hard feasibility constraint, not a soft penalty. Upstream cost machinery (J-cost on ratios, recognition-event cost, multiplicative-recognizer cost) supplies the action cost that least-action completion minimizes when restoring balance; the predicate itself only names the feasible set.
Module design separates creativity from physics: the policy proposes an unconstrained virtue-coefficient direction; projection enforces $\sigma=0$ before the move is scored. Eight-tick cadence (T6/T7) and Gibbs policies sit downstream of this constraint.
proof idea
Definitional, not a derived theorem. The predicate is the proposition that the moral state's skew field equals zero. No lemmas are applied; unfolding yields $s.\mathrm{skew} = 0$ by construction. Downstream audit goals restate the same equivalence by rfl.
why it matters
This predicate is the hard gate in the RS→RL stack. LACompletion is specified to project arbitrary virtue actions onto the $\sigma=0$ feasible manifold while minimizing added J-cost (propose-then-project, analogous to constrained policy optimization and control barrier functions). The RL audit theorem goal_sigma_feasibility records the equivalence as the admissibility constraint before harm-minimax, value, and robustness in the lexicographic selector.
In the broader framework it is the conservation-law cut: reciprocity balance must hold before thermodynamic learning ($p(a|s)\propto\exp(-J/T_R)$) or eight-tick window evaluation. Without a named feasible set, the bridge cannot separate policy exploration from physics enforcement. It does not itself prove existence of a projector; that lives in the LACompletion structure's postconditions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.