Finding a positive set among connected clusters #
Partition the vertices outside small black components into connected sets. If no red edge joins two small components, the red degree of their union counts attachments to these clusters exactly. Connectedness bounds the sum of the clusters' black cuts. Total degree three and sufficient red density then force some cluster to have more red attachments than black crossings. Adding the attached small components produces a bounded positive witness.
theorem
Algebraic.Cutwidth.Bisection.RedBlack.Internal.exists_positive_of_partition
{V E : Type}
[Fintype V]
[Fintype E]
(B : SimpleGraph V)
(R : Multigraph V E)
(loopless : R.Loopless)
(degree : ∀ (v : V), B.degree v + R.degree v = 3)
(M K : ℕ)
(U : Finset V)
(small : ∀ v ∈ U, Fintype.card ↥(B.connectedComponentMk v) ≤ M)
(noInside : internalEdges R U = ∅)
(parts : Finset (Finset V))
(disjoint : (↑parts).Pairwise Disjoint)
(cover : parts.biUnion id = Finset.univ \ U)
(connected : ∀ P ∈ parts, (SimpleGraph.induce {v : V | v ∈ P} B).Connected)
(bounded : ∀ P ∈ parts, P.card ≤ K)
(count : M * parts.card ≤ 2 * (Finset.univ \ U).card)
(density : (M + 4) * Fintype.card V < 2 * M * Fintype.card E)
: