lexBetter
plain-language theorem explainer
Lexicographic preference on audit outcomes for RS-to-RL control: feasible (σ=0) beats infeasible; among infeasible, smaller |σ|; among feasible, lower max harm, then higher value V, then higher spectral gap λ₂, then lower φ-tier. Anyone wiring multi-objective virtue selection or proving selector irreflexivity cites it. The body is a nested Boolean cascade over the five AuditResult fields.
Claim. Given two audit results $a,b$ (each carrying post-action skew $\sigma$, worst harm $\max\Delta S$, value $V$, spectral gap $\lambda_2$, and a $\varphi$-tier), return true exactly when $a$ is strictly preferred to $b$ under the fixed priority: (1) $\sigma=0$ beats $\sigma\neq 0$; (2) if both infeasible, smaller $|\sigma|$; (3) if both feasible, smaller max harm; (4) then larger $V$; (5) then larger $\lambda_2$; (6) then smaller $\varphi$-tier.
background
The RS→RL bridge treats Recognition Science as control theory: moral states, fourteen virtue generators as the action basis, hard $\sigma=0$ feasibility via LA-completion, and multi-objective selection rather than a scalar reward. An audit result packages the five scalars needed after evaluating a (state, action) pair: post-action skew $\sigma$ (feasibility gate), maximum harm $\max\Delta S$ imposed on any agent, value $V=\kappa\cdot I(A;E)-C_{J^*}$, spectral gap $\lambda_2$ as robustness, and a $\varphi$-tier for residual ties.
Module design separates propose from project: the policy may invent virtue coefficients; LA-completion enforces the feasible set. Selection among audited candidates must respect RS priority, not an ad hoc weighted sum. The eight-tick cadence (T6/T7) frames evaluation windows; this comparator is the static ranking used inside those windows and by the Gibbs policy layer.
proof idea
Definitional cascade, not a proof. Layer 1 branches on whether each side has $\sigma=0$: mixed feasibility decides immediately; both nonzero compares absolute skew; both zero falls through. Layers 2–4 are strict numeric comparisons on max harm (minimize), value (maximize), and $\lambda_2$ (maximize), each with early true/false exits on inequality. Only full ties reach layer 5, which prefers the smaller $\varphi$-tier. No lemmas are invoked; the Boolean expression is the entire content.
why it matters
This is the concrete LexicographicSelector promised by the module: hard $\sigma$-gate, then harm-minimax, then value and robustness, matching the RS ethics stack rather than scalarized RL. Downstream, selectByLex folds a candidate list with this predicate to pick a best virtue action; lexBetter_irrefl (and the RL goal wrapper) prove no result is strictly better than itself, a sanity obligation for any strict preference used in selection or policy proofs.
In the broader framework it operationalizes the separation of feasibility from optimization that LA-completion and the virtue basis assume. It does not itself invoke J-cost uniqueness (T5) or the mass ladder, but it sits on the same control path that later uses thermodynamic weights $p(a|s)\propto\exp(-J/T_R)$ and eight-tick windows.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.