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

Proof of `Treedepth and Δ-forestwidth` (2nd statement)

groundedproofs/Lax461425Proofs/TreedepthForestwidth.lean · lax-461425

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

Each vertex is placed at its unique top node. Vertices at a node of depth dd receive the ranks (d−1)(w+1),…,d(w+1)−1(d - 1)(w + 1), …, d(w + 1) - 1 in a fixed order, and uu is an ancestor of vv if it has smaller rank and its top node is an ancestor of that of vv. The endpoints of an edge lie in a common bag, so their top nodes are both ancestors of that node, hence comparable.