Draft — mutable and not usable as a dependency; its citation marks the draft state.

Proof of `Anticomponent or complete blockade`

groundedproofs/Lax57Proofs/AnticomponentBlockade.lean · lax-57

What this proof establishes

no assumptions

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Read the Lean proof on GitHub

Description

Consider the connected components of the complement induced on TT. A component of size at least T/Q2|T|/Q^2 gives the first outcome. Otherwise, greedily group whole components into QQ disjoint families, each of size at least T/(4Q3)|T|/(4Q^3). Distinct families are anticomplete in the complement and therefore complete in GG.