selectAction
plain-language theorem explainer
Given an RS environment, a moral state, and a list of virtue-coefficient actions, return the best admissible action after projecting each candidate onto the σ=0 feasible set. Control theorists and RL implementers working the RS→RL bridge cite this as the single entry point that couples propose-then-project with lexicographic multi-objective choice. The body is a one-line composition: map through the LACompletion projector, then call the environment's lexicographic selector.
Claim. For an RS environment $E$ (bundling an LACompletion projector and a lexicographic selector), a moral state $s$, and a finite list of virtue actions $A = [a_1,\ldots,a_n]$, define $\mathrm{select}(E,s,A) := E.\mathrm{selector}.\mathrm{selectBest}\bigl(s,\; [E.\mathrm{projector}.\mathrm{project}(a)]_{a\in A}\bigr) \in \mathrm{Option}(\mathrm{VirtueAction})$.
background
The RS→RL bridge treats Recognition Science as a fully specified control theory: states are lightweight moral states (reciprocity skew σ, energy budget, value functional $V$, max harm, spectral gap), and actions are 14-coefficient vectors over the virtue generators guaranteed complete and minimal by the DREAM theorem.
Hard physics is enforced by LACompletion: a propose-then-project map onto the σ=0 feasible set, so the policy may invent freely while the projector restores ledger reciprocity. Selection is multi-objective and lexicographic (feasible first, then harm-minimax, value, robustness), not a scalar reward. The environment structure packages initial state, projector, selector, and a Gibbs policy for thermodynamic exploration $p(a|s)\propto\exp(-J(s,a)/T_R)$.
Evaluation windows follow the forced eight-tick cadence (T6/T7), so there is no arbitrary discount factor. This definition sits at the end of the environment section, immediately before consent and harm constraints.
proof idea
Pure definitional composition, no proof obligations. Project every candidate virtue action through env.projector.project (LACompletion onto σ=0), then hand the projected list and the current moral state to env.selector.selectBest. The return type is Option VirtueAction, so the selector may refuse every candidate. No lemmas are invoked; the meaning is entirely in the two field applications.
why it matters
This is the operational hinge of the RS→RL bridge: it is the only place where creativity (the candidate list from a policy) is separated from physics (σ=0 projection) and then ranked by the lexicographic ethics stack. It realizes the module design principle "separate creativity from physics" and feeds any training loop that must emit an admissible virtue action rather than a raw control. Framework landmarks in play are the DREAM completeness of the 14 virtues, T6/T7 eight-tick cadence (via the surrounding environment), and the J-cost Gibbs policy carried on the same environment record. No downstream theorems currently depend on it in the graph; it is infrastructure for agent code and for later consent/harm sections that assume a chosen action already exists.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.