literal_unchanged_by_flip

formal source

  93  simp [flipBit, hij]
  94
  95/-- A literal not involving variable j has the same truth value after flipping j. -/
  96theorem literal_unchanged_by_flip {n : ℕ} (a : Assignment n) (j : Fin n)
  97    (lit : Fin n × Bool) (hlit : lit.1 ≠ j) :
  98    Literal.satisfiedBy lit (flipBit a j) = Literal.satisfiedBy lit a := by
  99  unfold Literal.satisfiedBy
 100  rw [flipBit_other a j lit.1 hlit]
 101
 102/-- A clause not containing variable j has the same satisfaction after flipping j. -/
 103theorem clause_unchanged_by_flip {n : ℕ} (a : Assignment n) (j : Fin n)
 104    (c : Clause n) (hc : containsVar c j = false) :
 105    c.satisfiedBy (flipBit a j) = c.satisfiedBy a := by
 106  have hne : ∀ lit ∈ c.literals, lit.fst ≠ j := by
 107    intro lit hmem heq
 108    unfold containsVar at hc
 109    have : c.literals.any (fun l => l.1 == j) = true :=
 110      List.any_eq_true.mpr ⟨lit, hmem, by rw [beq_iff_eq]; exact heq⟩
 111    rw [hc] at this; exact absurd this Bool.false_ne_true
 112  apply Bool.eq_iff_iff.mpr
 113  unfold Clause.satisfiedBy
 114  rw [List.any_eq_true, List.any_eq_true]
 115  exact ⟨fun ⟨l, hm, hs⟩ => ⟨l, hm, by rw [← literal_unchanged_by_flip a j l (hne l hm)]; exact hs⟩,
 116         fun ⟨l, hm, hs⟩ => ⟨l, hm, by rw [literal_unchanged_by_flip a j l (hne l hm)]; exact hs⟩⟩
 117
 118/-- The J-cost edge weight is bounded by the variable degree.
 119    Flipping bit j can only change clauses that contain variable j.
 120    Clauses not containing j have identical satisfaction (by `clause_unchanged_by_flip`),
 121    so only clauses containing j contribute to the cost difference.
 122
 123    The formal discharge requires a list-filter symmetric difference counting lemma:
 124    for predicates P, Q agreeing outside a subset S,
 125    |filter(P).length - filter(Q).length| ≤ S.length. Recorded as a named proposition. -/
 126def jcostEdgeWeight_le_varDegree_prop {n : ℕ} (f : CNFFormula n) (a : Assignment n)