Proof of `Treewidth transfer through an almost-embedding`
groundedproofs/Lax263307Proofs/AlmostEmbeddings.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
Represent a vertex by the union of its incident routes, connected through its mapped image. At a host vertex, all routes present share an endpoint with any one present route ; their endpoints lie in . Thus at most represented vertices use that host vertex. Apply the connected-set decomposition transfer with this load bound.
Attribution
Bonnet–Chang, Lemma 9.