flipBit_flipBit

formal source

  37def flipBit {n : ℕ} (a : Assignment n) (k : Fin n) : Assignment n :=
  38  fun j => if j = k then !a k else a j
  39
  40theorem flipBit_flipBit {n : ℕ} (a : Assignment n) (k : Fin n) :
  41    flipBit (flipBit a k) k = a := by
  42  funext j; simp only [flipBit]
  43  split_ifs with h
  44  · subst h; simp
  45  · rfl
  46
  47theorem flipBit_ne {n : ℕ} (a : Assignment n) (k : Fin n) :
  48    flipBit a k ≠ a := by
  49  intro h
  50  have : (flipBit a k) k = a k := congr_fun h k
  51  simp [flipBit] at this
  52
  53/-! ## J-Cost Edge Weights -/
  54
  55/-- The J-cost edge weight when flipping bit k. -/
  56def jcostEdgeWeight {n : ℕ} (f : CNFFormula n) (a : Assignment n) (k : Fin n) : ℝ :=
  57  |satJCost f a - satJCost f (flipBit a k)|
  58
  59theorem jcostEdgeWeight_nonneg {n : ℕ} (f : CNFFormula n) (a : Assignment n)
  60    (k : Fin n) : 0 ≤ jcostEdgeWeight f a k :=
  61  abs_nonneg _
  62
  63theorem jcostEdgeWeight_symm {n : ℕ} (f : CNFFormula n) (a : Assignment n)
  64    (k : Fin n) : jcostEdgeWeight f a k = jcostEdgeWeight f (flipBit a k) k := by
  65  unfold jcostEdgeWeight; rw [flipBit_flipBit]; exact (abs_sub_comm _ _).symm
  66
  67theorem jcostEdgeWeight_le_clauses {n : ℕ} (f : CNFFormula n) (a : Assignment n)
  68    (k : Fin n) : jcostEdgeWeight f a k ≤ f.clauses.length := by
  69  unfold jcostEdgeWeight satJCost
  70  have h1 : (↑(f.clauses.filter (fun c => !c.satisfiedBy a)).length : ℝ) ≤