filterFeasible
plain-language theorem explainer
Feasibility filter that keeps only virtue actions leaving reciprocity skew at zero after evaluation. The lexicographic RS→RL selector cites it as the hard first gate before harm, value, and robustness ranking. Implementation is a one-line list filter on the audit field σ_after = 0.
Claim. Given an evaluation map from moral states and virtue actions to audit results, a state $s$, and a list of actions, return the sublist of those actions $a$ for which the post-action reciprocity skew satisfies $\sigma_{\mathrm{after}}(s,a)=0$.
background
The RS→RL bridge treats Recognition Science as control theory: moral states carry skew σ, energy budget, value $V$, max harm, and spectral gap; actions are 14-coefficient vectors over the DREAM virtue generators. Hard physics is separated from proposal: only σ = 0 states are admissible (LACompletion projects proposals onto that set).
An audit result bundles the quantities needed for multi-objective selection: post-action σ, max harm ΔS, value, λ₂ robustness, and a φ-tier. The lexicographic selector ranks feasible actions first, then minimax harm, then value, then robustness. This definition is the pure feasibility cut inside that stack.
Upstream cost and entropy notions (J-cost on ratios, defect entropy) motivate why σ = 0 is non-negotiable: zero skew is the reciprocity-balanced, minimum-defect ledger state the ethics layer must preserve.
proof idea
Definitional one-liner: filter the input list by deciding equality of the audit field sigmaAfter with zero under the supplied evaluator at the fixed state. No lemmas; pure List.filter plus decide on real equality.
why it matters
Implements the hard constraint half of the module's design principle "separate creativity from physics": the policy may propose any virtue coefficients, but only σ = 0 survivors enter lexicographic ranking. That matches the bridge's claim that admissible ethical moves stay on the reciprocity-balanced ledger, consistent with LACompletion as propose-then-project and with T6-aligned eight-tick evaluation windows used later for undiscounted returns.
No downstream theorems currently depend on it in the graph; it is local scaffolding for the LexicographicSelector section before the Gibbs/thermodynamic policy (p(a|s) ∝ exp(-J/T_R)). It closes the feasibility gate that Temperance and Hope later soften via energy caps and exploratory temperature, without weakening the σ = 0 cut itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.