AuditResult
plain-language theorem explainer
An audit result packages five scalars from evaluating a moral state under a virtue action: residual ledger skew σ, worst-case harm, value functional V, spectral gap λ₂, and a φ-tier integer. Anyone building the RS→RL lexicographic selector cites this record as the comparison payload. It is a plain structure definition with no proof obligations.
Claim. An audit result is a 5-tuple $(\sigma_{\mathrm{after}},\,\Delta S_{\max},\,V,\,\lambda_2,\,t_\varphi)\in\mathbb{R}^4\times\mathbb{Z}$, where $\sigma_{\mathrm{after}}$ is residual skew after the action (feasibility requires $0$), $\Delta S_{\max}$ is maximum harm imposed on any agent, $V=\kappa\cdot I(A;E)-C_{J^*}$ is the value functional, $\lambda_2$ is the spectral gap (robustness), and $t_\varphi\in\mathbb{Z}$ is the $\varphi$-tier used only for tiebreaking.
background
The RS→RL bridge treats Recognition Science as a fully specified control theory: moral states carry ledger, bonds, skew, and energy; admissible moves are 14 virtue generators; hard feasibility is the σ=0 slice enforced by LA-completion (propose then project). Multi-objective choice is not a weighted sum. It is a strict priority stack: feasible first, then minimax harm, then value, then robustness, then φ-tier.
The five fields of this record are exactly the coordinates that stack needs. Residual σ after the action is the hard gate. Maximum harm ΔS is the primary soft objective among feasible moves. Value V is the mutual-information surplus over J-cost. The spectral gap λ₂ measures how stably the post-action configuration sits. The integer φ-tier breaks residual ties along the golden-ratio ladder forced by T6.
Sibling machinery (MoralState, VirtueAction, LACompletion, energyCost, SigmaFeasible) supplies the inputs; this structure only freezes the evaluation snapshot.
proof idea
No proof. The declaration is a structure with five fields and an Inhabited instance. Field meanings are fixed by the inline doc-comments: sigmaAfter for the post-action feasibility check, maxHarm for worst-case ΔS, value for V = κ·I(A;E) − C_J*, lambda2 for the spectral gap, and phiTier for the integer φ-ladder rank. Downstream comparison code (lexBetter) pattern-matches on these fields in priority order.
why it matters
This record is the comparison currency of the entire lexicographic selector. Downstream, lexBetter and lexBetter_irrefl read its fields in the RS priority order (σ-gate, then min max-harm, then max V, then max λ₂, then φ-tier). filterFeasible keeps only actions with sigmaAfter = 0. LexicographicSelector and selectByLex fold over lists of virtue actions by comparing AuditResult values; step advances the control loop on the same payload. The RL-side goal_lexBetter_irrefl re-exports irreflexivity for the goal layer.
In framework terms it implements the multi-objective half of the bridge module: hard σ=0 feasibility (LA-completion), harm-minimax ethics, value from the J-cost ledger, robustness via spectral gap, and T6-aligned φ-tier tiebreak. Without a single frozen 5-tuple, the priority stack cannot be stated as a pure Boolean comparison.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.