Proof of `Per-Client Fairness Parameters at Treewidth Four` (6th statement)
groundedproofs/Lax117284Proofs/Lemma14Treewidth.lean · lax-117284
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
The overall conflict graph of the constructed instance has a tree decomposition of width four: on every day the dummy client conflicts with the clients that take no part in the gadget and with none that does, so apart from the dummy and the two interaction clients, which every bag holds, the conflicts that remain are those inside a day's gadget — a vertex client with the selection client of its colour, and a vertex client with one of its own incidence clients.