aggCoeff_flatMap
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
claimLet $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 in Recognition Science
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.
scope and limits
- Does not apply when the input list contains duplicate pairs.
- Does not compute explicit numerical coefficient values.
- Does not address ordering among primitives inside a row.
- Does not extend beyond the coefficient extraction defined by aggCoeff.
Lean usage
have hflat := aggCoeff_flatMap (nf := nf) (pair := pair) (prim := prim) (l := pairList nf) (hl := pairList_nodup nf)formal statement (Lean)
375theorem aggCoeff_flatMap (nf : NormalForm) (pair : ℕ) (prim : Primitive)
376 (l : List ℕ) (hl : l.Nodup) :
377 aggCoeff (l.flatMap (rowMoves nf)) pair prim
378 = if pair ∈ l then aggCoeff (rowMoves nf pair) pair prim else 0 := by
proof body
Term-mode proof.
379 induction l with
380 | nil =>
381 simp only [List.flatMap_nil, List.not_mem_nil, ↓reduceIte]
382 unfold aggCoeff
383 simp
384 | cons h t ih =>
385 simp only [List.flatMap_cons]
386 rw [aggCoeff_append]
387 have hnodup_t : t.Nodup := hl.of_cons
388 have h_not_mem : h ∉ t := hl.not_mem
389 by_cases hpair : pair = h
390 · -- pair = h: contribution comes from rowMoves nf h, and pair ∉ t (since h ∉ t)
391 subst hpair
392 simp only [List.mem_cons, true_or, ↓reduceIte]
393 have h_pair_not_in_t : pair ∉ t := h_not_mem
394 rw [ih hnodup_t]
395 simp only [h_pair_not_in_t, ↓reduceIte, add_zero]
396 · -- pair ≠ h: contribution from rowMoves nf h is 0
397 have h_ne : h ≠ pair := Ne.symm hpair
398 rw [aggCoeff_rowMoves_of_ne nf h_ne]
399 simp only [zero_add]
400 rw [ih hnodup_t]
401 -- pair ∈ h :: t ↔ pair = h ∨ pair ∈ t, but pair ≠ h, so pair ∈ h :: t ↔ pair ∈ t
402 simp only [List.mem_cons, hpair, false_or]
403
404/-- Aggregated coefficient extracted from `toMoves` equals the canonical table. -/