norm

The RS→RL bridge treats Recognition Science as control theory: states are moral ledgers, and admissible moves are expanded in a fixed basis of fourteen virtue generators. A virtue action is exactly that coefficient vector; the DREAM theorem asserts the basis is complete and minimal, so every admissible ethical transformation decomposes uniquely into these generators.

This module therefore equips the coefficient space with elementary linear structure (zero, scale, add) and with a size functional. The natural choice is the ordinary Euclidean norm on $\mathbb{R}^{14}$. Upstream, the golden-integer field norm $N(a+b\varphi)=a^2+ab-b^2$ is a different algebraic object; the present definition is the real L² norm on virtue coefficients, not that number-field norm.

Local design goals include separate propose-then-project feasibility ($\sigma=0$ via LACompletion), lexicographic multi-objective selection, and Gibbs policies $p(a|s)\propto\exp(-J(s,a)/T_R)$ over eight-tick windows forced by T6.

Pure definition: evaluate $\sqrt{\sum_{i:\mathrm{Fin},14}(a.i)^2}$ with Mathlib's real square root and finite sum. No lemmas, no tactics, no reduction. Marked noncomputable only because Real.sqrt is.

Gives a canonical magnitude on the virtue-action space that the rest of the bridge uses for scaling, energy bookkeeping, and constraint checks (siblings include scale, energyCost, satisfiesTemperance, SigmaFeasible, LACompletion). In the RL reading, policies explore coefficient space rather than raw moves; the L² norm is the natural step-size and regularization measure on that space.

Framework-wise it sits under the DREAM completeness claim for the fourteen generators and under the eight-tick cadence (T6/T7) that forces undiscounted window evaluation. It does not itself invoke J-cost, RCL, or the forcing chain T0–T8; those enter through energy and feasibility layers that consume this norm. Downstream algebraic uses of similarly named norms (e.g. on $\mathbb{Z}[\varphi]$) are separate objects.