goal_virtueAction_zero_norm
plain-language theorem explainer
The zero virtue action (all fourteen coefficients zero) has Euclidean norm zero. RSA RL trainers and auditors cite this as a canonical gold goal for the whitelist tactics. The proof is a one-line wrapper of the underlying norm identity.
Claim. If $A_0$ is the zero virtue action (the $14$-vector of coefficients all equal to $0$), then its action norm satisfies $\|A_0\|_2 = 0$, where the norm is the Euclidean $L^2$ norm on coefficients.
background
In the RSA-to-RL bridge, a virtue action is a real $14$-vector of coefficients on a fixed generating set of ethical transformations. The DREAM theorem is cited upstream as guaranteeing that this set is a complete minimal basis: every admissible ethical map factors through these virtues, and none is redundant.
The action norm is the ordinary Euclidean norm on those coefficients: $\sqrt{\sum_{i=0}^{13} c_i^2}$. The zero action is the vector with every $c_i = 0$. (A separate GoldenInt field norm $N(a+b\varphi)=a^2+ab-b^2$ appears in the dependency graph but is not used in this identity.)
This module packages Recognition Stability Audit lemmas as RL-friendly gold goals and whitelisted simp/milestone tags, so an external policy can propose rsa_step/rsa_simp moves and receive a Lean reward on goal closure.
proof idea
One-line term wrapper: the goal is exactly the statement of virtueAction_zero_norm, which unfolds the action norm and the zero action and closes by simp (sum of squares of zeros is zero, square root of zero is zero). No extra algebraic work occurs at this layer.
why it matters
This is one of the module's canonical training goals: a proved, sorry-free gold theorem that exercises the RSA RL pipeline without touching physics constants or the forcing chain. Downstream use is empty in the graph; its role is pedagogical and operational for the audit loop rather than a step in T0–T8.
It anchors the basic sanity check that the policy's null action is costless under the $L^2$ action norm, which is the natural baseline before scaling, composition, or obstruction lemmas in the same RL library. It does not itself invoke J-cost, phi-ladder masses, or eight-tick structure; those live elsewhere in the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.