A cut witnessing many collisions #
A spanning forest has the same nonisolated vertices as the original graph. Its two-coloring gives a cut across which every nonisolated vertex has a neighbor. At least half of any specified set of nonisolated vertices lie on one side of this cut. Restricting that side to the specified vertices keeps all its witnesses outside the chosen set.
For the scheduler, vertices are requests together with an occupied-set vertex. Conditioning on directions outside the selected requests then makes their collision tests independent. No independence of graph edges is needed.
theorem
Algebraic.MassProduction.Nonuniform.existsCollisionCut
{Vertex : Type u_1}
(graph : SimpleGraph Vertex)
(bad : Finset Vertex)
(nonisolated : ∀ vertex ∈ bad, ∃ (neighbor : Vertex), graph.Adj vertex neighbor)
:
A finite set of nonisolated vertices contains a subset of at least half its cardinality whose vertices all have neighbors outside the subset.