ofMicroMoves
plain-language theorem explainer
ofMicroMoves assembles a NormalForm from an arbitrary list of micro-moves by aggregating coefficients per pair and primitive then restricting support to pairs with at least one nonzero total. Ethics researchers modeling DREAM scaffolding invoke the constructor to obtain canonical coefficient tables from raw move sequences. The definition is a direct structure literal that delegates the support filter to the aggregation function and fills the two axioms via companion lemmas.
Claim. Given a list of triples $(p, π, c)$ with $p ∈ ℕ$, $π$ a primitive, and $c ∈ ℝ$, the map returns the normal form whose support is the finite set of pairs $p$ for which there exists a primitive with nonzero aggregated coefficient, whose coefficient function is the aggregation map, and which satisfies the zero-outside and nontrivial axioms.
background
MicroMove is the structure that records one elementary action as the triple (pair, primitive, coeff) where pair is a natural-number scope index, primitive is drawn from the ordered list of primitives, and coeff is a real multiplier. NormalForm packages a coefficient table as a finite support set of pairs together with a function from pairs and primitives to reals, subject to the two axioms that the function vanishes outside the support and that every pair in the support has a nonzero coefficient for some primitive. The module develops these objects under the heading of micro-move normal forms to support DREAM scaffolding.
proof idea
The definition is a structure constructor. It sets supportPairs to the filtered finset of pairs that appear in the move list and possess at least one primitive with nonzero aggCoeff. The coeff field is set directly to the aggCoeff function. The zero_outside and nontrivial fields are discharged by the companion lemmas ofMicroMoves_zero_outside and ofMicroMoves_nontrivial.
why it matters
This definition supplies the forward map from move lists to normal forms. It is invoked inside the round-trip theorem of_toMoves, which states that applying toMoves followed by ofMicroMoves recovers the original normal form. The construction therefore completes the canonical representation loop required for coefficient tables in the DREAM scaffolding of the ethics module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.