Degree and cut accounting for an edge switch

The switch replaces one neighbor at each of its four endpoints. It leaves the cut of a side containing all four vertices unchanged. The later helpfulness accounting distinguishes the two membership patterns in which reversing a switch can lose helpfulness.

theorem Algebraic.Cutwidth.Bisection.Internal.switchEdges_neighbor_a {W : Type} [Fintype W] (H : SimpleGraph W) {a b c d : W} (valid : Switchable H a b c d) : (switchEdges H a b c d).neighborFinset a = insert c ((H.neighborFinset a).erase b)

theorem Algebraic.Cutwidth.Bisection.Internal.switchEdges_neighbor_b {W : Type} [Fintype W] (H : SimpleGraph W) {a b c d : W} (valid : Switchable H a b c d) : (switchEdges H a b c d).neighborFinset b = insert d ((H.neighborFinset b).erase a)

theorem Algebraic.Cutwidth.Bisection.Internal.switchEdges_neighbor_c {W : Type} [Fintype W] (H : SimpleGraph W) {a b c d : W} (valid : Switchable H a b c d) : (switchEdges H a b c d).neighborFinset c = insert a ((H.neighborFinset c).erase d)

theorem Algebraic.Cutwidth.Bisection.Internal.switchEdges_neighbor_d {W : Type} [Fintype W] (H : SimpleGraph W) {a b c d : W} (valid : Switchable H a b c d) : (switchEdges H a b c d).neighborFinset d = insert b ((H.neighborFinset d).erase c)

theorem Algebraic.Cutwidth.Bisection.Internal.switchEdges_neighbor_other {W : Type} [Fintype W] (H : SimpleGraph W) {a b c d v : W} (ha : v ≠ a) (hb : v ≠ b) (hc : v ≠ c) (hd : v ≠ d) : (switchEdges H a b c d).neighborFinset v = H.neighborFinset v

theorem Algebraic.Cutwidth.Bisection.Internal.switchEdges_degree {W : Type} [Fintype W] (H : SimpleGraph W) {a b c d : W} (valid : Switchable H a b c d) (v : W) : (switchEdges H a b c d).degree v = H.degree v

theorem Algebraic.Cutwidth.Bisection.Internal.switchEdges_cut {W : Type} [Fintype W] (H : SimpleGraph W) {a b c d : W} {S : Finset W} (ha : a ∈ S) (hb : b ∈ S) (hc : c ∈ S) (hd : d ∈ S) : (switchEdges H a b c d).cutFinset S = H.cutFinset S

theorem Algebraic.Cutwidth.Bisection.Internal.switchEdges_neighbors_outside {W : Type} [Fintype W] (H : SimpleGraph W) {a b c d : W} {S : Finset W} (ha : a ∈ S) (hb : b ∈ S) (hc : c ∈ S) (hd : d ∈ S) (v : W) : (switchEdges H a b c d).neighborFinset v \ S = H.neighborFinset v \ S

theorem Algebraic.Cutwidth.Bisection.Internal.switchEdges_boundary {W : Type} [Fintype W] (H : SimpleGraph W) {a b c d : W} {S : Finset W} (ha : a ∈ S) (hb : b ∈ S) (hc : c ∈ S) (hd : d ∈ S) : cutBoundary (switchEdges H a b c d) S = cutBoundary H S

theorem Algebraic.Cutwidth.Bisection.Internal.helpfulness_switchEdges {W : Type} [Fintype W] (H : SimpleGraph W) {a b c d : W} (valid : Switchable H a b c d) {S X : Finset W} (ha : a ∈ S) (hb : b ∈ S) (hc : c ∈ S) (hd : d ∈ S) (hX : X ⊆ S) : helpfulness (switchEdges H a b c d) S X = helpfulness H S X + 2 * ((if a ∈ X then 1 else 0) - if d ∈ X then 1 else 0) * ((if c ∈ X then 1 else 0) - if b ∈ X then 1 else 0)

