aggCoeff_rowMoves_of_ne
plain-language theorem explainer
The theorem shows that aggregated coefficients extracted from row moves of one pair index vanish for any other pair index. Modelers maintaining block-diagonal structure in micro-move coefficient tables cite it to justify independent aggregation per pair. The proof reduces the sum to zero by proving the relevant filter is empty via the rowMoves_pair lemma and the index inequality.
Claim. Let $N$ be a normal form, $k,p$ natural numbers, and $q$ a primitive. If $k≠p$ then the sum of coefficients over all micro-moves in the row for $k$ that match pair $p$ and primitive $q$ equals zero.
background
NormalForm is the structure holding a finite-support coefficient table: supportPairs is a Finset of pair indices and coeff maps each pair and primitive to a real coefficient, with zero_outside enforcing vanishing outside the support. Primitive is the inductive type enumerating the fourteen canonical generators (Love through Sacrifice). rowMoves nf k builds the ordered list of MicroMove records whose pair field equals k and whose coefficient is nonzero. aggCoeff sums the coefficients of those moves in a list that match a given pair and primitive. The upstream rowMoves_pair lemma states that every move produced by rowMoves nf pair satisfies m.pair = pair by construction.
proof idea
The tactic proof first unfolds aggCoeff, then constructs an auxiliary fact that the filtered sublist of moves satisfying both the target pair and primitive is empty. This fact is obtained by List.filter_eq_nil_iff together with rowMoves_pair (which forces the source pair index) and the hypothesis k ≠ pair, yielding a contradiction on any candidate move. The final simp step replaces the sum over the empty list by zero.
why it matters
It supplies the off-diagonal vanishing property required by the downstream aggCoeff_flatMap theorem, which distributes aggregation over concatenated rows. The result closes a key step in the NormalForm module whose module documentation describes canonical micro-move tables supporting DREAM scaffolding. Within the Recognition framework it mirrors the separation of distinct phi-ladder rungs, ensuring aggregation respects the eight-tick octave structure without cross-talk between distinct pair indices.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.