pairList_mem

formal source

  57noncomputable def pairList (nf : NormalForm) : List ℕ :=
  58  nf.supportPairs.sort (· ≤ ·)
  59
  60lemma pairList_mem {nf : NormalForm} {pair : ℕ} :
  61    pair ∈ pairList nf ↔ pair ∈ nf.supportPairs := by
  62  unfold pairList
  63  simp only [mem_sort]
  64
  65lemma pairList_nodup (nf : NormalForm) : (pairList nf).Nodup := by
  66  unfold pairList
  67  simp only [sort_nodup]
  68
  69/-- Micro-moves for a single pair. -/
  70noncomputable def rowMoves (nf : NormalForm) (pair : ℕ) : List MicroMove :=
  71  primitiveOrderList.filterMap (fun prim =>
  72    if nf.coeff pair prim = 0 then none
  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