virtueAction_norm_nonneg
plain-language theorem explainer
The Euclidean (L²) norm of any virtue-action coefficient vector is non-negative. Anyone wiring the RS→RL bridge, Gibbs policies, or energy-cost bounds would cite this elementary positivity fact. The proof unfolds the L² definition and applies non-negativity of the real square root.
Claim. For every virtue action $a$ (a real 14-tuple of coefficients on the virtue generators), the action norm $\|a\| = \sqrt{\sum_{i=0}^{13} a_i^2}$ satisfies $0 \le \|a\|$.
background
The ambient module is the RS→RL bridge: Recognition Science is treated as a control theory with MoralState, admissible virtue generators, σ=0 feasibility via LACompletion, and thermodynamic Gibbs policies. Actions are not raw moves; they are coefficient vectors on a fixed 14-generator basis.
A VirtueAction is exactly that 14-tuple of real coefficients. The DREAM theorem is cited in-module as guaranteeing the generators form a complete minimal set: every admissible ethical transformation decomposes into virtues, and none is redundant. The action norm used here is the ordinary L² norm on those coefficients: square-root of the sum of squares.
This sits beside scale, add, energyCost, and the temperance/feasibility predicates that turn the same coefficient space into an RL action representation with hard physics constraints.
proof idea
One-line term-style proof. Unfold the definition of the action norm (square root of the sum of squared coefficients over Fin 14), then apply Real.sqrt_nonneg to that sum of squares. No coefficient arithmetic or virtue-specific structure is needed; non-negativity is pure real analysis of √.
why it matters
Feeds the audit goal goal_virtueAction_norm_nonneg in the RL verification module, which is a thin wrapper re-exporting this fact under the goal namespace. Norm non-negativity is a prerequisite for treating virtue coefficients as a metric action space: energy costs, Gibbs weights ∝ exp(−J/T_R), scaling lemmas, and lexicographic selectors all assume a well-behaved non-negative size.
In the broader Recognition framework this is scaffolding hygiene rather than a forcing-chain step: it does not touch T5–T8, RCL, or the phi ladder. It does lock down the geometric side of the eight-tick cadence and virtue-basis design principles stated in the module doc, so downstream RL theorems can quote a proved non-negativity lemma instead of re-proving √≥0 at each call site.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.