VirtueAction
plain-language theorem explainer
A virtue action is a real 14-vector of coefficients on the virtue generators. The DREAM theorem treats those fourteen generators as a complete minimal basis for admissible ethical transformations, so the RL policy explores in coefficient space rather than raw moves. Anyone wiring Gibbs policies, temperance budgets, or LACompletion projection cites this type. It is a plain structure definition with an inhabited instance.
Claim. A virtue action is a map $a : \{0,\ldots,13\} \to \mathbb{R}$ giving real coefficients on the fourteen virtue generators. The zero action is the identity transformation in this basis. By the DREAM theorem the generators form a complete minimal set: every admissible ethical transformation decomposes into virtues, and no virtue is a composition of the others.
background
The RS→RL bridge treats Recognition Science as control theory, not philosophy. States are MoralState records (ledger, bonds, skew, energy). Admissible moves are not free vectors in an ambient action space; they live in the span of fourteen virtue generators from Ethics.Virtues.Generators, which the DREAM theorem certifies as a complete minimal generating set.
Hard physics constraints (σ=0 feasibility) are enforced downstream by LACompletion: the policy proposes coefficients, then a projector restores ledger balance. Thermodynamic selection uses a Gibbs law $p(a|s)\propto\exp(-J(s,a)/T_R)$ over these coefficient vectors, evaluated on undiscounted eight-tick windows forced by T6/T7.
Sibling operations on the type include zero (identity), Euclidean-style norm, positive scaling, addition, energy cost, and a temperance check against a φ-scaled budget. The identity recognition event (J-cost minimum at $x=1$) is the natural fixed point of the zero action.
proof idea
No proof body: this is a structure declaration. It packages a single field, a function from Fin 14 to real coefficients, and derives Inhabited so the zero vector is available as a default. Downstream lemmas (norm non-negativity, scaling homogeneity, identity projection) are proved separately against this carrier type.
why it matters
This is the action type for the entire RS→RL stack. Downstream audit goals use it directly: Gibbs weights and partition functions are positive on non-empty lists of virtue actions; LACompletion's identity projector fixes every action; temperance is the inequality energyCost ≤ budget/φ; norm is nonnegative and scales homogeneously. Compiler-correctness goals in the Recognition Stability Audit thread candidates through this representation.
Framework landmarks: the eight-tick cadence (T6/T7) fixes the evaluation window; the J-cost in the Gibbs factor is the unique T5 cost; φ appears in the temperance budget. The design separates creativity (policy proposes coefficients) from physics (LACompletion enforces σ=0), so RL never leaves the admissible cone. DREAM supplies the claim that fourteen is both enough and minimal.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.