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.
Description
Proof of Lemma 4.3. Apply Rödl's theorem with density parameter , then apply Lemma 4.2 with . The resulting set loses at most a factor of two in size and satisfies the required degree bound.