of_toMoves
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not address infinite support tables.
- Does not compute explicit numerical values for coefficients.
- Does not extend to non-canonical forms outside the NormalForm structure.
- Does not prove uniqueness of the move list representation.
formal statement (Lean)
442theorem of_toMoves (nf : NormalForm) :
443 ofMicroMoves (toMoves nf) = nf := by
proof body
Tactic-mode proof.
444 classical
445 ext pair prim
446 · constructor
447 · intro hmem
448 rcases Finset.mem_filter.mp hmem with ⟨hmap, hex⟩
449 rcases hex with ⟨prim', hagg⟩
450 have hcoeff : nf.coeff pair prim' ≠ 0 := by
451 simpa [sumCoeffs_toMoves] using hagg
452 have : pair ∈ nf.supportPairs := by
453 by_contra hnot
454 have := nf.zero_outside (pair := pair) (prim := prim') hnot
455 exact hcoeff (by simpa [sumCoeffs_toMoves] using this)
456 exact this
457 · intro hmem
458 obtain ⟨prim', hcoeff⟩ := nf.nontrivial hmem
459 have hcoeff' : nf.coeff pair prim' ≠ 0 := hcoeff
460 have hmap := pair_mem_toMoves_map (nf := nf) hmem hcoeff'
461 have : aggCoeff (toMoves nf) pair prim' ≠ 0 := by
462 simpa [sumCoeffs_toMoves] using hcoeff'
463 refine Finset.mem_filter.mpr ⟨hmap, ?_⟩
464 exact ⟨prim', this⟩
465 · simpa [ofMicroMoves, sumCoeffs_toMoves]
466
467/-- The canonical pair list matches the 16-window filtered enumeration. -/