toMoves
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not include entries with zero coefficient.
- Does not reorder pairs beyond the ascending sort in pairList.
- Does not perform any coefficient aggregation or summation.
formal statement (Lean)
76noncomputable def toMoves (nf : NormalForm) : List MicroMove :=
proof body
Definition body.
77 (pairList nf).flatMap (rowMoves nf)
78
79/-- Aggregate coefficient for `(pair, primitive)` extracted from a move list. -/