pairList_nodup
plain-language theorem explainer
The lemma shows that the ascending sorted list of support pairs from any normal form contains no duplicates. Workers on micro-move coefficient tables cite it to guarantee a unique ordering when flattening or aggregating moves. The argument is a direct one-line reduction that unfolds the list definition and invokes the standard fact that sorted finite lists are duplicate-free.
Claim. For every normal form $nf$ the ascending sorted list of its support pairs has no repeated entries.
background
The module develops canonical normal forms for micro-move coefficient tables supporting DREAM scaffolding. NormalForm is the structure consisting of a finite set of support pairs, a coefficient function from pairs and primitives to reals, together with the zero-outside-support and nontriviality axioms. The pairList operation extracts those support pairs and returns them in ascending sorted order. The result relies on the upstream NormalForm structure and the pairList definition; it also uses the general property that sorting a finite set produces a duplicate-free list.
proof idea
The proof is a one-line wrapper. It unfolds the definition of pairList and simplifies using the lemma that the output of sorting is nodup.
why it matters
The lemma supplies the uniqueness hypothesis required in the proof of sumCoeffs_toMoves, which shows that aggregated coefficients recovered from the move list equal the original table entries. It closes a basic well-formedness condition for the normal-form representation of micro-move tables. In the Recognition framework this supports the canonical ordering needed for coefficient aggregation steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.