Seymour--Thomas duality

The Seymour--Thomas theorem ("brambles and tree width", J. Combin. Theory Ser. B 58 (1993)) says that the maximum order of a bramble of H equals treewidth H + 1. TreewidthGonality/Gonality/TreewidthGonality.lean consumes the existence of a bramble whose order is exactly treewidth H + 1.

This module assembles that statement from TreewidthGonality/Treewidth/SeymourThomasInduction.lean, which proves the hard half (some bramble has order at least treewidth H + 1) following Bellenbaum--Diestel, Two short proofs concerning tree-decompositions, §4.

Why the easy half is not proved

Getting order exactly treewidth H + 1 classically needs the other inequality: every bramble is covered by some bag, so no bramble has order above treewidth H + 1. Its proof orients every edge of the decomposition tree towards the side that covers the bramble and takes the end of a maximal directed path — a second consumer of Bellenbaum--Diestel's Lemma 1.

It is avoidable. The order of a bramble is monotone in its member family (Bramble.order_restrict_le) and increases by at most one when a single member is adjoined (Bramble.order_le_succ_erase: a hitting set of the smaller family plus one vertex of the new member hits the larger one). Peeling members off one at a time therefore realizes every value between 0 and the order, so a bramble of order ≥ treewidth H + 1 contains a sub-bramble of order exactly treewidth H + 1. That is exists_subfamily_order_eq below, and it is strictly cheaper than the easy half of duality.

theorem Utilities.Treewidth.Bramble.order_restrict_self {V : Type u} [DecidableEq V] {H : SimpleGraph V} (𝔅 : Bramble H) : (𝔅.restrict 𝔅.members ⋯).order = 𝔅.order

Restricting to the full member family changes nothing.

theorem Utilities.Treewidth.Bramble.order_restrict_empty {V : Type u} [DecidableEq V] {H : SimpleGraph V} (𝔅 : Bramble H) (h : ∅ ⊆ 𝔅.members) : (𝔅.restrict ∅ h).order = 0

The empty sub-bramble has order 0: the empty set hits it vacuously.

theorem Utilities.Treewidth.Bramble.order_le_succ_erase {V : Type u} [DecidableEq V] {H : SimpleGraph V} [Finite V] (𝔅 : Bramble H) {M : Finset (Finset V)} (hM : M ⊆ 𝔅.members) {B : Finset V} (hB : B ∈ M) : (𝔅.restrict M hM).order ≤ (𝔅.restrict (M.erase B) ⋯).order + 1

Removing one member drops the order by at most one. A hitting set of the smaller family together with one vertex of the removed member hits the larger family.

theorem Utilities.Treewidth.Bramble.exists_subfamily_order_eq {V : Type u} [DecidableEq V] {H : SimpleGraph V} [Finite V] (𝔅 : Bramble H) (M : Finset (Finset V)) (hM : M ⊆ 𝔅.members) (m : ℕ) : m ≤ (𝔅.restrict M hM).order → ∃ (M' : Finset (Finset V)) (hM' : M' ⊆ M), (𝔅.restrict M' ⋯).order = m

Discrete intermediate value for the order of sub-brambles. Every value below the order of a family is attained by some subfamily.

Discharge plan: strong induction on M. If m = (restrict M).order take M' := M. Otherwise m < (restrict M).order, so M is nonempty (order_restrict_empty); pick B ∈ M and apply the induction hypothesis to M.erase B, whose order is at least m by order_le_succ_erase.

theorem Utilities.Treewidth.exists_bramble_of_treewidth {V : Type u} [Finite V] [DecidableEq V] [Nonempty V] (H : SimpleGraph V) : ∃ (𝔅 : Bramble H), 𝔅.order = treewidth H + 1

Seymour--Thomas duality, hard direction. Every graph carries a bramble whose order is exactly treewidth H + 1.

Nonempty V is required: on the empty graph both treewidth and the order of the empty bramble are 0, and there is no bramble of order 1.

Proved 2026-08-25 from exists_bramble_treewidth_succ_le (Bellenbaum--Diestel's Theorem 5, forward direction, with Menger's theorem replaced by an explicit separator) and Bramble.exists_subfamily_order_eq (which supplies exactness without the easy half of duality).