Counting red incidences across clusters

In a loopless multigraph, summing degrees over a set counts its crossing edges once and its internal edges twice. A partition of the complementary vertices counts every crossing edge exactly once through its outside part. Parallel edges retain their individual edge identities throughout.

theorem Algebraic.Cutwidth.Bisection.RedBlack.Internal.red_degree_sum_cut {V E : Type} [Fintype E] (R : Multigraph V E) (loopless : R.Loopless) (X : Finset V) : (R.cut X).card + 2 * (internalEdges R X).card = ∑ v ∈ X, R.degree v

theorem Algebraic.Cutwidth.Bisection.RedBlack.Internal.red_sum_degrees {V E : Type} [Fintype E] (R : Multigraph V E) [Fintype V] (loopless : R.Loopless) : ∑ v : V, R.degree v = 2 * Fintype.card E

theorem Algebraic.Cutwidth.Bisection.RedBlack.Internal.sum_card_cut_inter_partition {V E : Type} [Fintype E] (R : Multigraph V E) [Fintype V] (U : Finset V) (parts : Finset (Finset V)) (disjoint : (↑parts).Pairwise Disjoint) (cover : parts.biUnion id = Finset.univ \ U) : ∑ P ∈ parts, (R.cut U ∩ R.cut P).card = (R.cut U).card