theorem Algebraic.Cutwidth.Bisection.Internal.helpfulness_reverse_switch_le {W : Type} [Fintype W] (H : SimpleGraph W) {a b c d : W} (valid : Switchable H a b c d) {S X : Finset W} (ha : a ∈ S) (hb : b ∈ S) (hc : c ∈ S) (hd : d ∈ S) (hX : X ⊆ S) (notAC : ¬(a ∈ X ∧ c ∈ X ∧ b ∉ X ∧ d ∉ X)) (notBD : ¬(b ∈ X ∧ d ∈ X ∧ a ∉ X ∧ c ∉ X)) : helpfulness (switchEdges H a b c d) S X ≤ helpfulness H S X

theorem Algebraic.Cutwidth.Bisection.Internal.exists_restore_boundary_switch {W : Type} [Fintype W] (H : SimpleGraph W) {a b c d : W} (valid : Switchable H a b c d) {S X : Finset W} (degree : ∀ v ∈ S, H.degree v ≤ 3) (ha : a ∈ cutBoundary H S) (hb : b ∈ cutBoundary H S) (hc : c ∈ S) (hd : d ∈ S) (bc : H.Adj b c) (hX : X ⊆ S) : ∃ (Y : Finset W), X ⊆ Y ∧ Y ⊆ S ∧ Y.card ≤ X.card + 2 ∧ helpfulness (switchEdges H a b c d) S X ≤ helpfulness H S Y ∧ (Y = X ∨ a ∈ Y ∧ b ∈ Y ∧ (a ∈ X ∧ b ∉ X ∨ b ∈ X ∧ a ∉ X)) ∧ Y ⊆ insert c (insert a (insert b X))

theorem Algebraic.Cutwidth.Bisection.Internal.exists_restore_three_neighbor_switch {W : Type} [Fintype W] (H : SimpleGraph W) {a b c d : W} (valid : Switchable H a b c d) {S X : Finset W} (degree : ∀ v ∈ S, H.degree v ≤ 3) (ha : a ∈ S) (hb : b ∈ cutBoundary H S) (hc : c ∈ S \ cutBoundary H S) (hd : d ∈ S) (bc : H.Adj b c) (three : (H.neighborFinset a ∩ cutBoundary H S).card = 3) (hX : X ⊆ S) : ∃ (Y : Finset W), X ⊆ Y ∧ Y ⊆ S ∧ Y.card ≤ X.card + 4 ∧ helpfulness (switchEdges H a b c d) S X ≤ helpfulness H S Y ∧ (Y = X ∨ a ∈ Y ∧ b ∈ Y ∧ (a ∈ X ∧ b ∉ X ∨ b ∈ X ∧ a ∉ X)) ∧ (a ∈ X → Y ⊆ insert b X) ∧ Y ⊆ insert c (insert a (X ∪ H.neighborFinset a ∩ cutBoundary H S))

theorem Algebraic.Cutwidth.Bisection.Internal.exists_boundary_switch {W : Type} [Fintype W] (H : SimpleGraph W) {S : Finset W} (regular : H.IsRegularOfDegree 3) (noHelpful : ∀ X ⊆ S, X.card ≤ 11 → helpfulness H S X ≤ 0) {a b : W} (ha : a ∈ cutBoundary H S) (hb : b ∈ cutBoundary H S) (ab : H.Adj a b) : ∃ (c : W) (d : W), Switchable H a b c d ∧ H.Adj b c ∧ c ∈ S \ cutBoundary H S ∧ d ∈ S \ cutBoundary H S ∧ (H.neighborFinset c ∩ cutBoundary H S).card ≤ 2 ∧ (H.neighborFinset d ∩ cutBoundary H S).card ≤ 1

theorem Algebraic.Cutwidth.Bisection.Internal.exists_three_neighbor_switch {W : Type} [Fintype W] (H : SimpleGraph W) {S : Finset W} (regular : H.IsRegularOfDegree 3) (noHelpful : ∀ X ⊆ S, X.card ≤ 11 → helpfulness H S X ≤ 0) {a b : W} (ha : a ∈ S \ cutBoundary H S) (hb : b ∈ cutBoundary H S) (ab : H.Adj a b) (three : (H.neighborFinset a ∩ cutBoundary H S).card = 3) : ∃ (c : W) (d : W), Switchable H a b c d ∧ H.Adj b c ∧ c ∈ S \ cutBoundary H S ∧ d ∈ S \ cutBoundary H S ∧ (H.neighborFinset c ∩ cutBoundary H S).card ≤ 2 ∧ (H.neighborFinset d ∩ cutBoundary H S).card ≤ 1