Proof of `Tree-decomposition transfer through connected vertex representations`
groundedproofs/Lax263307Proofs/ConnectedRepresentations.lean · lax-263307
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
Keep the original tree and replace each bag by all represented vertices whose carriers meet it. Connected carriers preserve connected bag indices; touching carriers ensure edge coverage. Sum the load bound over each original bag to obtain the new bag-size bound.
Attribution
The transfer construction in Bonnet–Chang, Lemma 9.