aggCoeff_rowMoves_aux_theorem
plain-language theorem explainer
The auxiliary lemma establishes that the sum of coefficients drawn from micro-moves filtered by a fixed pair and primitive recovers exactly the normal-form coefficient when the primitive lies in the canonical order list. Researchers maintaining aggregation identities inside ethical coefficient tables invoke the identity to collapse filtered sums. The proof proceeds by case analysis on coefficient vanishing, using filter-congruence and membership lemmas to show the filtered list is either empty or a singleton.
Claim. Let $nf$ be a normal form, $p$ a natural number, and $q$ a primitive. Then the sum of the coefficients of all micro-moves of the form $(p, r, nf.coeff(p,r))$ with $r=q$ equals $nf.coeff(p,q)$ whenever $q$ belongs to the canonical primitive order list, and equals zero otherwise.
background
The module constructs canonical normal forms for micro-move coefficient tables that support DREAM scaffolding. NormalForm is the structure whose fields are a finite support set of pair indices and a coefficient map from pairs and primitives to reals, required to vanish outside the support and to be nontrivial on it. Primitive is the inductive type enumerating the fourteen generators (Love, Justice, Forgiveness, Wisdom, Courage, Temperance, Prudence, Compassion, Gratitude, Patience, Humility, Hope, Creativity, Sacrifice) equipped with the fixed list primitiveOrderList. MicroMove packages a triple (pair, primitive, coefficient).
proof idea
The tactic proof first applies primitive_mem_order to replace the membership conditional by the true branch. It defines the moves list via filterMap on nonzero coefficients, proves every element carries the input pair, then shows the pair-and-primitive filter is equivalent to the primitive-only filter by congruence. Case split on whether the target coefficient vanishes: the zero case produces an empty filtered list whose sum is zero; the nonzero case produces a unique matching move, shows the filter yields exactly the singleton containing that move, and concludes the sum equals the coefficient.
why it matters
The lemma supplies the identity required by the downstream backward-compatibility alias aggCoeff_rowMoves_aux_axiom inside the same module. It closes a bookkeeping step in the micro-move normal-form construction whose module documentation explicitly ties the forms to DREAM scaffolding. No open questions are indicated; the result is fully discharged with no remaining hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.