aggCoeff_rowMoves
plain-language theorem explainer
The lemma shows that the aggregated coefficient extracted from row moves generated for a given pair in a NormalForm recovers exactly the stored coefficient table entry for that pair and primitive. Developers of micro-move ethical models cite it when verifying that row extraction preserves table values. The short proof invokes an auxiliary aggregation lemma after confirming membership in the canonical primitive order list.
Claim. Let $nf$ be a NormalForm, $p$ a natural number, and $q$ a Primitive. Then the sum of coefficients over the list of micro-moves produced by rowMoves for pair $p$, filtered to those with primitive $q$, equals the value of the coefficient function of $nf$ at $(p,q)$.
background
The module introduces canonical micro-move normal forms as coefficient tables with finite support, intended to support DREAM scaffolding. NormalForm is the structure with a Finset of support pairs and a function coeff : ℕ → Primitive → ℝ obeying zero_outside (vanishes off the support) and nontrivial (nonzero somewhere on each supported pair). Primitive is the inductive enumeration of fourteen generators in fixed order: Love, Justice, Forgiveness, Wisdom, Courage, Temperance, Prudence, Compassion, Gratitude, Patience, Humility, Hope, Creativity, Sacrifice. aggCoeff sums the coefficients of moves whose pair and primitive fields match the query arguments.
proof idea
One-line wrapper that applies aggCoeff_rowMoves_aux. The proof opens with classical, obtains the membership fact prim ∈ primitiveOrderList via the lemma primitive_mem_order, then uses simpa with the definitions of aggCoeff and rowMoves to reduce directly to the auxiliary statement.
why it matters
The result guarantees that row extraction from a NormalForm is faithful to the stored table, supplying the key step used by sumCoeffs_toMoves to confirm that the full toMoves construction recovers the original coefficients. It therefore closes an internal consistency check inside the NormalForm construction for ethical virtue modeling. The module positions these forms as the canonical representation supporting DREAM scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.