A family of regions with compensating red attachments

The cycle-removal step of Monien and Preis's argument isolates thin paths. For restoration, the relevant data are disjoint regions with at most two black boundary edges, each joined by a red edge to an attached set with empty black cut. Attached sets can overlap one another, but are disjoint from all regions. No path ordering or cycle choice is needed for the simultaneous restoration theorem.

structure Algebraic.Cutwidth.Bisection.RedBlack.RestorationFamily {V E : Type} [Fintype V] (B : SimpleGraph V) (R : Multigraph V E) (ι : Type) : Type

Disjoint regions that can pay for restoration of their black cuts by adding their closed red attachments. This records the data of removed paths; it does not assert that a cycle-removal procedure has produced them.

• region : ι → Finset V

  The regions whose black cuts are temporarily deleted.

• attachment : ι → Finset V

  Closed sets added together with their regions during restoration.

• disjoint : Pairwise fun (i j : ι) => Disjoint (self.region i) (self.region j)
• separate (i j : ι) : Disjoint (self.region i) (self.attachment j)
• closed (i : ι) : B.cutFinset (self.attachment i) = ∅
• boundary (i : ι) : (B.cutFinset (self.region i)).card ≤ 2
• redEdge : ι → E

  A red edge paying for the restored region's remaining black boundary.

• incident (i : ι) : R.fst (self.redEdge i) ∈ self.region i ∧ R.snd (self.redEdge i) ∈ self.attachment i ∨ R.snd (self.redEdge i) ∈ self.region i ∧ R.fst (self.redEdge i) ∈ self.attachment i

def Algebraic.Cutwidth.Bisection.RedBlack.RestorationFamily.restrict {V E ι : Type} [Fintype V] {B : SimpleGraph V} {R : Multigraph V E} (F : RestorationFamily B R ι) (indices : Finset ι) : RestorationFamily B R ↥indices

Retain any chosen subfamily of the regions and their attachments.

Equations

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

noncomputable def Algebraic.Cutwidth.Bisection.RedBlack.RestorationFamily.deletedEdges {V E ι : Type} [Fintype V] [Fintype ι] {B : SimpleGraph V} {R : Multigraph V E} (F : RestorationFamily B R ι) : Finset (Sym2 V)

All black edges removed to isolate the family's regions.

Equations

• F.deletedEdges = Finset.univ.biUnion fun (i : ι) => B.cutFinset (F.region i)

noncomputable def Algebraic.Cutwidth.Bisection.RedBlack.RestorationFamily.deletedGraph {V E ι : Type} [Fintype V] [Fintype ι] {B : SimpleGraph V} {R : Multigraph V E} (F : RestorationFamily B R ι) : SimpleGraph V

The black graph after every region has been isolated.

Equations

• F.deletedGraph = B.deleteEdges ↑F.deletedEdges

theorem Algebraic.Cutwidth.Bisection.RedBlack.RestorationFamily.deletedEdges_restrict {V E ι : Type} [Fintype V] {B : SimpleGraph V} {R : Multigraph V E} (F : RestorationFamily B R ι) (indices : Finset ι) : (F.restrict indices).deletedEdges = indices.biUnion fun (i : ι) => B.cutFinset (F.region i)

Restricting the family deletes exactly the cuts of the selected regions.