Suppressing an independent cut boundary

A boundary vertex with two interior neighbors becomes a red edge between them. Its identity is the edge identity, so parallel edges are preserved. The black graph is the original graph induced on the interior vertices.

structure Algebraic.Cutwidth.Bisection.BoundarySuppression {W : Type} (H : SimpleGraph W) (S : Finset W) : Type

A loopless red graph on the interior of a side. Its edges are precisely the boundary vertices, and red incidence is original boundary adjacency.

• red : Multigraph ↥(S \ cutBoundary H S) ↥(cutBoundary H S)

  Suppressed boundary vertices retain distinct edge identities.

• loopless : self.red.Loopless

  A boundary vertex has two distinct interior neighbors.

• incident_iff (v : ↥(S \ cutBoundary H S)) (c : ↥(cutBoundary H S)) : self.red.Incident v c ↔ H.Adj ↑c ↑v

  The two red endpoints are exactly the original interior neighbors.