pair_mem_toMoves_map
plain-language theorem explainer
If a pair lies in the support of a normal form and its coefficient for a given primitive is nonzero, then the pair appears in the finite set of pairs extracted from the toMoves conversion. Researchers verifying round-trip properties of micro-move coefficient tables in virtue modeling cite this membership fact. The proof obtains the explicit micro-move via the non-zero coefficient lemma, then applies the list map membership rule and Finset conversion.
Claim. Let $nf$ be a normal form. If $pair$ belongs to the support pairs of $nf$ and the coefficient of $pair$ for primitive $prim$ is nonzero, then $pair$ belongs to the finite set of pairs obtained by mapping each micro-move in toMoves$(nf)$ to its pair component.
background
A NormalForm is a structure with a finite Finset of support pairs and a coefficient map from pairs and Primitives to reals, obeying zero outside support and nontriviality on each supported pair. Primitives form the fixed list of fourteen generators in canonical order: Love, Justice, Forgiveness, Wisdom, Courage, Temperance, Prudence, Compassion, Gratitude, Patience, Humility, Hope, Creativity, Sacrifice. The function toMoves produces the canonical ordered list of micro-moves by flattening rowMoves over the ordered pair list from pairList.
proof idea
The proof runs in tactic mode. It first applies the upstream lemma mem_toMoves_of_coeff_ne_zero to obtain the concrete MicroMove triple. It then uses List.mem_map.mpr to witness membership in the mapped list, with simp discharging the pair projection. Finally List.mem_toFinset.mpr converts the list membership into the required Finset membership.
why it matters
The lemma supplies a key membership step for the round-trip theorem of_toMoves, which asserts that ofMicroMoves applied to toMoves recovers the original normal form. It thereby confirms faithfulness of the coefficient-table representation inside the micro-move normal forms module. The construction supplies discrete algebraic scaffolding for virtue aggregation that parallels the Recognition Composition Law and phi-ladder structures used in the core forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.