Exact accounting for the red/black lift

The proof counts the outside neighbors of each moved vertex. A selected interior vertex pays its remaining black edges. An adjacent boundary vertex is neutral when one of its interior neighbors was selected, and contributes one when both were selected. This is the lifting step in Monien and Preis's bounded helpful-set lemma.

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

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

theorem Algebraic.Cutwidth.Bisection.Internal.boundaryLift_subset {W : Type} (H : SimpleGraph W) {S X : Finset W} (hX : X ⊆ S) : boundaryLift H S X ⊆ S

theorem Algebraic.Cutwidth.Bisection.Internal.card_boundaryLift_le {W : Type} [Fintype W] (H : SimpleGraph W) {S X : Finset W} (degree : ∀ v ∈ X, H.degree v ≤ 3) : (boundaryLift H S X).card ≤ 4 * X.card

theorem Algebraic.Cutwidth.Bisection.Internal.helpfulness_boundaryLift {W : Type} [Fintype W] (H : SimpleGraph W) {S X : Finset W} (regular : H.IsRegularOfDegree 3) (outside : ∀ c ∈ cutBoundary H S, (H.neighborFinset c \ S).card = 1) (independent : ∀ c ∈ cutBoundary H S, ∀ d ∈ cutBoundary H S, ¬H.Adj c d) (hX : X ⊆ S \ cutBoundary H S) : helpfulness H S (boundaryLift H S X) = ↑(sharedBoundary H S X).card - ↑(H.cutFinset X \ H.cutFinset (cutBoundary H S)).card

theorem Algebraic.Cutwidth.Bisection.Internal.card_cutBoundary_eq_cut {W : Type} [Fintype W] (H : SimpleGraph W) {S : Finset W} (outside : ∀ c ∈ cutBoundary H S, (H.neighborFinset c \ S).card = 1) : (cutBoundary H S).card = (H.cutFinset S).card

theorem Algebraic.Cutwidth.Bisection.Internal.card_boundary_interior_neighbors {W : Type} [Fintype W] (H : SimpleGraph W) {S : Finset W} (regular : H.IsRegularOfDegree 3) (outside : ∀ c ∈ cutBoundary H S, (H.neighborFinset c \ S).card = 1) (independent : ∀ c ∈ cutBoundary H S, ∀ d ∈ cutBoundary H S, ¬H.Adj c d) {c : W} (hc : c ∈ cutBoundary H S) : (H.neighborFinset c ∩ (S \ cutBoundary H S)).card = 2

theorem Algebraic.Cutwidth.Bisection.Internal.card_interior_neighbors {W : Type} [Fintype W] (H : SimpleGraph W) {S : Finset W} (regular : H.IsRegularOfDegree 3) {v : W} (hv : v ∈ S \ cutBoundary H S) : (H.neighborFinset v ∩ cutBoundary H S).card + (H.neighborFinset v ∩ (S \ cutBoundary H S)).card = 3

theorem Algebraic.Cutwidth.Bisection.Internal.boundary_red_density {W : Type} [Fintype W] (H : SimpleGraph W) {S : Finset W} {ξ : ℝ} (hξ : 0 < ξ) (outside : ∀ c ∈ cutBoundary H S, (H.neighborFinset c \ S).card = 1) (dense : (1 / 3 + ξ) * ↑S.card < ↑(H.cutFinset S).card) : (1 / 2 + 3 * ξ / 2) * ↑(S \ cutBoundary H S).card < ↑(cutBoundary H S).card

theorem Algebraic.Cutwidth.Bisection.Internal.card_interior_edges {W : Type} [Fintype W] (H : SimpleGraph W) {S : Finset W} (regular : H.IsRegularOfDegree 3) (outside : ∀ c ∈ cutBoundary H S, (H.neighborFinset c \ S).card = 1) (independent : ∀ c ∈ cutBoundary H S, ∀ d ∈ cutBoundary H S, ¬H.Adj c d) : 2 * (SimpleGraph.induce {v : W | v ∈ S \ cutBoundary H S} H).edgeFinset.card + 2 * (cutBoundary H S).card = 3 * (S \ cutBoundary H S).card

theorem Algebraic.Cutwidth.Bisection.Internal.exists_small_interior_tree_component {W : Type} [Fintype W] (H : SimpleGraph W) {S : Finset W} (regular : H.IsRegularOfDegree 3) (outside : ∀ c ∈ cutBoundary H S, (H.neighborFinset c \ S).card = 1) (independent : ∀ c ∈ cutBoundary H S, ∀ d ∈ cutBoundary H S, ¬H.Adj c d) {ξ : ℝ} (hξ : 0 < ξ) (dense : (1 / 3 + ξ) * ↑S.card < ↑(H.cutFinset S).card) (M : ℕ) (budget : 1 ≤ (↑M + 1) * (3 * ξ / 2)) : ∃ (C : (SimpleGraph.induce {v : W | v ∈ S \ cutBoundary H S} H).ConnectedComponent), C.toSimpleGraph.IsTree ∧ Fintype.card ↥C ≤ M

theorem Algebraic.Cutwidth.Bisection.Internal.exists_helpful_set_of_red_surplus {W : Type} [Fintype W] (H : SimpleGraph W) {S X : Finset W} (regular : H.IsRegularOfDegree 3) (outside : ∀ c ∈ cutBoundary H S, (H.neighborFinset c \ S).card = 1) (independent : ∀ c ∈ cutBoundary H S, ∀ d ∈ cutBoundary H S, ¬H.Adj c d) (hX : X ⊆ S \ cutBoundary H S) (positive : (H.cutFinset X \ H.cutFinset (cutBoundary H S)).card < (sharedBoundary H S X).card) : ∃ Y ⊆ S, Y.card ≤ 4 * X.card ∧ 1 ≤ helpfulness H S Y