add
plain-language theorem explainer
Coefficient-wise sum of two virtue actions, each a 14-vector over the DREAM generators. Anyone building linear combinations, convex mixtures, or policy updates in the RS→RL bridge cites this. The body is a one-line structure constructor: add the real coefficients pointwise on Fin 14.
Claim. Given two virtue actions $a,b$, each a map $\mathrm{Fin}\,14\to\mathbb{R}$ of coefficients on the fourteen virtue generators, their sum is the virtue action whose $i$-th coefficient is $a_i+b_i$.
background
The RS→RL bridge treats Recognition Science as control theory: states are moral ledgers, and admissible moves are expanded in a fixed basis of fourteen virtues. A VirtueAction is exactly that coefficient vector (Fin 14 → ℝ). The DREAM theorem is invoked in the module as guaranteeing this basis is a complete minimal generating set: every admissible ethical transformation decomposes into virtues, and none is redundant.
The module therefore explores policies in virtue-coefficient space rather than raw action space, then projects onto the σ=0 feasible set via LACompletion. Pointwise addition is the abelian-group operation that lets one form sums, averages, and residual updates of such coefficient vectors before projection or Gibbs scoring.
Local companions include the zero action (identity), scalar scaling, and an energy-cost functional; together they make the coefficient space a real vector space of actions aligned with the ethical generators.
proof idea
Definitional one-liner. The structure is unpacked and rebuilt with coefficients $i \mapsto a.coefficients,i + b.coefficients,i$. No lemmas are applied; Lean’s anonymous constructor supplies the resulting VirtueAction.
why it matters
Gives the additive structure on the virtue-action space that the RS→RL bridge needs for linear combinations of generators, residual policy steps, and multi-objective mixing before LACompletion and the lexicographic selector. It sits under the module’s design rule that RL explores in the DREAM virtue basis, not raw moves, and pairs with zero and scale to make that basis a real vector space. Downstream usage is not yet wired in this audit graph (used_by empty), but the operation is the natural sum for Gibbs-policy updates and eight-tick window aggregates forced by T6. It does not itself encode ethics or feasibility; those live in interpret, energyCost, SigmaFeasible, and LACompletion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.