rowMoves_pair
The theorem establishes that every micro-move extracted for a given pair index from a normal form's coefficient table has its pair field equal to that index. Researchers aggregating coefficients across micro-move rows cite it to guarantee isolation between distinct pair scopes. The proof unfolds the filterMap definition of rowMoves and performs case analysis on coefficient zero/nonzero to confirm the pair component by construction.
claimLet $nf$ be a normal form and $pair$ a natural number. For any micro-move $m$ belonging to the list of row moves generated by $nf$ for $pair$, the pair component of $m$ equals $pair$.
background
A NormalForm consists of a finite support set of pair indices together with a coefficient map from pairs and primitives to reals, required to vanish outside the support and to be nontrivial on the support. A MicroMove is the triple (pair index, primitive, real coefficient). The auxiliary definition rowMoves builds, for a fixed pair, the ordered list of such triples by filterMap over the canonical primitive list, emitting a move only when the stored coefficient is nonzero.
proof idea
The term proof first invokes classical logic, unfolds rowMoves, and simplifies the membership predicate to a filterMap condition. It obtains the underlying primitive and the equality produced by the constructor, then cases on whether the coefficient at that pair and primitive is zero. The zero branch yields an immediate contradiction with membership; the nonzero branch yields the required equality by the definition of MicroMove.mk.
why it matters in Recognition Science
The result is invoked directly by aggCoeff_rowMoves_of_ne to conclude that row moves belonging to one pair contribute zero to aggregation for any other pair, and it underpins the companion aggregation lemma aggCoeff_rowMoves. It supplies the scope-isolation property required for consistent coefficient tables in the DREAM scaffolding of the Recognition framework, ensuring that pair-wise rows remain independent under the eight-tick octave and related aggregation steps.
scope and limits
- Does not constrain the numerical values of any coefficients.
- Does not address moves generated for pairs outside the normal form support.
- Does not prove uniqueness or canonicity of the normal form itself.
- Does not interact with the forcing chain or phi-ladder constructions.
Lean usage
have h : m.pair = pair := rowMoves_pair hmformal statement (Lean)
129theorem rowMoves_pair {nf : NormalForm} {pair : ℕ} {m : MicroMove}
130 (hm : m ∈ rowMoves nf pair) : m.pair = pair := by
proof body
Term-mode proof.
131 classical
132 unfold rowMoves at hm
133 simp only [List.mem_filterMap] at hm
134 obtain ⟨prim, _, heq⟩ := hm
135 by_cases h : nf.coeff pair prim = 0 <;> simp only [h, ite_true, ite_false] at heq
136 · cases heq
137 · cases heq; rfl
138
139/-- If a coefficient is non-zero, the corresponding micro-move appears in the row.
140
141Proof: rowMoves uses filterMap which includes moves for non-zero coefficients. -/