Endpoint marks for isolated regions #
Every edge of a region's black cut assigns one mark to its outside endpoint.
The finite map retains multiplicity when several boundary edges meet the
same vertex. A restoration family's endpoint marks sum these contributions
over its regions. For the shaded subfamily, apply this definition to
F.restrict shaded.
noncomputable def
Algebraic.Cutwidth.Bisection.RedBlack.boundaryMarks
{V : Type}
[Fintype V]
(B : SimpleGraph V)
(P : Finset V)
:
One mark on the outside endpoint of each boundary edge of P.
Equations
- Algebraic.Cutwidth.Bisection.RedBlack.boundaryMarks B P = ∑ e ∈ B.cutFinset P, ∑ v ∈ e.toFinset \ P, Finsupp.single v 1
Instances For
noncomputable def
Algebraic.Cutwidth.Bisection.RedBlack.RestorationFamily.endpointMarks
{V E ι : Type}
[Fintype V]
[Fintype ι]
{B : SimpleGraph V}
{R : Multigraph V E}
(F : RestorationFamily B R ι)
:
Endpoint marks created by isolating all regions of the family.
Equations
- F.endpointMarks = ∑ i : ι, Algebraic.Cutwidth.Bisection.RedBlack.boundaryMarks B (F.region i)