mem_toMoves_of_coeff_ne_zero
plain-language theorem explainer
Non-zero coefficients for a primitive in a supported pair of a NormalForm ensure the corresponding triple appears in the toMoves list. Researchers modeling ethical micro-moves would cite this when confirming that coefficient tables generate complete move sets. The term proof unfolds toMoves, pulls pair membership from pairList_mem, and feeds the non-zero coefficient into rowMoves_mem_of_coeff_ne_zero via List.mem_flatMap.
Claim. Let $nf$ be a NormalForm with finite supportPairs and coefficient function. For any pair $p$ in the support and primitive $q$ with $nf.coeff(p,q)neq0$, the triple $langle p,q,nf.coeff(p,q)rangle$ belongs to toMoves($nf$).
background
NormalForm is the structure holding a finite support set of pairs (supportPairs : Finset ℕ) together with a coefficient map (coeff : ℕ → Primitive → ℝ) that is zero outside the support and nontrivial on each supported pair. Primitive is the inductive enumeration of fourteen fixed generators (Love, Justice, Forgiveness, Wisdom, Courage, Temperance, Prudence, Compassion, Gratitude, Patience, Humility, Hope, Creativity, Sacrifice). pairList returns the sorted ascending list of supportPairs, and pairList_mem equates membership in that list with membership in the support finset. toMoves is obtained by flat-mapping rowMoves over pairList, where rowMoves for a given pair collects the non-zero coefficient triples.
proof idea
The term proof invokes classical, unfolds toMoves, obtains the pair membership via pairList_mem, and applies List.mem_flatMap.mpr to the pair together with the membership statement supplied by rowMoves_mem_of_coeff_ne_zero.
why it matters
The lemma guarantees faithful inclusion of every non-zero contribution inside toMoves, supplying the key membership fact used by the downstream pair_mem_toMoves_map. It completes the interface for NormalForm inside the Micro-Move Normal Forms module, whose canonical tables support DREAM scaffolding. No open scaffolding remains; the membership direction for the normal form is now closed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.