Exact cut changes in the bisection argument

Flipping a set toggles exactly the edges in its cut. The resulting integer identities make successive moves telescope, including moves that restore balance after improving the cut.

theorem Algebraic.Cutwidth.Bisection.Internal.cutFinset_symmDiff {W : Type} [Fintype W] (H : SimpleGraph W) (S X : Finset W) : H.cutFinset (symmDiff S X) = symmDiff (H.cutFinset S) (H.cutFinset X)

theorem Algebraic.Cutwidth.Bisection.Internal.helpfulness_eq_sub {W : Type} [Fintype W] (H : SimpleGraph W) (S X : Finset W) : helpfulness H S X = ↑(H.cutFinset S).card - ↑(H.cutFinset (symmDiff S X)).card

theorem Algebraic.Cutwidth.Bisection.Internal.helpfulness_eq_sub_sdiff {W : Type} [Fintype W] (H : SimpleGraph W) {S X : Finset W} (hX : X ⊆ S) : helpfulness H S X = ↑(H.cutFinset S).card - ↑(H.cutFinset (S \ X)).card

theorem Algebraic.Cutwidth.Bisection.Internal.helpfulness_eq_sub_union {W : Type} [Fintype W] (H : SimpleGraph W) {S X : Finset W} (hX : Disjoint S X) : helpfulness H S X = ↑(H.cutFinset S).card - ↑(H.cutFinset (S ∪ X)).card

theorem Algebraic.Cutwidth.Bisection.Internal.helpfulness_add {W : Type} [Fintype W] (H : SimpleGraph W) (S X Y : Finset W) : helpfulness H S (symmDiff X Y) = helpfulness H S X + helpfulness H (symmDiff S X) Y

theorem Algebraic.Cutwidth.Bisection.Internal.helpfulness_compl {W : Type} [Fintype W] (H : SimpleGraph W) (S X : Finset W) : helpfulness H Sᶜ X = helpfulness H S X

theorem Algebraic.Cutwidth.Bisection.Internal.exists_min_cut_of_card {W : Type} [Fintype W] (H : SimpleGraph W) {m : ℕ} (hm : m ≤ Fintype.card W) : ∃ (S : Finset W), S.card = m ∧ ∀ (T : Finset W), T.card = m → (H.cutFinset S).card ≤ (H.cutFinset T).card

theorem Algebraic.Cutwidth.Bisection.Internal.exists_min_bisection {W : Type} [Fintype W] (H : SimpleGraph W) : ∃ (S : Finset W), S.card ≤ Sᶜ.card + 1 ∧ Sᶜ.card ≤ S.card + 1 ∧ ∀ (T : Finset W), T.card ≤ Tᶜ.card + 1 → Tᶜ.card ≤ T.card + 1 → (H.cutFinset S).card ≤ (H.cutFinset T).card

theorem Algebraic.Cutwidth.Bisection.Internal.two_moves_le_zero {W : Type} [Fintype W] (H : SimpleGraph W) {S : Finset W} (minimal : ∀ (T : Finset W), T.card = S.card → (H.cutFinset S).card ≤ (H.cutFinset T).card) {X Y : Finset W} (hX : X ⊆ S) (hY : Y ⊆ (S \ X)ᶜ) (sameSize : Y.card = X.card) : helpfulness H S X + helpfulness H (S \ X)ᶜ Y ≤ 0

theorem Algebraic.Cutwidth.Bisection.Internal.cutFinset_singleton {W : Type} [Fintype W] (H : SimpleGraph W) (v : W) : H.cutFinset {v} = Finset.map (Sym2.mkEmbedding v) (H.neighborFinset v)

theorem Algebraic.Cutwidth.Bisection.Internal.helpfulness_eq_two_mul_inter_sub {W : Type} [Fintype W] (H : SimpleGraph W) (S X : Finset W) : helpfulness H S X = 2 * ↑(H.cutFinset X ∩ H.cutFinset S).card - ↑(H.cutFinset X).card

theorem Algebraic.Cutwidth.Bisection.Internal.helpfulness_singleton {W : Type} [Fintype W] (H : SimpleGraph W) {S : Finset W} {v : W} (hv : v ∈ S) : helpfulness H S {v} = 2 * ↑(H.neighborFinset v \ S).card - ↑(H.degree v)

theorem Algebraic.Cutwidth.Bisection.Internal.one_le_helpfulness_singleton {W : Type} [Fintype W] (H : SimpleGraph W) {S : Finset W} {v : W} (hv : v ∈ S) (degree : H.degree v ≤ 3) (outside : 2 ≤ (H.neighborFinset v \ S).card) : 1 ≤ helpfulness H S {v}

theorem Algebraic.Cutwidth.Bisection.Internal.card_cut_inter_eq_sum_neighbors {W : Type} [Fintype W] (H : SimpleGraph W) {S X : Finset W} (hX : X ⊆ S) : (H.cutFinset X ∩ H.cutFinset S).card = ∑ v ∈ X, (H.neighborFinset v \ S).card

theorem Algebraic.Cutwidth.Bisection.Internal.card_cutFinset_eq_sum_neighbors {W : Type} [Fintype W] (H : SimpleGraph W) (X : Finset W) : (H.cutFinset X).card = ∑ v ∈ X, (H.neighborFinset v \ X).card

theorem Algebraic.Cutwidth.Bisection.Internal.degree_sum_cut {W : Type} [Fintype W] (H : SimpleGraph W) (X : Finset W) : (H.cutFinset X).card + 2 * (SimpleGraph.induce {w : W | w ∈ X} H).edgeFinset.card = ∑ v ∈ X, H.degree v

theorem Algebraic.Cutwidth.Bisection.Internal.abs_helpfulness_le_card_cut {W : Type} [Fintype W] (H : SimpleGraph W) (S X : Finset W) : |helpfulness H S X| ≤ ↑(H.cutFinset X).card

theorem Algebraic.Cutwidth.Bisection.Internal.abs_helpfulness_le_mul_card {W : Type} [Fintype W] (H : SimpleGraph W) (S X : Finset W) {d : ℕ} (degree : ∀ v ∈ X, H.degree v ≤ d) : |helpfulness H S X| ≤ ↑d * ↑X.card

theorem Algebraic.Cutwidth.Bisection.Internal.helpfulness_eq_degree_sum {W : Type} [Fintype W] (H : SimpleGraph W) {S X : Finset W} (hX : X ⊆ S) : helpfulness H S X = 2 * ∑ v ∈ X, ↑(H.neighborFinset v \ S).card + 2 * ↑(SimpleGraph.induce {w : W | w ∈ X} H).edgeFinset.card - ∑ v ∈ X, ↑(H.degree v)

theorem Algebraic.Cutwidth.Bisection.Internal.card_sub_two_le_helpfulness {W : Type} [Fintype W] (H : SimpleGraph W) {S X : Finset W} (hX : X ⊆ S) (connected : (SimpleGraph.induce {w : W | w ∈ X} H).Connected) (degree : ∀ v ∈ X, H.degree v ≤ 3) (boundary : ∀ v ∈ X, ∃ w ∉ S, H.Adj v w) : ↑X.card - 2 ≤ helpfulness H S X