of_toMoves
plain-language theorem explainer
Normal forms are recovered exactly after conversion to micro-move lists and reconstruction. Workers on canonical representations for micro-move tables in ethics models cite this to guarantee lossless encoding. The tactic proof uses extensionality on pairs and primitives, matching supports via aggregation equalities and nonzero coefficient lemmas.
Claim. Let $nf$ be a normal form with finite support of pairs and coefficient function to reals. Then the reconstruction from the aggregated micro-move list generated by $nf$ equals $nf$ exactly.
background
NormalForm is the structure holding a finite set of supported pairs together with a coefficient map from pairs and primitives to reals, satisfying zero outside support and nontriviality on support. ofMicroMoves builds such a structure by filtering pairs with nonzero aggregated coefficients from a list of MicroMove records. toMoves produces the list of moves from the coefficient table. The module develops canonical normal forms for micro-move coefficient tables to support DREAM scaffolding in ethics. Upstream results include the aggregation function aggCoeff that sums coefficients for matching pair-primitive pairs, and lemmas establishing that toMoves preserves nonzero coefficients.
proof idea
The proof applies classical logic and extensionality on the pair and primitive indices. For the support membership direction it uses the filter characterization of ofMicroMoves together with sumCoeffs_toMoves to recover nonzero coefficients and the zero_outside property. The converse direction invokes the nontriviality axiom of NormalForm and the pair_mem_toMoves_map lemma to place the pair in the filtered set. The coefficient equality follows directly by simplification with sumCoeffs_toMoves.
why it matters
This round-trip theorem confirms that the micro-move encoding is bijective on the space of normal forms, closing the representation loop in the NormalForm module. It supports the DREAM scaffolding mentioned in the module documentation by ensuring that coefficient tables can be serialized and deserialized without loss. No downstream uses are recorded yet, but it underpins any further development of virtue or kinship models relying on these normal forms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.