selectByLex
plain-language theorem explainer
Given an evaluator from moral state and virtue action to an audit bundle, pick the best action from a finite list under the RS lexicographic order (feasibility first, then harm, value, robustness, φ-tier). Anyone wiring the multi-objective selector in the RS→RL bridge cites this. Implementation is a left fold that keeps the current champion via the Boolean lex comparator.
Claim. Fix an evaluation map $E$ sending a moral state $s$ and virtue action $a$ to an audit result (post-action skew $\sigma$, max harm, value $V$, spectral gap $\lambda_2$, $\varphi$-tier). For a list of candidate virtue actions, return $\mathrm{None}$ if the list is empty, otherwise the unique left-to-right champion under the lexicographic preference that ranks feasible ($\sigma=0$) above infeasible, then minimizes worst harm, maximizes $V$, maximizes $\lambda_2$, and breaks remaining ties by $\varphi$-tier.
background
The ambient module is the RS→RL bridge: Recognition Science is treated as a control theory with moral states, 14 virtue generators as the admissible action basis, hard $\sigma=0$ feasibility, and a multi-objective lexicographic selector before any thermodynamic (Gibbs) policy.
A MoralState packages reciprocity skew $\sigma$, energy budget, value $V=\kappa\cdot I(A;E)-C_{J^*}$, max harm, and a spectral-gap robustness coordinate. A VirtueAction is a 14-coefficient vector over the DREAM-complete minimal virtue generators; the policy explores in that basis, not raw moves. An AuditResult bundles the post-action quantities the selector needs: $\sigma$ after the action, max harm $\Delta_S$, value $V$, $\lambda_2$, and a $\varphi$-tier tiebreak.
Upstream, lexBetter encodes the fixed priority order from RS: (1) feasibility gate $\sigma=0$, (2) minimize worst harm, (3) maximize value, (4) maximize robustness $\lambda_2$, (5) $\varphi$-tier. The module design separates propose (policy) from project ($\sigma=0$ via LACompletion) and uses undiscounted eight-tick windows forced by T6/T7.
proof idea
Pure definition, not a proof. Initialize the accumulator to none and left-fold over the candidate list. The first action becomes the provisional champion. For each later action $a$, evaluate both $a$ and the current best under the supplied evaluator at the fixed state $s$, and replace the champion exactly when lexBetter returns true on those two AuditResults. Empty input yields none; otherwise the fold returns some of the lex-champion (stable under ties: the earlier list entry wins).
why it matters
This is the concrete multi-objective selector named in the module design principles: feasible → harm-minimax → value → robustness (with $\varphi$-tier). It turns the abstract RS priority stack into an executable argmax over virtue-coefficient actions, which is the decision core of the RS→RL bridge before Gibbs sampling $p(a|s)\propto\exp(-J(s,a)/T_R)$ and eight-tick cadence evaluation.
No downstream dependents are recorded yet in the graph, so the declaration presently stands as infrastructure for the LexicographicSelector story rather than a lemma feeding a named parent theorem. It sits downstream of the DREAM completeness claim for the 14 virtues and of the hard $\sigma=0$ feasibility discipline (LACompletion), and it respects the T6/T7 eight-tick minimality theme by staying undiscounted and list-finite. Scaffolding closure would be wiring this into a full policy loop with LACompletion projection and Gibbs sampling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.