Proof of `Treewidth loss under edge deletion`
groundedproofs/Lax263307Proofs/EdgeDeletionWidth.lean · lax-263307
What this proof establishes
no assumptions
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
Choose the first endpoint of each deleted unordered pair. Their image has cardinality at most the number of deleted edges and meets every deleted edge. Add this image to every bag, restoring coverage while preserving connected bag indices. Bound each enlarged bag by the sum of its two constituent sizes.
Attribution
The deletion estimate used in Bonnet–Chang, Lemma 11.