pairList_nodup
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not constrain the numerical values taken by any coefficients.
- Does not require the support set to be nonempty.
- Does not invoke the nontriviality axiom of the normal form.
- Does not address any property of the coefficient function beyond list uniqueness.
Lean usage
have hl := pairList_nodup nfformal statement (Lean)
65lemma pairList_nodup (nf : NormalForm) : (pairList nf).Nodup := by
proof body
Term-mode proof.
66 unfold pairList
67 simp only [sort_nodup]
68
69/-- Micro-moves for a single pair. -/