sumCoeffs_toMoves
plain-language theorem explainer
The lemma shows that the aggregated coefficient extracted from the move list generated by toMoves recovers exactly the stored coefficient table entry in a NormalForm for any pair and primitive. Researchers verifying round-trip properties of micro-move representations in ethical modeling would cite this result. The proof proceeds by unfolding toMoves, applying the flat-map aggregation theorem, and splitting cases on membership in the support list.
Claim. Let $nf$ be a normal form. For any pair $p$ and primitive $prim$, the sum of coefficients over moves matching $(p, prim)$ in the list produced by $toMoves(nf)$ equals the value $nf.coeff(p, prim)$.
background
A NormalForm is a structure holding a finite Finset of support pairs together with a coefficient function from pairs and primitives to reals; it satisfies zero_outside (coefficients vanish outside the support) and nontrivial (each supported pair has a nonzero primitive entry). Primitives form an inductive type of fourteen fixed virtues in canonical order. The pairList definition yields the sorted ascending list of those support pairs. The aggCoeff definition sums the coefficients of all moves in a list that match a given pair and primitive. Upstream lemmas establish that aggregation commutes with flat-mapping over row moves and that the row-moves list for a supported pair recovers the stored coefficient exactly.
proof idea
The tactic proof first invokes classical reasoning and unfolds toMoves. It obtains the flat-map aggregation equality via aggCoeff_flatMap using the nodup property of pairList. Case analysis on whether the pair lies in pairList nf then applies aggCoeff_rowMoves when membership holds, or the zero_outside property of nf when it fails, with both cases simplified through the flat-map result.
why it matters
This lemma supplies the coefficient equality needed inside of_toMoves, the round-trip theorem that recovers the original NormalForm after conversion to moves and back. It thereby confirms faithful representation of finite-support coefficient tables under the micro-move encoding, closing a verification step for the DREAM scaffolding in the ethics module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.