toMoves

formal source

  73    else some ⟨pair, prim, nf.coeff pair prim⟩)
  74
  75/-- Canonical ordered list of micro-moves. -/
  76noncomputable def toMoves (nf : NormalForm) : List MicroMove :=
  77  (pairList nf).flatMap (rowMoves nf)
  78
  79/-- Aggregate coefficient for `(pair, primitive)` extracted from a move list. -/
  80noncomputable def aggCoeff (moves : List MicroMove) (pair : ℕ) (prim : Primitive) : ℝ :=
  81  ((moves.filter fun m => m.pair = pair ∧ m.primitive = prim).map (·.coeff)).sum
  82
  83/-- **NormalForm construction**: The ofMicroMoves construction is well-formed.
  84
  85Proof by contraposition: if aggCoeff is nonzero, pair must be in the filtered set.
  86-/
  87theorem ofMicroMoves_zero_outside (moves : List MicroMove) :
  88  ∀ {pair prim}, pair ∉ (moves.map (·.pair)).toFinset.filter (fun k =>
  89    ∃ prim, aggCoeff moves k prim ≠ 0) → aggCoeff moves pair prim = 0 := by
  90  intro pair prim h_not_mem
  91  by_contra h_ne
  92  apply h_not_mem
  93  rw [Finset.mem_filter, List.mem_toFinset]
  94  constructor
  95  · -- Show pair ∈ moves.map (·.pair)
  96    -- If aggCoeff ≠ 0, there's a move with matching pair and prim
  97    have h_filter_ne : (moves.filter fun m => m.pair = pair ∧ m.primitive = prim) ≠ [] := by
  98      intro h_empty
  99      unfold aggCoeff at h_ne
 100      rw [h_empty] at h_ne
 101      simp at h_ne
 102    obtain ⟨m, hm⟩ := List.exists_mem_of_ne_nil _ h_filter_ne
 103    rw [List.mem_filter] at hm
 104    simp only [decide_eq_true_eq] at hm
 105    rw [List.mem_map]
 106    exact ⟨m, hm.1, hm.2.1⟩