The bounded positive-set theorem from red density #
First collect all original black components with at most M vertices.
A red edge within this union already gives a small positive witness.
Otherwise partition the remaining components into bounded connected sets
and apply the cluster incidence count. This supplies the red/black lemma
without a leaf reorganization or color-swap invariant.
theorem
Algebraic.Cutwidth.Bisection.RedBlack.Internal.exists_positive_of_density
{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 : ℕ)
(positive : 0 < M)
(density : (M + 4) * Fintype.card V < 2 * M * Fintype.card E)
:
theorem
Algebraic.Cutwidth.Bisection.RedBlack.Internal.exists_positive_of_red_density
{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 : ℕ)
(positive : 0 < M)
{ε : ℝ}
(budget : 2 ≤ ε * ↑M)
(density : (1 / 2 + ε) * ↑(Fintype.card V) < ↑(Fintype.card E))
: