aggCoeff_append
plain-language theorem explainer
The aggregation of coefficients for a fixed pair and primitive distributes over concatenation of micro-move lists. Researchers constructing normal forms for ethical micro-moves in Recognition Science cite this to compose coefficient tables from sub-sequences. The proof is a one-line term wrapper that unfolds the aggregation definition and simplifies via the append lemmas for filter, map, and sum.
Claim. Let $f(L, k, p)$ denote the sum of coefficients over all micro-moves in list $L$ whose pair index equals $k$ and whose primitive generator equals $p$. Then $f(xs ++ ys, pair, prim) = f(xs, pair, prim) + f(ys, pair, prim)$ for any lists $xs, ys$ of micro-moves.
background
The module defines canonical normal forms for micro-move coefficient tables that support DREAM scaffolding. A MicroMove is a triple consisting of a pair index, a Primitive generator (one of fourteen fixed virtues such as Love or Justice), and a real coefficient. The function aggCoeff extracts the sublist of moves matching a given pair and primitive, maps out their coefficients, and sums them. Upstream results on J-cost and ledger factorization supply the broader Recognition Science setting in which these coefficient tables appear.
proof idea
The proof is a term-mode one-liner. It applies classical reasoning, unfolds the definition of aggCoeff, and invokes simp on the three list lemmas filter_append, map_append, and sum_append.
why it matters
The lemma is invoked by aggCoeff_flatMap to justify aggregation over flat-mapped row moves inside NormalForm constructions. It supplies the additive property required for the canonical normal form of micro-move tables. In the Recognition framework this algebraic step closes the composition law for ethical primitives before they are lifted into the phi-ladder and eight-tick octave structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.