interpret
plain-language theorem explainer
Decomposes a 14-coefficient virtue-action into a list of (virtue name, coefficient) pairs for human-readable logging and audit. Anyone wiring the RS→RL bridge or inspecting Gibbs policies cites this. The body is a one-line List.ofFn zip of the fixed name table with the coefficient vector.
Claim. Given a virtue action $a$ (a map $a : \{0,\ldots,13\} \to \mathbb{R}$ of coefficients on the fourteen virtue generators), return the length-14 list of pairs $(\mathrm{name}_i, a_i)$ for $i=0,\ldots,13$, where $\mathrm{name}_i$ is the fixed string label of the $i$-th virtue.
background
The RS→RL bridge treats Recognition Science as control theory: states are moral ledgers, admissible moves are the fourteen virtue generators, and hard physics is enforced by a σ=0 projector (LACompletion). A VirtueAction is exactly a coefficient vector in that basis. The DREAM theorem is cited in-module as guaranteeing that the fourteen virtues form a complete minimal generating set: every admissible ethical transformation factors through them, and none is redundant.
interpret is the audit face of that vector. It does not change the action; it only pairs each coefficient with its fixed string name so logs, dashboards, and multi-objective selectors can speak in virtue language rather than raw Fin 14 indices. Nearby siblings (energyCost, satisfiesTemperance, the Gibbs policy) consume the same coefficient data for thermodynamics and feasibility; this definition is the named projection used for interpretability.
proof idea
Pure definition, no proof obligations. Build List.ofFn over Fin 14, sending each index i to the pair (virtueNames i, a.coefficients i). The name table and the coefficient field are the only inputs; there is no arithmetic and no appeal to cost lemmas.
why it matters
In the bridge architecture, policies explore in the virtue basis rather than raw action space, and creativity (propose) is separated from physics (project onto σ=0). Named decomposition is what makes that separation inspectable: selectors, Gibbs sampling at temperature $T_R$, and eight-tick window evaluation (T6/T7 octave) can report which virtues were loaded and by how much.
Downstream consumers in this module include energy accounting and feasibility checks that read the same coefficients. Framework landmarks in play are the eight-tick cadence forced by T6 and the DREAM completeness claim for the virtue generators. The declaration itself is scaffolding-free bookkeeping; it does not discharge DREAM or the forcing chain, but every audited RL trace in this stack routes through it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.