rowMoves_mem_of_coeff_ne_zero
plain-language theorem explainer
If a coefficient in a NormalForm is nonzero for a given pair and primitive, then the corresponding micro-move triple appears in the rowMoves list for that pair. Researchers formalizing canonical representations of ethical micro-moves cite this when checking membership in filtered coefficient tables. The proof is a direct term-mode reduction that unfolds the filterMap definition of rowMoves and applies the primitive order membership lemma together with conditional simplification.
Claim. Let $nf$ be a canonical micro-move normal form. For any pair index $pair$ and primitive generator $prim$, if the coefficient $nf.coeff(pair, prim) ≠ 0$, then the triple $⟨pair, prim, nf.coeff(pair, prim)⟩$ belongs to the list $rowMoves(nf, pair)$.
background
NormalForm is the structure for a canonical micro-move coefficient table with finite support: it carries a Finset of supported pairs together with a coefficient function from pairs and primitives to reals, plus axioms ensuring coefficients vanish outside the support and that every supported pair has at least one nonzero coefficient. Primitive is the inductive enumeration of fourteen ethical generators in fixed order (Love, Justice, Forgiveness, Wisdom, Courage, Temperance, Prudence, Compassion, Gratitude, Patience, Humility, Hope, Creativity, Sacrifice). The module develops Micro-Move Normal Forms to supply canonical representations supporting DREAM scaffolding. rowMoves is the auxiliary definition that builds, for a fixed pair, the ordered list of MicroMove triples by filterMap over primitiveOrderList, retaining only those primitives whose coefficient is nonzero. The lemma depends on primitive_mem_order, which states that every primitive appears in the canonical ordered list.
proof idea
The term proof begins with classical, unfolds rowMoves, and reduces membership in the filterMap via simp. It supplies the witness prim together with the lemma primitive_mem_order prim, then simplifies the ite condition under the nonzero hypothesis to retain the move in the resulting list.
why it matters
The result is used by mem_toMoves_of_coeff_ne_zero to lift the membership statement from a single row to the full toMoves list. It supplies the basic membership fact required by the normal-form construction in the Ethics.Virtues.NormalForm module, thereby supporting the DREAM scaffolding for micro-move coefficient tables. No open questions are addressed; the lemma closes a routine verification step inside the canonical-form machinery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.