zero
plain-language theorem explainer
The zero virtue action is the 14-coefficient vector with every entry zero, i.e. the identity ethical transformation. Anyone building policies, norms, or Gibbs distributions over virtue generators cites it as the neutral element. The definition is a one-line structure constructor.
Claim. The zero action is the virtue action whose coefficient map $i \mapsto 0$ for every $i \in \{0,\ldots,13\}$, representing the identity transformation on moral states.
background
The RS→RL bridge treats Recognition Science as control theory: states are moral ledgers, and admissible moves are spanned by a fixed basis of 14 virtues. By the DREAM theorem that basis is complete and minimal, so every ethical transformation decomposes uniquely into virtue coefficients and no generator is redundant.
A virtue action is therefore just a map $\mathrm{Fin},14 \to \mathbb{R}$. The RL policy outputs those coefficients rather than raw environment moves; hard physics constraints (σ=0 feasibility) are enforced later by LACompletion projection. The zero vector is the algebraic identity in that coefficient space.
The module also equips actions with an $L^2$ norm, scalar scaling, and addition, so the zero element is the natural origin for those operations and for energy-cost comparisons.
proof idea
Pure definitional construction: build a VirtueAction whose coefficients field is the constantly-zero function on Fin 14. No lemmas or tactics are required.
why it matters
In the RS→RL stack, policies explore in the virtue basis and thermodynamic learning uses Gibbs weights $p(a|s)\propto\exp(-J(s,a)/T_R)$. The zero action is the identity baseline against which energy cost, temperance, and lexicographic selection are measured. It anchors the eight-tick cadence evaluation forced by T6 and keeps the propose-then-project split well-typed: the policy may emit zero, and LACompletion leaves the identity feasible when σ is already zero. No downstream theorems currently depend on it in the graph, but sibling operations (norm, scale, add, energyCost) treat it as the neutral element of the action monoid.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.