aggCoeff
plain-language theorem explainer
aggCoeff extracts the summed real coefficient for one pair index and one primitive generator from an arbitrary list of micro-moves. Workers constructing NormalForm tables from raw move sequences cite it when populating coefficient fields or proving aggregation lemmas. The definition is a single filter-map-sum expression over the input list using standard list operations.
Claim. Let $M$ be a finite list of triples $(p_i, q_i, c_i)$ where each $p_i$ is a natural number, each $q_i$ belongs to the fixed set of fourteen primitive generators, and each $c_i$ is real. For fixed $p$ and $q$, the aggregated coefficient is the sum of all $c_i$ such that $(p, q, c_i)$ appears in $M$.
background
MicroMove is the structure carrying a pair scope, a primitive generator, and a real coefficient. Primitive is the inductive enumeration of fourteen canonical generators (Love, Justice, Forgiveness, Wisdom, Courage, Temperance, Prudence, Compassion, Gratitude, Patience, Humility, Hope, Creativity, Sacrifice) in fixed order. NormalForm is the structure whose fields are a finite support set of pairs together with a coefficient table that vanishes outside the support and is nontrivial on the support.
proof idea
One-line definition that filters the input list to retain only those moves whose pair and primitive fields match the arguments, maps the retained moves to their coefficients, and returns the sum of that list.
why it matters
aggCoeff supplies the coefficient function passed to ofMicroMoves when NormalForm is built from a move list. It is invoked by the distributivity lemma aggCoeff_append, the recovery lemma aggCoeff_rowMoves, and the flat-map theorem aggCoeff_flatMap. The definition therefore closes the loop between raw micro-move data and the canonical coefficient table required by DREAM scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.