pairList
plain-language theorem explainer
The canonical ordered list of supported pairs for a micro-move normal form is obtained by sorting its finite support set in ascending order. Researchers formalizing coefficient tables for DREAM scaffolding cite this when enumerating moves or checking membership. The definition is realized by a direct sort of the support finset.
Claim. Let $nf$ be a normal form with finite support set $S$. The canonical list is the ascending sort of $S$.
background
The module defines micro-move normal forms as coefficient tables with finite support, supporting DREAM scaffolding. A normal form consists of a Finset of pairs, a coefficient map from pairs and primitives to reals, with coefficients required to vanish outside the support and to be nontrivial on the support. The upstream structure supplies the supportPairs field that this definition consumes.
proof idea
One-line wrapper that applies the sort operation with the natural order to the supportPairs field of the normal form.
why it matters
This definition supplies the ordered enumeration required by eight downstream lemmas, including membership tests and the theorem equating the list to the filtered range up to 16. It completes the canonical representation step in the micro-move normal form machinery of the ethics module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.