Proof of `Maximum-degree form of Rödl's theorem`

groundedproofs/Lax54Proofs/MaximumDegreeReduction.lean · lax-54

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

In the paper

  • page 10 of this submission's paper

Description

Proof of Lemma 4.3. Apply Rödl's theorem with density parameter 4E4E, then apply Lemma 4.2 with m=⌈∣Z∣/2⌉m=\lceil |Z|/2\rceil. The resulting set loses at most a factor of two in size and satisfies the required degree bound.