scale
plain-language theorem explainer
Coefficient-wise scaling of a 14-dimensional virtue action by a real factor. Anyone building the RS→RL action algebra (linear combinations of virtue generators, Gibbs policies, LACompletion) cites this. The body is a one-line structure constructor: multiply each Fin-14 coefficient by the scalar.
Claim. Given a virtue action $a$ (a map from $\{0,\ldots,13\}$ to $\mathbb{R}$ giving coefficients on the 14 virtue generators) and a scalar $c\in\mathbb{R}$, the scaled action has coefficients $i\mapsto c\,a_i$.
background
The RS→RL bridge treats Recognition Science as control theory: states are moral ledgers, and admissible moves are spanned by a fixed basis of 14 virtues. A VirtueAction is exactly that coefficient vector. The DREAM theorem is invoked in-module to claim the basis is complete and minimal, so the RL policy outputs these 14 numbers rather than raw environment moves.
This definition sits next to zero, add, and norm in the same namespace, giving the obvious real-vector-space operations on actions. The module then feeds scaled and summed actions into energy cost, temperance checks, σ=0 projection (LACompletion), and the Gibbs policy $p(a|s)\propto\exp(-J(s,a)/T_R)$. Eight-tick cadence (T7/T6 landmark) governs the evaluation window; no discount factor is introduced.
proof idea
Pure definition, not a proof. The structure is rebuilt by pointwise multiplication: the new coefficient function is $i\mapsto c\cdot a.\mathrm{coefficients}(i)$. No lemmas are applied.
why it matters
Gives the scalar multiplication half of the linear structure on virtue actions, without which linear combinations, step-size schedules, and tempered Gibbs sampling cannot be stated inside the bridge. Downstream in-module consumers include energy cost, feasibility (SigmaFeasible / LACompletion), and the lexicographic selector. Framework role is instrumental rather than foundational: it does not touch T5 J-uniqueness, RCL, or the mass ladder; it only equips the RL layer that reuses those objects. Name collisions with unrelated scale defs (φ-ladder cosmology scale, etc.) exist elsewhere in the monolith; this one is local to VirtueAction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.