Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Proof of `Deleting high-degree vertices in an independent blow-up` (3rd statement)

groundedproofs/Lax263307Proofs/BlowUpDeletion.lean · lax-263307

What this proof establishes

thm✓Lax263307.BlowUpDeletion (3rd statement)

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

Choose ss to be the ceiling of (m+1)((1−b)/2)(m+1)^((1-b)/2). The deletion term and the lifted-bag term then both have exponent (1+b)/2(1+b)/2, with the additional one accounting for isolated vertices.

Attribution

Bonnet–Chang, the threshold optimization in Lemma 16.