toMoves
plain-language theorem explainer
toMoves produces the canonical ordered list of micro-moves from a NormalForm coefficient table by flattening rowMoves over the sorted support pairs. Researchers working on DREAM scaffolding cite it when converting between normal forms and explicit move sequences for aggregation or round-tripping. The definition is a direct one-line composition via flatMap on pairList and rowMoves.
Claim. For a normal form $nf$ with finite support pairs and coefficient map from pairs and primitives to reals, toMoves$(nf)$ returns the concatenated list of triples $(p, prim, c)$ where $p$ runs over the ascending pairList$(nf)$ and $c = nf.coeff(p, prim) > 0$.
background
NormalForm is the structure holding supportPairs as a Finset of naturals together with a coefficient function from pairs and primitives to reals, subject to the zero-outside-support and nontriviality axioms. MicroMove packages the triple of pair, primitive, and real coefficient. The module supplies canonical normal forms for micro-move coefficient tables that support DREAM scaffolding.
proof idea
The definition is a one-line wrapper that applies flatMap to pairList nf using the rowMoves function.
why it matters
toMoves supplies the move-list representation required by of_toMoves for the round-trip theorem and by sumCoeffs_toMoves together with aggCoeff_flatMap for coefficient recovery. It completes the list-construction step in the NormalForm machinery of the ethics module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.