MoralState
plain-language theorem explainer
MoralState is the five-component real state vector used by the RS-to-RL bridge: reciprocity skew σ, energy budget, value functional V, max externalized harm ΔS, and spectral gap λ₂. Anyone wiring Recognition Science into a control or RL loop cites it as the observation type. It is a plain structure definition with Inhabited, not a proved claim.
Claim. A moral state is a 5-tuple $(\sigma, E, V, \Delta S_{\max}, \lambda_2) \in \mathbb{R}^5$, where $\sigma$ is reciprocity skew (log-multiplier imbalance), $E$ is the available recognition-cost energy budget, $V$ is the value functional (of the form $\kappa\, I(A;E) - C_{J}^*$), $\Delta S_{\max}$ bounds imposed harm, and $\lambda_2$ is the spectral gap measuring robustness.
background
The enclosing module is the RS→RL bridge: it treats Recognition Science as already-specified control theory and exports state, admissible actions, hard constraints, a lexicographic multi-objective selector, and a Gibbs policy. Design rules include actions as virtue coefficients, propose-then-project separation of creativity from physics, and undiscounted eight-tick windows forced by T6 rather than arbitrary discounting.
MoralState is the lightweight observation type for that loop. Field meanings are fixed by the doc-comment and field annotations: skew is reciprocity imbalance σ; energy is the recognition-cost budget; value is the scalar $V = \kappa\cdot I(A;E) - C_J^*$; maxHarm is maximum imposed ΔS; lambda2 is the robustness spectral gap λ₂. Upstream edges touch RS-native Action (just ℝ), various certified value evaluators, and foundation quantities (gap active-edge count, simplex vertices), which supply the real-valued carriers this structure packages rather than new physics.
Sibling machinery in the same file (VirtueAction as a 14-coefficient generator vector, SigmaFeasible, LACompletion, EightTickCadence) consumes this state type.
proof idea
No proof. This is a structure declaration with five ℝ fields and deriving Inhabited, so the zero/default inhabitant is automatic. Mathematical content is entirely in the field names and their doc-comments; there is no tactic block or term proof to walk.
why it matters
MoralState is the shared state carrier for the whole Recognition Stability Audit RL layer. Downstream, EightTickCadence stores an 8-tick window of MoralState (the unique temporal aggregator from T6 minimality: no arbitrary discount, evaluate undiscounted blocks). Feasibility is literally SigmaFeasible s ↔ s.skew = 0. Gibbs policy goals (positive weights, positive partition function) and eight-tick total-value finiteness are stated over MoralState → ℝ maps.
In framework terms it packages the control observables needed to enforce σ=0 admissibility, harm-minimax, value, and robustness in lexicographic order, while the DREAM theorem supplies the 14-virtue action basis that acts on this state. It does not itself prove T6, RCL, or DREAM; it is the typed interface those results feed when RS is run as RL.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.