virtueNames
plain-language theorem explainer
Lookup table sending each of the fourteen virtue-generator indices to a fixed English name (Love through Creativity). Downstream interpretability code cites it when decomposing a VirtueAction into named coefficient pairs. Pure pattern-match definition on Fin 14; no proof obligations.
Claim. A function $v : \{0,\ldots,13\} \to \mathrm{String}$ with $v(0)=\mathrm{Love}$, $v(1)=\mathrm{Compassion}$, $v(2)=\mathrm{Sacrifice}$, $v(3)=\mathrm{Justice}$, $v(4)=\mathrm{Temperance}$, $v(5)=\mathrm{Humility}$, $v(6)=\mathrm{Wisdom}$, $v(7)=\mathrm{Patience}$, $v(8)=\mathrm{Prudence}$, $v(9)=\mathrm{Forgiveness}$, $v(10)=\mathrm{Gratitude}$, $v(11)=\mathrm{Courage}$, $v(12)=\mathrm{Hope}$, $v(13)=\mathrm{Creativity}$.
background
The RS→RL bridge treats Recognition Science as control theory: moral states carry ledger, bonds, skew, and energy; admissible moves are spanned by fourteen virtue generators. Actions are coefficient vectors in that basis (VirtueAction), not raw environment controls.
Those fourteen generators are the complete minimal set referenced from Ethics.Virtues.Generators. This definition only names them for humans and debuggers; it does not encode dynamics, costs, or feasibility.
The module also enforces σ=0 via LACompletion projection, lexicographic multi-objective selection, and Gibbs policies with J-cost temperatures, plus eight-tick evaluation windows forced by T6.
proof idea
Definitional pattern match on Fin 14: each constructor ⟨k, _⟩ for k = 0..13 is assigned a string literal. No lemmas, tactics, or computation beyond the match.
why it matters
Feeds interpret, which builds the list of (name, coefficient) pairs for a VirtueAction so policies and audits can be read as virtue mixtures rather than anonymous ℝ¹⁴ vectors. That interpretability layer sits under the broader RS→RL design: explore in the virtue basis, project onto σ=0 feasibility, score with J-cost thermodynamics, and evaluate on eight-tick windows (T6).
It does not itself touch T5–T8 forcing, the Recognition Composition Law, or mass/α numerics; it is scaffolding for human-facing decomposition of the fourteen generators the bridge treats as complete and minimal.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.