Endpoint marks record boundary edges and degree loss

Each cut edge supplies one outside mark. For a restoration family, marks at vertices outside all regions count exactly their incident deleted edges. The original degree is the sum of the remaining degree and these marks. On a set avoiding every region, marks count the region cuts crossing it; these are the incidences that require compensation during restoration.

theorem Algebraic.Cutwidth.Bisection.RedBlack.degree_boundaryMarks {V : Type} [Fintype V] (B : SimpleGraph V) (P : Finset V) : Finsupp.degree (boundaryMarks B P) = (B.cutFinset P).card

Every boundary edge gives exactly one outside mark.

theorem Algebraic.Cutwidth.Bisection.RedBlack.boundaryMarks_apply {V : Type} [Fintype V] (B : SimpleGraph V) (P : Finset V) (v : V) : (boundaryMarks B P) v = if v ∈ P then 0 else (B.incidenceFinset v ∩ B.cutFinset P).card

Marks at an outside vertex count its incident boundary edges; inside vertices get none.

theorem Algebraic.Cutwidth.Bisection.RedBlack.sum_boundaryMarks {V : Type} [Fintype V] (B : SimpleGraph V) (P : Finset V) {X : Finset V} (fresh : Disjoint X P) : ∑ v ∈ X, (boundaryMarks B P) v = (B.cutFinset P ∩ B.cutFinset X).card

On a set disjoint from a region, its marks count exactly the shared cut edges.

theorem Algebraic.Cutwidth.Bisection.RedBlack.RestorationFamily.degree_endpointMarks {V : Type} [Fintype V] {E ι : Type} [Fintype ι] {B : SimpleGraph V} {R : Multigraph V E} (F : RestorationFamily B R ι) : Finsupp.degree F.endpointMarks = ∑ i : ι, (B.cutFinset (F.region i)).card

Total endpoint marks equal the sum of the region boundary sizes.

theorem Algebraic.Cutwidth.Bisection.RedBlack.RestorationFamily.sum_endpointMarks {V : Type} [Fintype V] {E ι : Type} [Fintype ι] {B : SimpleGraph V} {R : Multigraph V E} (F : RestorationFamily B R ι) {X : Finset V} (fresh : ∀ (i : ι), Disjoint X (F.region i)) : ∑ v ∈ X, F.endpointMarks v = ∑ i : ι, (B.cutFinset (F.region i) ∩ B.cutFinset X).card

Marks on an outside set count all region boundaries meeting its cut.

theorem Algebraic.Cutwidth.Bisection.RedBlack.RestorationFamily.endpointMarks_apply {V : Type} [Fintype V] {E ι : Type} [Fintype ι] {B : SimpleGraph V} {R : Multigraph V E} (F : RestorationFamily B R ι) {v : V} (outside : ∀ (i : ι), v ∉ F.region i) : F.endpointMarks v = (B.incidenceFinset v ∩ F.deletedEdges).card

At an outside vertex, endpoint marks count precisely the incident deleted edges.

theorem Algebraic.Cutwidth.Bisection.RedBlack.RestorationFamily.degree_deletedGraph_add_endpointMarks {V : Type} [Fintype V] {E ι : Type} [Fintype ι] {B : SimpleGraph V} {R : Multigraph V E} (F : RestorationFamily B R ι) {v : V} (outside : ∀ (i : ι), v ∉ F.region i) : F.deletedGraph.degree v + F.endpointMarks v = B.degree v

Isolating the regions reduces each outside vertex's degree by exactly its mark count.