Proof of `Treewidth is at most feedback vertex number plus one`

groundedproofs/Lax379983Proofs/TreewidthBound.lean · lax-379983

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.

Read the Lean proof on GitHub

Description

Choose a minimum feedback vertex set SS. The remaining forest has a tree decomposition with at most two vertices in each bag: for a nonempty forest, extend it to a tree, root it, and use each vertex together with its parent as a bag, with a singleton bag at the root. For the empty forest, use one empty bag. Adding SS to every bag covers all original edges and preserves connectedness of the bags containing each vertex. Each new bag has at most S+2|S|+2 vertices, so its width is at most S+1|S|+1.