Counting endpoint marks and lost degrees

A cut edge has exactly one outside endpoint, so its contribution has total one. On a set avoiding the region, its marks count exactly those boundary edges crossing the set. For disjoint regions, marks on an outside vertex are precisely its incident deleted edges.

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

theorem Algebraic.Cutwidth.Bisection.RedBlack.RestorationFamily.Internal.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

theorem Algebraic.Cutwidth.Bisection.RedBlack.RestorationFamily.Internal.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

theorem Algebraic.Cutwidth.Bisection.RedBlack.RestorationFamily.Internal.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

theorem Algebraic.Cutwidth.Bisection.RedBlack.RestorationFamily.Internal.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

theorem Algebraic.Cutwidth.Bisection.RedBlack.RestorationFamily.Internal.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

theorem Algebraic.Cutwidth.Bisection.RedBlack.RestorationFamily.Internal.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