Proof of `Restricted set or uniform blockade in a house-free graph`
groundedproofs/Lax57Proofs/HouseDichotomy.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
Rödl's maximum-degree reduction gives a linearly large induced set on which one of the two complementary graphs is -sparse. In the direct orientation, iterate the sparse-house acceleration lemma until the requested parameter is reached. In the complementary orientation, the graph is -free, so the sparse anticomplete-pair lemma gives a complete two-block blockade in the original graph. A single exponent absorbs the fixed and polynomial losses.
Attribution
This packages the iteration in the proof of Lemma 7.3 of Nguyen, Scott, and Seymour, using their Lemmas 4.4 and 7.2 and the maximum-degree form of Rödl's theorem already formalized in Lax 54.