rowMoves_pair

formal source

 126
 127Proof: rowMoves constructs MicroMove.mk with pair as first argument,
 128so any move in the list has m.pair = pair by construction. -/
 129theorem rowMoves_pair {nf : NormalForm} {pair : ℕ} {m : MicroMove}
 130    (hm : m ∈ rowMoves nf pair) : m.pair = pair := by
 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. -/
 142theorem rowMoves_mem_of_coeff_ne_zero {nf : NormalForm} {pair : ℕ} {prim : Primitive}
 143    (hcoeff : nf.coeff pair prim ≠ 0) :
 144    ⟨pair, prim, nf.coeff pair prim⟩ ∈ rowMoves nf pair := by
 145  classical
 146  unfold rowMoves
 147  simp only [List.mem_filterMap]
 148  use prim, primitive_mem_order prim
 149  simp only [hcoeff, ite_false]
 150
 151/-- Auxiliary lemma: sum over a primitive list.
 152
 153This proof involves complex list manipulations with filterMap and filter.
 154The proof strategy:
 155- If coeff = 0: the filterMap excludes this primitive, so sum = 0
 156- If coeff ≠ 0: exactly one move matches, contributing the coefficient -/
 157theorem aggCoeff_rowMoves_aux_theorem
 158    (nf : NormalForm) (pair : ℕ) (prim : Primitive) :
 159    (((primitiveOrderList.filterMap fun q =>