ofMicroMoves

formal source

 115  exact h_mem.2
 116
 117/-- Build NormalForm from a move list (aggregates coefficients). -/
 118noncomputable def ofMicroMoves (moves : List MicroMove) : NormalForm where
 119  supportPairs := (moves.map (·.pair)).toFinset.filter (fun k =>
 120    ∃ prim, aggCoeff moves k prim ≠ 0)
 121  coeff := aggCoeff moves
 122  zero_outside := ofMicroMoves_zero_outside moves
 123  nontrivial := ofMicroMoves_nontrivial moves
 124
 125/-- Every micro-move generated for `pair` stays within that pair scope.
 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