virtueAction_zero_norm
plain-language theorem explainer
The zero virtue action (all fourteen coefficients zero) has Euclidean L² norm zero. Anyone checking basic metric axioms on the RS-to-RL action space, or wiring the virtue-coefficient policy layer, would cite this. The proof is a two-step unfold-and-simp of the coefficient-sum definition.
Claim. Let $a_0$ be the zero virtue action, i.e. the coefficient map $i \mapsto 0$ on $\mathrm{Fin}\,14$. Its action norm satisfies $\|a_0\|_2 = 0$, where $\|a\|_2 = \sqrt{\sum_{i=0}^{13} a_i^2}$.
background
The RS→RL bridge treats Recognition Science as a control theory: states are moral ledgers, and admissible moves are spanned by fourteen virtue generators (DREAM completeness and minimality). A virtue action is exactly a real 14-vector of coefficients on that basis; the RL policy outputs those coefficients rather than raw environment moves.
The action norm used here is the ordinary Euclidean L² norm on coefficients: square-root of the sum of squares. The zero action is the identity transformation in that basis (every coefficient zero). This sits beside scale, add, energy cost, and σ=0 feasibility projection (LACompletion) in the same module.
Upstream, the GoldenInt field norm $N(a+b\varphi)=a^2+ab-b^2$ is a different object; the depends edge is only name-sharing. The local norm is the real L² map on VirtueAction.
proof idea
Term-style tactic proof in two steps. Unfold the local action-norm definition (square root of sum of squared coefficients) and the zero-action constructor (constant-zero coefficient map). Then simp discharges the resulting identity $\sqrt{\sum_i 0^2}=0$. No external lemmas beyond definitional reduction.
why it matters
Feeds the audit goal goal_virtueAction_zero_norm in the RL verification module, which re-exports the same identity as a named checklist item. That goal sits next to non-negativity of the norm and other basic metric facts the stability audit expects before Gibbs policies and lexicographic selectors are trusted.
In the broader RS→RL design, actions live in a virtue basis forced by the DREAM theorem (complete minimal generators), with eight-tick evaluation windows from T6/T7. Zero-norm of the identity is the trivial base case for energy-cost and temperance checks that treat norm as a magnitude of ethical intervention. It does not itself invoke J-cost, φ-ladder masses, or the forcing chain T0–T8 beyond the module’s stated eight-tick cadence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.