rowMoves
plain-language theorem explainer
The rowMoves definition extracts the ordered list of nonzero micro-moves for one pair from a NormalForm coefficient table by filtering the fixed primitive list. Workers on ethical normal forms and DREAM scaffolding cite it when converting tables to move sequences for aggregation. The definition is a direct filterMap that builds MicroMove records only for nonzero coefficients and drops the rest.
Claim. For a normal form $nf$ and integer pair $n$, rowMoves$(nf,n)$ returns the list of triples $(n,p,c)$ where $p$ runs over the canonical primitive order and $c=coeff(nf,n,p)$ is nonzero.
background
NormalForm is the structure holding a finite set of supported pairs together with a coefficient function from pairs and primitives to reals, required to vanish outside the support and to be nontrivial on each supported pair. MicroMove packages one triple (pair, primitive, coefficient). The module works inside the micro-move normal-form machinery that supports DREAM scaffolding for ethical coefficient tables. primitiveOrderList supplies the fixed ascending list of fourteen primitives used for canonical ordering.
proof idea
The definition is a one-line filterMap over primitiveOrderList. For each primitive it checks whether the stored coefficient is zero and emits a MicroMove record containing the pair, primitive, and coefficient only when the coefficient is nonzero.
why it matters
rowMoves supplies the row decomposition used by aggCoeff_rowMoves to recover stored coefficients and by ofMicroMoves to reconstruct normal forms from move lists. It implements the micro-move extraction step inside the NormalForm machinery for ethical virtues, directly supporting the DREAM scaffolding described in the module doc. The definition closes the loop between table representation and list representation in the ethics layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.