Helpful configurations used in normalization

Monien and Preis's Upper Bounds on the Bisection Width of 3- and 4-regular Graphs excludes five local configurations before normalizing the graph. Improvement covers the singleton and connected-boundary cases. This module proves the remaining witnesses of at most five, seven, and eleven vertices. All statements allow a subcubic graph and overlapping boundary neighborhoods.

The eleven-vertex construction starts with a nonnegative-helpfulness set of at most four vertices, then closes a small interior set under its neighbors. Its contrapositive supplies the interior neighbor of boundary degree at most one needed for an edge switch. EdgeSwitch proves one switch and its local reverse transfer. BoundaryNormalization and NeighborNormalization complete both phases with a uniform bound on their combined reverse extension.

theorem Algebraic.Cutwidth.helpfulness_insert {W : Type} [Fintype W] (H : SimpleGraph W) {S X : Finset W} (hX : X ⊆ S) {v : W} (hv : v ∈ S) (fresh : v ∉ X) : helpfulness H S (insert v X) = helpfulness H S X + 2 * ↑(H.neighborFinset v \ S).card - ↑(H.degree v) + 2 * ↑(H.neighborFinset v ∩ X).card

Adding a vertex contributes its singleton helpfulness and twice the number of its neighbors already in the moved set.

theorem Algebraic.Cutwidth.Bisection.helpfulness_union_boundary {W : Type} [Fintype W] (H : SimpleGraph W) {S X A : Finset W} (hX : X ⊆ S) (hA : A ⊆ cutBoundary H S) (degree : ∀ c ∈ A, H.degree c ≤ 3) (adjacent : ∀ c ∈ A, ∃ x ∈ X, H.Adj c x) : helpfulness H S X + ↑(A \ X).card ≤ helpfulness H S (X ∪ A)

Each new boundary vertex attached to the old set increases helpfulness by at least one.

theorem Algebraic.Cutwidth.Bisection.helpfulness_union_boundaryLift_of_closed {W : Type} [Fintype W] (H : SimpleGraph W) {S X Z : Finset W} (hX : X ⊆ S) (hZ : Z ⊆ S \ cutBoundary H S) (degree : ∀ v ∈ S, H.degree v ≤ 3) (closed : ∀ z ∈ Z, H.neighborFinset z ⊆ X ∪ Z ∪ cutBoundary H S) (touch : ∃ x ∈ X, ∃ z ∈ Z \ X, H.Adj x z) : helpfulness H S X + 1 ≤ helpfulness H S (X ∪ boundaryLift H S Z)

Adjoining an interior set and its boundary neighbors improves helpfulness if the interior set has no other neighbors and has an edge to the old set.

theorem Algebraic.Cutwidth.Bisection.nonneg_helpfulness_boundary_pair {W : Type} [Fintype W] (H : SimpleGraph W) {S : Finset W} {c d : W} (hc : c ∈ cutBoundary H S) (hd : d ∈ cutBoundary H S) (degree : ∀ v ∈ S, H.degree v ≤ 3) (adjacent : H.Adj c d) : 0 ≤ helpfulness H S {c, d}

Adjacent boundary vertices form a set of nonnegative helpfulness.

theorem Algebraic.Cutwidth.Bisection.nonneg_helpfulness_boundary_star {W : Type} [Fintype W] (H : SimpleGraph W) {S : Finset W} (degree : ∀ v ∈ S, H.degree v ≤ 3) {v : W} (hv : v ∈ S) (three : (H.neighborFinset v ∩ cutBoundary H S).card = 3) : 0 ≤ helpfulness H S (insert v (H.neighborFinset v ∩ cutBoundary H S))

A vertex with three boundary neighbors and those neighbors form a set of nonnegative helpfulness.

theorem Algebraic.Cutwidth.Bisection.exists_helpful_of_boundary_pair_three_neighbors {W : Type} [Fintype W] (H : SimpleGraph W) {S : Finset W} (degree : ∀ v ∈ S, H.degree v ≤ 3) {c d v : W} (hc : c ∈ cutBoundary H S) (hd : d ∈ cutBoundary H S) (pair : H.Adj c d) (hv : v ∈ S \ cutBoundary H S) (adjacent : H.Adj v c) (three : (H.neighborFinset v ∩ cutBoundary H S).card = 3) : ∃ X ⊆ S, X.card ≤ 5 ∧ 1 ≤ helpfulness H S X

Monien--Preis configuration (iii): a boundary edge incident to the neighborhood of an interior vertex with three boundary neighbors.

theorem Algebraic.Cutwidth.Bisection.exists_helpful_of_shared_boundary_neighbor {W : Type} [Fintype W] (H : SimpleGraph W) {S : Finset W} (degree : ∀ v ∈ S, H.degree v ≤ 3) {u v c : W} (hu : u ∈ S \ cutBoundary H S) (hv : v ∈ S \ cutBoundary H S) (distinct : u ≠ v) (hc : c ∈ cutBoundary H S) (adjU : H.Adj u c) (adjV : H.Adj v c) (threeU : (H.neighborFinset u ∩ cutBoundary H S).card = 3) (threeV : (H.neighborFinset v ∩ cutBoundary H S).card = 3) : ∃ X ⊆ S, X.card ≤ 7 ∧ 1 ≤ helpfulness H S X

