aggCoeff_rowMoves_aux
plain-language theorem explainer
The lemma equates the summed coefficients of filtered micro-moves for a fixed pair and primitive to the normal form table entry when the primitive lies in the canonical list, and to zero otherwise. Researchers formalizing coefficient aggregation in ethical normal forms cite it to recover stored values from move lists. The proof is a direct one-line term application of the auxiliary axiom.
Claim. Let $nf$ be a normal form, $p$ a natural number, and $q$ a primitive. Then the sum of coefficients over micro-moves with pair $p$ and primitive $q$ equals $nf.coeff(p,q)$ if $q$ belongs to the canonical primitive list, and equals zero otherwise.
background
NormalForm is the structure for a canonical micro-move coefficient table with finite support: it carries a Finset of support pairs together with a function coeff from pairs and primitives to reals, required to vanish outside the support and to be nontrivial on each supported pair. Primitive is the inductive enumeration of fourteen fixed generators in canonical order: Love, Justice, Forgiveness, Wisdom, Courage, Temperance, Prudence, Compassion, Gratitude, Patience, Humility, Hope, Creativity, Sacrifice. MicroMove packages a triple (pair, primitive, coefficient). The module develops these objects to supply canonical normal forms for micro-move tables that support DREAM scaffolding.
proof idea
The proof is a one-line term wrapper that applies the axiom aggCoeff_rowMoves_aux_axiom directly to the three arguments nf, pair, and prim.
why it matters
The lemma is invoked by the parent result aggCoeff_rowMoves, which equates the aggregated coefficient extracted from rowMoves to the stored table value. It supplies the aggregation identity required for coefficient tables in the ethics virtues normal-form module. Within the Recognition Science framework the construction maintains consistency with the micro-move representation used for DREAM scaffolding, though it does not invoke the T0-T8 forcing chain or the Recognition Composition Law directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.