virtueAction_scale_norm
plain-language theorem explainer
Scaling a virtue-action vector by a nonnegative scalar multiplies its Euclidean coefficient-norm by that same scalar. Anyone setting RL step sizes, temperature schedules, or Gibbs weights over the 14-virtue basis cites this homogeneity. The proof unfolds the L2 definition, factors c squared from the finite sum of squares, and takes square roots under c ≥ 0.
Claim. Let $a$ be a virtue action (a real 14-vector of coefficients on the virtue generators) and let $c\ge 0$. Write $\|a\|_2=\sqrt{\sum_{i=0}^{13}a_i^2}$ and $(c\cdot a)_i=c\,a_i$. Then $\|c\cdot a\|_2=c\,\|a\|_2$.
background
The RS→RL bridge treats Recognition Science as a control theory: states are moral ledgers, and admissible moves are expanded in a fixed 14-dimensional virtue basis. A virtue action is exactly that coefficient vector. The DREAM theorem is invoked in-module to justify completeness and minimality of the generators, so the RL policy outputs these coefficients rather than raw environment moves.
The action norm is ordinary Euclidean length on the fourteen coefficients. Scaling multiplies every coefficient by a real factor $c$. Homogeneity of this norm under nonnegative scaling is the elementary linear-algebra fact recorded here; it is independent of the ethical interpretation of the basis.
Upstream, the same module defines the zero action, coefficient-wise addition, and the LACompletion projector onto the $\sigma=0$ feasible set. Those structures use the norm as a size measure when ranking or regularizing proposals.
proof idea
Unfold the definitions of scale and norm. The squared-sum identity
$\sum_i (c a_i)^2 = c^2\sum_i a_i^2$
is obtained by pulling $c^2$ out of the finite sum (Finset.mul_sum) and simplifying each term by ring. Rewrite the outer square root as $\sqrt{c^2\cdot S}$, apply Real.sqrt_mul with $c^2\ge 0$, then Real.sqrt_sq using the hypothesis $c\ge 0$ to recover the factor $c$.
why it matters
The RL audit re-exports this fact as goal_virtueAction_scale_norm, a named stability goal for the virtue-action interface. Homogeneous scaling is required before one can treat step-size or temperature as a free positive parameter without distorting relative action magnitudes in the Gibbs policy $p(a|s)\propto\exp(-J(s,a)/T_R)$.
In the broader Recognition framework the 14-virtue basis is the admissible-move algebra feeding the eight-tick evaluation window (T6/T7 cadence). This lemma does not itself invoke the forcing chain or the J-cost; it only certifies that the RL action metric behaves as an ordinary norm under positive rescaling, so later multi-objective and thermodynamic selectors can quote a clean size relation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.