Lifting a red/black witness through the cut boundary

In the normalized side of Monien and Preis's helpful-set argument, each boundary vertex has one outside neighbor and two nonboundary neighbors. It represents a red edge between those two neighbors. Boundary vertices remain distinct, so parallel red edges retain their multiplicity.

noncomputable def Algebraic.Cutwidth.Bisection.boundaryLift {W : Type} (H : SimpleGraph W) (S X : Finset W) : Finset W

Add every boundary vertex adjacent to the chosen interior set.

Equations

• Algebraic.Cutwidth.Bisection.boundaryLift H S X = X ∪ {c ∈ Algebraic.Cutwidth.cutBoundary H S | ∃ x ∈ X, H.Adj c x}

noncomputable def Algebraic.Cutwidth.Bisection.sharedBoundary {W : Type} [Fintype W] (H : SimpleGraph W) (S X : Finset W) : Finset W

Boundary vertices incident to at least two chosen vertices. When each boundary vertex has two interior neighbors, these count internal red edges, including parallel edges represented by different boundary vertices.

Equations

• Algebraic.Cutwidth.Bisection.sharedBoundary H S X = {c ∈ Algebraic.Cutwidth.cutBoundary H S | 2 ≤ (H.neighborFinset c ∩ X).card}