Local improvements of a graph bisection

These are the cut identities, minimization argument, and first local cases in Monien and Preis's Upper Bounds on the Bisection Width of 3- and 4-regular Graphs. A helpful move decreases the cut by exactly its signed helpfulness. An equally sized reverse move restores balance; if the total helpfulness is positive, the original cut was not minimal.

A subcubic vertex with two crossing edges is helpful. More generally, a connected set of boundary vertices has helpfulness at least its size minus two. Bisection.LocalConfigurations proves the remaining small configurations used before normalization. Bisection.Rebalancing supplies the rebalancing step. The bounded local helpful-set lemma needed for the sharp bisection theorem is Bisection.exists_bounded_helpful in Bisection.Helpful.

theorem Algebraic.Cutwidth.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)

Flipping membership in X toggles exactly the edges in the cut of X.

theorem Algebraic.Cutwidth.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

Helpfulness is exactly the signed decrease in the cut size.

theorem Algebraic.Cutwidth.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

Moving a subset out of one side decreases the cut by its helpfulness.

theorem Algebraic.Cutwidth.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

Moving a disjoint set into a side decreases the cut by its helpfulness.

theorem Algebraic.Cutwidth.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

Successive moves have additive helpfulness, measured at the current cut.

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

Renaming the two sides does not affect the helpfulness of a flip.

theorem Algebraic.Cutwidth.Bisection.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

Among all cuts with a prescribed side cardinality, a minimum exists.

theorem Algebraic.Cutwidth.Bisection.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

A minimum balanced cut exists, including when the graph has odd order.

theorem Algebraic.Cutwidth.Bisection.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

A minimum cut cannot admit an improving pair of moves that restores its side cardinality. The reverse move may include vertices of the first move.

theorem Algebraic.Cutwidth.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

Crossing edges incident to a moved subset are counted once by their endpoint in that subset.

theorem Algebraic.Cutwidth.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

The degree sum of a vertex set counts internal edges twice and crossing edges once.

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

Flipping a set changes the cut by at most the number of edges leaving that set, whether the move is helpful or costly.

theorem Algebraic.Cutwidth.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

A maximum degree bound controls the change in cut size by the number of moved vertices. In particular, this bounds overshoot when accumulating moves.

theorem Algebraic.Cutwidth.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)

Helpfulness expressed by outside neighbors, internal edges, and degrees.

theorem Algebraic.Cutwidth.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)

A single vertex removes its outside edges and adds its inside edges.

theorem Algebraic.Cutwidth.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}

A subcubic vertex incident to at least two crossing edges is helpful.

theorem Algebraic.Cutwidth.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

Connected boundary vertices have helpfulness at least their number minus two in a graph of maximum degree three.

theorem Algebraic.Cutwidth.one_le_helpfulness_of_connected_boundary {W : Type} [Fintype W] (H : SimpleGraph W) {S X : Finset W} (hX : X ⊆ cutBoundary H S) (connected : (SimpleGraph.induce {w : W | w ∈ X} H).Connected) (degree : ∀ v ∈ X, H.degree v ≤ 3) (size : 3 ≤ X.card) : 1 ≤ helpfulness H S X

In particular, three or more connected boundary vertices form a helpful set. This is a local case in Monien–Preis's bounded helpful-set lemma.