Canonical connected regions among eligible vertices

The path system in Monien and Preis's red/black argument starts with an eligible set of unmarked black degree-two vertices. Its regions are the connected components induced on that set, viewed back in the original vertex type. The definition also makes sense for any eligible set; degree assumptions enter the theorems about spanning paths and boundary size.

noncomputable def Algebraic.Cutwidth.Bisection.RedBlack.PathSystem.region {V : Type} (B : SimpleGraph V) (U : Finset V) (C : (SimpleGraph.induce {v : V | v ∈ U} B).ConnectedComponent) : Finset V

The vertices of an induced connected component, in the ambient vertex type.

Equations

• Algebraic.Cutwidth.Bisection.RedBlack.PathSystem.region B U C = Finset.image Subtype.val C.supp.toFinset

noncomputable def Algebraic.Cutwidth.Bisection.RedBlack.PathSystem.attachmentEdges {V E : Type} [Fintype V] [Fintype E] (B : SimpleGraph V) (R : Multigraph V E) (P : Finset V) (M : ℕ) : Finset E

Red edges joining the region to a black component of at most M vertices.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algebraic.Cutwidth.Bisection.RedBlack.PathSystem.attachmentComponent {V E : Type} [Fintype V] (B : SimpleGraph V) (R : Multigraph V E) (P : Finset V) (M : ℕ) (e : E) : B.ConnectedComponent

The attached black component, choosing the second endpoint when it qualifies. Only values on attachmentEdges are used.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algebraic.Cutwidth.Bisection.RedBlack.PathSystem.attachment {V E : Type} [Fintype V] (B : SimpleGraph V) (R : Multigraph V E) (P : Finset V) (M : ℕ) (e : E) : Finset V

The vertices of the attached small black component.

Equations

• Algebraic.Cutwidth.Bisection.RedBlack.PathSystem.attachment B R P M e = (Algebraic.Cutwidth.Bisection.RedBlack.PathSystem.attachmentComponent B R P M e).supp.toFinset

noncomputable def Algebraic.Cutwidth.Bisection.RedBlack.PathSystem.thinComponents {V E : Type} [Fintype V] [Fintype E] (B : SimpleGraph V) (R : Multigraph V E) (U : Finset V) (M : ℕ) : Finset (SimpleGraph.induce {v : V | v ∈ U} B).ConnectedComponent

Eligible components with at least one red attachment per M vertices.

Equations

• One or more equations did not get rendered due to their size.