pairList
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not include coefficients or primitives in the output.
- Does not impose any bound on support size.
- Does not compute aggregates or sums over the list.
- Does not alter the underlying support set.
formal statement (Lean)
57noncomputable def pairList (nf : NormalForm) : List ℕ :=
proof body
Definition body.
58 nf.supportPairs.sort (· ≤ ·)
59