Monien--Preis configuration (iv): two interior vertices with three boundary neighbors share one of those neighbors.

theorem Algebraic.Cutwidth.Bisection.exists_helpful_extension_of_neighbor_types {W : Type} [Fintype W] (H : SimpleGraph W) {S X : Finset W} (hX : X ⊆ S) (neutral : 0 ≤ helpfulness H S X) (degree : ∀ v ∈ S, H.degree v ≤ 3) {v : W} (hv : v ∈ S \ cutBoundary H S) (fresh : v ∉ X) (touch : ∃ x ∈ X, H.Adj v x) (neighbors : ∀ (p : W), H.Adj v p → p ∉ X → p ∈ cutBoundary H S ∨ p ∈ S \ cutBoundary H S ∧ 2 ≤ (H.neighborFinset p ∩ cutBoundary H S).card) : ∃ Y ⊆ S, Y.card ≤ X.card + 7 ∧ 1 ≤ helpfulness H S Y

A nonnegative-helpfulness set grows into a helpful set using at most seven new vertices if each remaining neighbor of an adjacent interior vertex is a boundary vertex or has at least two boundary neighbors.

theorem Algebraic.Cutwidth.Bisection.exists_helpful_of_boundary_neighbor_configuration {W : Type} [Fintype W] (H : SimpleGraph W) {S : Finset W} (degree : ∀ v ∈ S, H.degree v ≤ 3) {v c : W} (hv : v ∈ S \ cutBoundary H S) (hc : c ∈ cutBoundary H S) (adjacent : H.Adj v c) (anchor : (∃ d ∈ cutBoundary H S, H.Adj c d) ∨ ∃ u ∈ S \ cutBoundary H S, u ≠ v ∧ H.Adj c u ∧ (H.neighborFinset u ∩ cutBoundary H S).card = 3) (neighbors : ∀ (p : W), H.Adj v p → p ≠ c → p ∈ cutBoundary H S ∨ p ∈ S \ cutBoundary H S ∧ 2 ≤ (H.neighborFinset p ∩ cutBoundary H S).card) : ∃ Y ⊆ S, Y.card ≤ 11 ∧ 1 ≤ helpfulness H S Y

Monien--Preis configuration (v), covering either a boundary edge or a vertex with three boundary neighbors at the other end of the boundary attachment.

theorem Algebraic.Cutwidth.Bisection.exists_switch_neighbor {W : Type} [Fintype W] (H : SimpleGraph W) {S : Finset W} (degree : ∀ v ∈ S, H.degree v ≤ 3) (noHelpful : ∀ X ⊆ S, X.card ≤ 11 → helpfulness H S X ≤ 0) {v c : W} (hv : v ∈ S \ cutBoundary H S) (hc : c ∈ cutBoundary H S) (adjacent : H.Adj v c) (anchor : (∃ d ∈ cutBoundary H S, H.Adj c d) ∨ ∃ u ∈ S \ cutBoundary H S, u ≠ v ∧ H.Adj c u ∧ (H.neighborFinset u ∩ cutBoundary H S).card = 3) : ∃ (p : W), H.Adj v p ∧ p ≠ c ∧ p ∈ S \ cutBoundary H S ∧ (H.neighborFinset p ∩ cutBoundary H S).card ≤ 1

If no helpful set of at most eleven vertices exists, the edge-switch configuration has another interior neighbor with at most one boundary neighbor.

theorem Algebraic.Cutwidth.Bisection.outside_eq_one_of_no_small_helpful {W : Type} [Fintype W] (H : SimpleGraph W) {S : Finset W} (degree : ∀ v ∈ S, H.degree v ≤ 3) (noHelpful : ∀ X ⊆ S, X.card ≤ 11 → helpfulness H S X ≤ 0) {c : W} (hc : c ∈ cutBoundary H S) : (H.neighborFinset c \ S).card = 1

Excluding the singleton helpful case leaves one outside edge at every boundary vertex.

theorem Algebraic.Cutwidth.Bisection.boundary_degree_le_one_of_no_small_helpful {W : Type} [Fintype W] (H : SimpleGraph W) {S : Finset W} (degree : ∀ v ∈ S, H.degree v ≤ 3) (noHelpful : ∀ X ⊆ S, X.card ≤ 11 → helpfulness H S X ≤ 0) {c : W} (hc : c ∈ cutBoundary H S) : (H.neighborFinset c ∩ cutBoundary H S).card ≤ 1

Excluding three connected boundary vertices leaves maximum degree one in the boundary-induced graph.