rowMoves_pair
plain-language theorem explainer
The theorem establishes that every micro-move extracted for a given pair index from a normal form's coefficient table has its pair field equal to that index. Researchers aggregating coefficients across micro-move rows cite it to guarantee isolation between distinct pair scopes. The proof unfolds the filterMap definition of rowMoves and performs case analysis on coefficient zero/nonzero to confirm the pair component by construction.
Claim. Let $nf$ be a normal form and $pair$ a natural number. For any micro-move $m$ belonging to the list of row moves generated by $nf$ for $pair$, the pair component of $m$ equals $pair$.
background
A NormalForm consists of a finite support set of pair indices together with a coefficient map from pairs and primitives to reals, required to vanish outside the support and to be nontrivial on the support. A MicroMove is the triple (pair index, primitive, real coefficient). The auxiliary definition rowMoves builds, for a fixed pair, the ordered list of such triples by filterMap over the canonical primitive list, emitting a move only when the stored coefficient is nonzero.
proof idea
The term proof first invokes classical logic, unfolds rowMoves, and simplifies the membership predicate to a filterMap condition. It obtains the underlying primitive and the equality produced by the constructor, then cases on whether the coefficient at that pair and primitive is zero. The zero branch yields an immediate contradiction with membership; the nonzero branch yields the required equality by the definition of MicroMove.mk.
why it matters
The result is invoked directly by aggCoeff_rowMoves_of_ne to conclude that row moves belonging to one pair contribute zero to aggregation for any other pair, and it underpins the companion aggregation lemma aggCoeff_rowMoves. It supplies the scope-isolation property required for consistent coefficient tables in the DREAM scaffolding of the Recognition framework, ensuring that pair-wise rows remain independent under the eight-tick octave and related aggregation steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.