ofMicroMoves_zero_outside
plain-language theorem explainer
The theorem shows that for any list of micro-moves the aggregated coefficient for a pair vanishes whenever that pair lies outside the finite set of pairs carrying at least one nonzero primitive coefficient. Workers building NormalForm instances from move lists in the ethics module cite the result to confirm the zero_outside axiom. The proof runs by contraposition: a nonzero coefficient produces a nonempty filtered sublist whose witness move places the pair inside the mapped support set.
Claim. Let $M$ be a list of micro-moves. Let $S$ be the finite set of pair indices $k$ such that there exists a primitive $p$ with aggregated coefficient of $(k,p)$ in $M$ nonzero. Then for every pair index $q$ outside $S$ and every primitive $r$, the aggregated coefficient of $(q,r)$ in $M$ equals zero.
background
MicroMove records a pair index (natural number), a primitive, and a real coefficient. aggCoeff extracts the sum of coefficients over all moves in the list that match a given pair and primitive. NormalForm is the structure whose supportPairs field is a finite set of indices, whose coeff field is the table of aggregated values, and whose zero_outside field requires the table to vanish on pairs outside the support. The module develops canonical normal forms for micro-move coefficient tables that support DREAM scaffolding.
proof idea
The proof assumes the pair is absent from the filtered support set and proceeds by contradiction on a nonzero aggregated coefficient. It first shows that the nonzero assumption yields a nonempty filtered sublist of matching moves. An element is extracted from this sublist and mapped to establish membership of the pair in the image of the move list; the existential witness for the filter predicate is supplied directly by the nonzero coefficient.
why it matters
The result supplies the zero_outside field required by the ofMicroMoves definition that assembles a NormalForm from an arbitrary list of micro-moves. It thereby guarantees that every such construction yields a well-formed NormalForm object. In the Recognition framework the construction furnishes the coefficient tables used for virtue modeling and DREAM scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.