RSEnvironment
plain-language theorem explainer
Bundles the full Recognition Science control stack into one RL environment: initial moral state, σ=0 least-action projector, lexicographic multi-objective selector, and Gibbs policy. Anyone wiring RS ethics into a training loop cites this as the environment type. Pure structure definition; no proof obligations beyond field well-formedness.
Claim. An RS environment is a 4-tuple $(s_0, P, L, G)$ where $s_0$ is an initial moral state (skew $\sigma$, energy, value $V$, max harm, spectral gap), $P$ is a least-action completion map projecting virtue actions onto the $\sigma=0$ feasible set, $L$ is a lexicographic selector (feasibility gate, then harm-minimax, then value and robustness), and $G$ is a Gibbs policy $p(a|s)\propto\exp(-J(s,a)/T_R)$ with $T_R>0$.
background
The RS→RL bridge treats Recognition Science as already-specified control theory, not philosophy. States are lightweight moral records: reciprocity skew $\sigma$, energy budget, value $V=\kappa\cdot I(A;E)-C_{J^*}$, max harm $\Delta S$, and spectral gap $\lambda_2$. Actions are 14-coefficient vectors over the virtue generators; the DREAM theorem asserts these form a complete minimal generating set for admissible ethical transformations.
Hard physics is enforced by LACompletion: the policy proposes freely, then a least-action projector lands the move on the $\sigma=0$ manifold while minimizing added $J$-cost. Selection is lexicographic (feasible first, harm-minimax second, then value and robustness), not a scalarized reward. Exploration uses the RS thermodynamic law $p(a|s)\propto\exp(-J(s,a)/T_R)$, the same $J$ forced by the Recognition Composition Law and T5 uniqueness.
Temporal aggregation is fixed by T6: undiscounted eight-tick windows, not arbitrary discount factors. The module imports Cost and Constants so $J$ and $\phi$-native units are available to the policy cost field.
proof idea
No proof: this is a structure declaration packing four already-defined components (MoralState, LACompletion, LexicographicSelector, GibbsPolicy) into a single environment record. Field docs only annotate roles. Downstream defs step and selectAction are the first consumers; they pattern-match on the packed fields rather than proving new properties here.
why it matters
This is the single type that makes RS-native RL executable. Downstream, step projects an action through LACompletion then audits via the lexicographic selector; selectAction maps candidates through the projector and picks the best. Together they implement the design split "propose (policy) vs project (physics)" stated in the module header.
Framework landmarks in play: T5/T6 force the cost $J$ and the eight-tick cadence that replace discounting; the Gibbs form is the thermodynamic exploration rule grounded in that same $J$, not an ad-hoc entropy bonus. The 14-virtue action basis comes from the DREAM completeness claim on ethical generators. Without this bundle, the audit machinery (feasibility, harm, value, robustness) cannot be threaded through a standard RL loop as one environment object.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.