Pith. sign in
structure

LexicographicSelector

definition
show as:
module
IndisputableMonolith.Verification.RecognitionStabilityAudit.RStoRL
domain
Verification
line
252 · github
papers citing
none yet

plain-language theorem explainer

A multi-objective action selector that encodes the Recognition Science priority order for RL: hard-gate on reciprocity feasibility (σ = 0), then minimize maximum harm ΔS, then maximize value V and spectral robustness λ₂. Anyone wiring an RS-native policy or environment cites this interface. It is a pure structure definition bundling evaluate and selectBest; no proof content.

Claim. A lexicographic selector is a pair of maps: an evaluator sending a moral state $s$ and virtue-action $a$ to an audit result $(\sigma_{\mathrm{after}}, \Delta S_{\max}, V, \lambda_2, \varphi\text{-tier})$, and a chooser sending $s$ and a list of virtue-actions to an optional best action. Selection is intended to enforce the priority $\sigma=0$ (hard) $\succ$ minimize $\max\Delta S$ $\succ$ maximize $V$ $\succ$ maximize $\lambda_2$.

background

The RS→RL bridge treats Recognition Science as a specified control theory rather than philosophy. States are lightweight moral states carrying reciprocity skew σ, energy budget, value functional $V = \kappa\cdot I(A;E) - C_{J*}$, maximum harm ΔS, and spectral gap λ₂. Actions are 14-coefficient vectors over the virtue generators; the DREAM theorem is cited as guaranteeing that set is a complete minimal basis for admissible ethical transformations.

Audit results bundle the post-action quantities needed for ordered comparison: σ after the action, max harm, value, λ₂, and a φ-tier for tiebreaking. The module design separates creativity from physics via a propose-then-project pattern (LACompletion onto the σ = 0 set) and uses undiscounted eight-tick windows forced by T6/T7 octave structure, not an arbitrary discount factor.

Within that setting the selector is the multi-objective ranking layer: feasibility first, harm-minimax second, then value and robustness.

proof idea

No proof. This is a structure declaration with two fields: evaluate (MoralState → VirtueAction → AuditResult) and selectBest (MoralState → List VirtueAction → Option VirtueAction). Concrete ranking logic lives in sibling definitions such as the feasibility filter that retains only actions with σ_after = 0. The structure itself only fixes the interface shape.

why it matters

This is the multi-objective priority ordering named in the module header: feasible → harm-minimax → value → robustness. It is the selection half of the RS→RL stack, paired with LACompletion (projection) and GibbsPolicy (thermodynamic sampling $p(a|s)\propto\exp(-J(s,a)/T_R)$).

Downstream, the full RS environment bundles this selector with initial moral state and the LACompletion projector so an agent can train natively in RS units. The feasibility filter is defined against the evaluate field. Eight-tick cadence checks (including patience: zero action until tick 7) sit in the same training interface.

Framework landmarks in play: T6/T7 eight-tick windows, J-cost in the Gibbs layer, and the virtue-generator basis from the ethics stack. The declaration does not itself prove uniqueness of the priority order; it packages the order the audit module treats as canonical.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.