pairList_mem
The lemma equates membership of a natural number in the sorted support list of a normal form structure with membership in its finite support set. Researchers working on micro-move coefficient tables cite this equivalence when converting between set-based and list-based representations of supported pairs. The proof is a direct unfolding of the list definition followed by simplification using the membership property of sorted Finsets.
claimFor a normal form structure $nf$ and natural number $pair$, $pair$ belongs to the sorted support list of $nf$ if and only if $pair$ belongs to the support set of $nf$.
background
The module develops canonical normal forms for micro-move coefficient tables that support DREAM scaffolding. A normal form structure consists of a finite set of support pairs together with a coefficient function from pairs and primitives to reals, subject to zero-outside-support and nontriviality conditions. The sorted support list is the ascending sort of that finite set.
proof idea
One-line wrapper that unfolds the definition of the sorted support list and applies the membership lemma for sorted lists.
why it matters in Recognition Science
This equivalence is invoked in the proofs of mem_toMoves_of_coeff_ne_zero and sumCoeffs_toMoves, which extract moves and aggregate coefficients from the normal form. It closes the gap between the set-based support in the normal form structure and the list-based operations required for move extraction. The module provides scaffolding for DREAM in the Recognition framework.
scope and limits
- Does not prove that the sorted list is duplicate-free.
- Does not constrain coefficient values or the Primitive type.
- Does not address the nontriviality axiom of the normal form structure.
- Does not establish uniqueness of the normal form representation.
Lean usage
have hpair : pair ∈ pairList nf := (pairList_mem).2 hsuppformal statement (Lean)
60lemma pairList_mem {nf : NormalForm} {pair : ℕ} :
61 pair ∈ pairList nf ↔ pair ∈ nf.supportPairs := by
proof body
Term-mode proof.
62 unfold pairList
63 simp only [mem_sort]
64