Proof of `Prepared sparse-or-complete house blockades`
groundedproofs/Lax57Proofs/PreparedHouseBlockade.lean · lax-57
What this proof establishes
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
Apply the semisparse-blockade theorem at scale and sample each block to a common size. Simultaneous cleaning retains at least half of every sample and makes each noncomplete pair sparse in both directions. In each cleaned block, either the complement has a large connected component, or its components yield the required complete -blockade. Choosing a large component in every block preserves the relations between blocks.
Attribution
Claim 7.1.1 of Nguyen, Scott, and Seymour, with reciprocal parameters and rounding expressed over the natural numbers.