Proof of `Anticomplete pairs in sparse -free graphs`
groundedproofs/Lax57Proofs/SparseP5Pair.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.
Description
Repeatedly choose a large connected component, producing nested connected sets. Sparsity keeps the successive neighborhoods small. If no large anticomplete pair exists, two applications of connectivity across a cut produce five vertices that induce .
Attribution
Lemma 4.4 of Nguyen, Scott, and Seymour, with cleared denominators.