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

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.

Read the Lean proof on GitHub

Description

Apply the semisparse-blockade theorem at scale L=Q4dL=Q^{4d} 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 QQ-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.