Positive sets in a red/black graph

Monien and Preis's core lemma seeks a set with more internal red edges than external black edges. The black graph is simple; the red graph retains edge identities, allowing parallel edges created by suppressing boundary vertices. Degree and density assumptions belong to the theorems that need them, since the proof also deletes black edges.

noncomputable def Algebraic.Cutwidth.Bisection.RedBlack.internalEdges {V E : Type} [Fintype E] (R : Multigraph V E) (X : Finset V) : Finset E

Red edges with both endpoints in the chosen set, counted with multiplicity.

Equations

• Algebraic.Cutwidth.Bisection.RedBlack.internalEdges R X = {e : E | R.fst e ∈ X ∧ R.snd e ∈ X}

def Algebraic.Cutwidth.Bisection.RedBlack.Positive {V E : Type} [Fintype V] [Fintype E] (B : SimpleGraph V) (R : Multigraph V E) (X : Finset V) : Prop

More internal red edges than external black edges.

Equations

• Algebraic.Cutwidth.Bisection.RedBlack.Positive B R X = ((B.cutFinset X).card < (Algebraic.Cutwidth.Bisection.RedBlack.internalEdges R X).card)