The suppressed graph and its helpful-set transfer

An independent boundary with one outside neighbor per vertex in a cubic graph has a loopless red suppression. The original interior edges form the black graph. The red and black degrees sum to three, internal red edges count shared boundary vertices, and black cuts count the remaining interior crossings. Thus every positive red/black set lifts to a helpful move.

NeighborNormalization supplies normalization of an arbitrary cubic side, unless a uniformly small helpful set already exists. Its exclusion of interior vertices with three boundary neighbors ensures positive black degree.

theorem Algebraic.Cutwidth.Bisection.exists_boundarySuppression {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) : Nonempty (BoundarySuppression H S)

Suppress each boundary vertex to the red edge joining its two interior neighbors.

theorem Algebraic.Cutwidth.Bisection.boundaryInterior_cut_card {W : Type} [Fintype W] (H : SimpleGraph W) {S : Finset W} (X : Finset ↥(S \ cutBoundary H S)) : ((SimpleGraph.induce {v : W | v ∈ S \ cutBoundary H S} H).cutFinset X).card = (H.cutFinset (Finset.map (Function.Embedding.subtype fun (v : W) => v ∈ S \ cutBoundary H S) X) \ H.cutFinset (cutBoundary H S)).card

The cut in the black graph equals the original cut after removing edges incident to the boundary.

theorem Algebraic.Cutwidth.Bisection.BoundarySuppression.red_degree {W : Type} [Fintype W] {H : SimpleGraph W} {S : Finset W} (Q : BoundarySuppression H S) (v : ↥(S \ cutBoundary H S)) : Q.red.degree v = (H.neighborFinset ↑v ∩ cutBoundary H S).card

Red degree counts the original boundary neighbors.

theorem Algebraic.Cutwidth.Bisection.BoundarySuppression.degree_sum {W : Type} [Fintype W] {H : SimpleGraph W} {S : Finset W} (Q : BoundarySuppression H S) (regular : H.IsRegularOfDegree 3) (v : ↥(S \ cutBoundary H S)) : (SimpleGraph.induce {v : W | v ∈ S \ cutBoundary H S} H).degree v + Q.red.degree v = 3

Suppression preserves the total degree three at each interior vertex.

theorem Algebraic.Cutwidth.Bisection.BoundarySuppression.internalEdges_card {W : Type} [Fintype W] {H : SimpleGraph W} {S : Finset W} (Q : BoundarySuppression H S) (X : Finset ↥(S \ cutBoundary H S)) : (RedBlack.internalEdges Q.red X).card = (sharedBoundary H S (Finset.map (Function.Embedding.subtype fun (v : W) => v ∈ S \ cutBoundary H S) X)).card

Internal red edges count shared boundary vertices, including parallel edges.

theorem Algebraic.Cutwidth.Bisection.BoundarySuppression.exists_helpful_set_of_positive {W : Type} [Fintype W] {H : SimpleGraph W} {S : Finset W} (Q : BoundarySuppression H S) (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) {X : Finset ↥(S \ cutBoundary H S)} (positive : RedBlack.Positive (SimpleGraph.induce {v : W | v ∈ S \ cutBoundary H S} H) Q.red X) : ∃ Y ⊆ S, Y.card ≤ 4 * X.card ∧ 1 ≤ helpfulness H S Y

A positive set in the suppressed graph gives a helpful move in the original side with at most four times as many vertices.