aggCoeff_flatMap
plain-language theorem explainer
The theorem states that for a normal form with coefficient table c, the aggregated coefficient over the flat-mapped row moves from a duplicate-free list l of pairs equals the single-row aggregation for that pair if the pair belongs to l, and zero otherwise. Researchers formalizing canonical micro-move tables for virtue coefficients in the ethics module cite it to justify summation simplifications. The proof proceeds by induction on l, splitting on membership at the cons step and invoking append distributivity together with the row non-contribut
Claim. Let $nf$ be a normal form with coefficient function $c$. Let $l$ be a duplicate-free list of pairs. Then the aggregated coefficient over the concatenation of row moves for each pair in $l$, evaluated at a target pair and primitive, equals the row aggregation for that pair when the target belongs to $l$, and equals zero otherwise.
background
A NormalForm is a structure consisting of a finite Finset of support pairs together with a coefficient map from pairs and Primitive values to reals; the map vanishes outside the support and is nontrivial on the support. Primitive is the inductive enumeration of fourteen canonical virtues (Love through Sacrifice) in fixed order. rowMoves(nf, p) builds the list of MicroMove records carrying the nonzero coefficients for pair p. aggCoeff sums the coefficients of those moves in a list that match a given pair and primitive.
proof idea
Proof by induction on the list l. The nil case simplifies directly to zero. For the cons case the flatMap is rewritten via append; the induction hypothesis is applied after a case split on whether the target pair equals the head. When equal, the tail hypothesis is used after confirming absence from the tail. When unequal, aggCoeff_rowMoves_of_ne sets the head contribution to zero before the hypothesis is invoked.
why it matters
The result is the key step inside sumCoeffs_toMoves, which recovers the original coefficient table from the aggregated toMoves list. It therefore guarantees that the list representation of micro-moves is faithful to the canonical NormalForm table, closing the representation loop required for DREAM scaffolding in the ethics module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.