Lax Lean Archive

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

Proof of `Sparse-house acceleration`

groundedproofs/Lax57Proofs/SparseHouseAcceleration.lean · lax-57

What this proof establishes

thm✓Lax57.SparseHouseAcceleration

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 sparse-house trichotomy at Q=R2/2Q=R^2/2. Its sparse and complete outcomes give the required alternatives after rescaling. In the peel outcome, repeatedly remove the anticomplete piece. Each removal loses at most a 3/Q3/Q fraction of the current set, so after RR steps at least half of the original set remains. The removed pieces form the required anticomplete RR-blockade.

Attribution

This is the maximal-peeling proof of Lemma 7.2 of Nguyen, Scott, and Seymour, stated with square reciprocal parameters and cleared denominators.