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

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.

Read the Lean proof on GitHub

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 xyxy; their endpoints lie in N(x)∪N(y)N(x) ∪ N(y). Thus at most 2d2d represented vertices use that host vertex. Apply the connected-set decomposition transfer with this load bound.

Attribution

Bonnet–Chang, Lemma 9.