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

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.

Read the Lean proof on GitHub

Description

Rödl's maximum-degree reduction gives a linearly large induced set on which one of the two complementary graphs is 1/6421/64^2-sparse. In the direct orientation, iterate the sparse-house acceleration lemma until the requested parameter is reached. In the complementary orientation, the graph is P5P_5-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.