ofMicroMoves_zero_outside

formal source

  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⟩
 107  · -- Show ∃ prim', aggCoeff moves pair prim' ≠ 0
 108    exact ⟨prim, h_ne⟩
 109
 110theorem ofMicroMoves_nontrivial (moves : List MicroMove) :
 111  ∀ {pair}, pair ∈ (moves.map (·.pair)).toFinset.filter (fun k =>
 112    ∃ prim, aggCoeff moves k prim ≠ 0) → ∃ prim, aggCoeff moves pair prim ≠ 0 := by
 113  intro pair h_mem
 114  rw [Finset.mem_filter] at h_mem
 115  exact h_mem.2
 116
 117/-- Build NormalForm from a move list (aggregates coefficients). -/