+# Small helpful configurations before normalization

Monien and Preis exclude several bounded configurations before switching edges to normalize a side. The proofs below grow a set through adjacent boundary vertices and count shared neighbors without assuming they are distinct across different stars.

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

theorem Algebraic.Cutwidth.Bisection.Internal.helpfulness_insert_boundary {W : Type} [Fintype W] (H : SimpleGraph W) {S X : Finset W} (hX : X ⊆ S) {c : W} (hc : c ∈ cutBoundary H S) (fresh : c ∉ X) (degree : H.degree c ≤ 3) (adjacent : ∃ x ∈ X, H.Adj c x) : helpfulness H S X + 1 ≤ helpfulness H S (insert c X)

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

theorem Algebraic.Cutwidth.Bisection.Internal.helpfulness_insert_boundary_neighbors {W : Type} [Fintype W] (H : SimpleGraph W) {S X : Finset W} (hX : X ⊆ S) (degree : ∀ v ∈ S, H.degree v ≤ 3) {v : W} (hv : v ∈ S) (fresh : v ∉ X) : helpfulness H S X + 2 * ↑(H.neighborFinset v ∩ X).card - 3 + ↑((H.neighborFinset v ∩ cutBoundary H S) \ X).card ≤ helpfulness H S (insert v (X ∪ H.neighborFinset v ∩ cutBoundary H S))

theorem Algebraic.Cutwidth.Bisection.Internal.three_boundary_neighbors_extension {W : Type} [Fintype W] (H : SimpleGraph W) {S X : Finset W} (hX : X ⊆ S) (degree : ∀ v ∈ S, H.degree v ≤ 3) {v : W} (hv : v ∈ S) (fresh : v ∉ X) (three : (H.neighborFinset v ∩ cutBoundary H S).card = 3) (overlap : (H.neighborFinset v ∩ cutBoundary H S ∩ X).Nonempty) : (insert v (X ∪ H.neighborFinset v ∩ cutBoundary H S)).card ≤ X.card + 3 ∧ helpfulness H S X + 1 ≤ helpfulness H S (insert v (X ∪ H.neighborFinset v ∩ cutBoundary H S))

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

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

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

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

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

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

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

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

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

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