Proof of `Tree decompositions from recursive balanced separators` (2nd statement)
groundedproofs/Lax263307Proofs/SeparatorDecompositions.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
Induct on the graph order. Relabel each component by a finite numbered vertex set, apply heredity and the induction hypothesis, and pull its decomposition back. Its edge count cannot increase, and balance consumes one depth level. Joining the children adds just the separator bound.