The Bellenbaum--Diestel induction

The forward half of the tree-width duality theorem: if no bramble of H has order > k, then treewidth H < k, proved exactly as in Bellenbaum--Diestel, Two short proofs concerning tree-decompositions, Theorem 5, except that the appeal to Menger's theorem is replaced by the explicit separator rerootSep below.

The induction

A decomposition is 𝔅-admissible when every bag of order > k fails to cover 𝔅. The statement proved by induction is

for every bramble 𝔅 there is a 𝔅-admissible decomposition of H,

by induction on 2 ^ |V| − |𝔅.members|, i.e. downward on the number of members: the induction hypothesis is applied to 𝔅 ∪ {C} for a component C of H − X, X a minimum cover of 𝔅. Applying the result to the empty bramble — every set covers it — forces every bag to have at most k vertices, hence treewidth H ≤ k − 1.

The Menger-free step

Where the paper produces ℓ = |X| disjoint X–V_s paths from Menger's theorem and reads |W_t| ≤ |V_t| off them, this development exhibits the single set

rerootSep t = (bag t \ (C ∪ X)) ∪ (X \ (Z t \ bag t))

directly, proves that it separates X from bag s (rerootSep_separates, using only Lemma 1), and concludes |rerootSep t| ≥ |X| from Lemma 4 plus minimality of X — the same two facts the paper already uses. The counting then falls out (rerootBag_card_le). Mathlib has no Menger's theorem, no vertex separators, and no treewidth, so this is what makes the campaign finite.

Admissibility

def Utilities.Treewidth.Bramble.Admissible {V : Type u} [DecidableEq V] {H : SimpleGraph V} (k : ℕ) (𝔅 : Bramble H) {U : Finset V} (D : PartialDecomposition H U) : Prop

A partial decomposition is 𝔅-admissible when every bag with more than k vertices fails to cover 𝔅.

Equations

• Utilities.Treewidth.Bramble.Admissible k 𝔅 D = ∀ (t : D.Node), k < (D.bag t).card → ¬𝔅.IsHittingSet (D.bag t)

theorem Utilities.Treewidth.Bramble.admissible_single {V : Type u} [DecidableEq V] {H : SimpleGraph V} (𝔅 : Bramble H) {k : ℕ} {X : Finset V} (h : X.card ≤ k) : Admissible k 𝔅 (PartialDecomposition.single H X)

The one-bag decomposition is admissible as soon as its bag is small.

theorem Utilities.Treewidth.Bramble.admissible_pairDecomp {V : Type u} [DecidableEq V] {H : SimpleGraph V} (𝔅 : Bramble H) {k : ℕ} {X Y : Finset V} (hedge : ∀ v ∈ X ∪ Y, ∀ w ∈ X ∪ Y, H.Adj v w → v ∈ X ∧ w ∈ X ∨ v ∈ Y ∧ w ∈ Y) (hX : X.card ≤ k) (hY : ¬𝔅.IsHittingSet Y) : Admissible k 𝔅 (PartialDecomposition.pairDecomp H X Y hedge)

The two-bag decomposition is admissible when one bag is small and the other fails to cover.

theorem Utilities.Treewidth.Bramble.admissible_join {V : Type u} [DecidableEq V] {H : SimpleGraph V} (𝔅 : Bramble H) {k : ℕ} {U₁ U₂ X : Finset V} {D₁ : PartialDecomposition H U₁} {r₁ : D₁.Node} {h₁ : D₁.bag r₁ = X} {D₂ : PartialDecomposition H U₂} {r₂ : D₂.Node} {h₂ : D₂.bag r₂ = X} {hcap : ∀ v ∈ U₁, v ∈ U₂ → v ∈ X} {hsep : ∀ v ∈ U₁, ∀ w ∈ U₂, v ∉ X → w ∉ X → ¬H.Adj v w} (a₁ : Admissible k 𝔅 D₁) (a₂ : Admissible k 𝔅 D₂) : Admissible k 𝔅 (D₁.join r₁ h₁ D₂ r₂ h₂ hcap hsep)

A join of admissible decompositions is admissible: its bags are exactly the bags of the two pieces.

Two small brambles

def Utilities.Treewidth.Bramble.empty {V : Type u} [DecidableEq V] (H : SimpleGraph V) : Bramble H

The empty bramble. Every set covers it, which is what makes the base case of the induction say something.

Equations

• Utilities.Treewidth.Bramble.empty H = { members := ∅, connected_mem := ⋯, touching := ⋯ }

@[simp]

theorem Utilities.Treewidth.Bramble.empty_members {V : Type u} [DecidableEq V] (H : SimpleGraph V) : (empty H).members = ∅

theorem Utilities.Treewidth.Bramble.isHittingSet_empty {V : Type u} [DecidableEq V] {H : SimpleGraph V} (S : Finset V) : (empty H).IsHittingSet S

theorem Utilities.Treewidth.Bramble.connected_induce_singleton {V : Type u} (H : SimpleGraph V) (v : V) : (SimpleGraph.induce (↑{v}) H).Connected

A one-element vertex set induces a connected subgraph.

def Utilities.Treewidth.Bramble.singletonBramble {V : Type u} [DecidableEq V] (H : SimpleGraph V) (v : V) : Bramble H

The one-member bramble {{v}}, of order 1. It is what rules out k = 0 when V is nonempty.

Equations

• Utilities.Treewidth.Bramble.singletonBramble H v = { members := {{v}}, connected_mem := ⋯, touching := ⋯ }

theorem Utilities.Treewidth.Bramble.one_le_order_singletonBramble {V : Type u} [DecidableEq V] [Finite V] (H : SimpleGraph V) (v : V) : 1 ≤ (singletonBramble H v).order

Adding one member

def Utilities.Treewidth.Bramble.insertMember {V : Type u} [DecidableEq V] {H : SimpleGraph V} (𝔅 : Bramble H) (C : Finset V) (hC : (SimpleGraph.induce (↑C) H).Connected) (htouch : ∀ B ∈ 𝔅.members, (SimpleGraph.induce (↑(C ∪ B)) H).Connected) : Bramble H

Adjoin a connected set touching every member.

Equations

• 𝔅.insertMember C hC htouch = { members := insert C 𝔅.members, connected_mem := ⋯, touching := ⋯ }

@[simp]

theorem Utilities.Treewidth.Bramble.insertMember_members {V : Type u} [DecidableEq V] {H : SimpleGraph V} (𝔅 : Bramble H) (C : Finset V) (hC : (SimpleGraph.induce (↑C) H).Connected) (htouch : ∀ B ∈ 𝔅.members, (SimpleGraph.induce (↑(C ∪ B)) H).Connected) : (𝔅.insertMember C hC htouch).members = insert C 𝔅.members

theorem Utilities.Treewidth.Bramble.card_lt_card_insertMember {V : Type u} [DecidableEq V] {H : SimpleGraph V} (𝔅 : Bramble H) (C : Finset V) (hC : (SimpleGraph.induce (↑C) H).Connected) (htouch : ∀ B ∈ 𝔅.members, (SimpleGraph.induce (↑(C ∪ B)) H).Connected) (hCnot : C ∉ 𝔅.members) : 𝔅.members.card < (𝔅.insertMember C hC htouch).members.card

The rerooted decomposition 𝒟_s(H)

noncomputable def Utilities.Treewidth.rerootZ {V : Type u} [Fintype V] {H : SimpleGraph V} (D : PartialDecomposition H Finset.univ) (s : D.Node) (X : Finset V) (home : V → D.Node) (t : D.Node) : Finset V

The paper's {x ∈ X | t ∈ t_x T s}.

Equations

• Utilities.Treewidth.rerootZ D s X home t = {x ∈ X | t ∈ Utilities.Treewidth.Anc ⋯ s (home x)}

theorem Utilities.Treewidth.mem_rerootZ_iff {V : Type u} [Fintype V] {H : SimpleGraph V} (D : PartialDecomposition H Finset.univ) (s : D.Node) (X : Finset V) (home : V → D.Node) (t : D.Node) (x : V) : x ∈ rerootZ D s X home t ↔ x ∈ X ∧ t ∈ Anc ⋯ s (home x)

noncomputable def Utilities.Treewidth.rerootBag {V : Type u} [Fintype V] [DecidableEq V] {H : SimpleGraph V} (D : PartialDecomposition H Finset.univ) (s : D.Node) (X C : Finset V) (home : V → D.Node) (t : D.Node) : Finset V

The paper's W_t := (V_t ∩ V(H)) ∪ {x ∈ X | t ∈ t_x T s}, with V(H) = C ∪ X.

Equations

• Utilities.Treewidth.rerootBag D s X C home t = D.bag t ∩ (C ∪ X) ∪ Utilities.Treewidth.rerootZ D s X home t

noncomputable def Utilities.Treewidth.rerootSep {V : Type u} [Fintype V] [DecidableEq V] {H : SimpleGraph V} (D : PartialDecomposition H Finset.univ) (s : D.Node) (X C : Finset V) (home : V → D.Node) (t : D.Node) : Finset V

The separator that replaces Menger's theorem: S t = (V_t \ (C ∪ X)) ∪ (X \ Y_t) with Y_t = Z_t \ V_t.

Equations

• Utilities.Treewidth.rerootSep D s X C home t = D.bag t \ (C ∪ X) ∪ X \ (Utilities.Treewidth.rerootZ D s X home t \ D.bag t)

theorem Utilities.Treewidth.rerootSep_separates {V : Type u} [Fintype V] [DecidableEq V] {H : SimpleGraph V} {D : PartialDecomposition H Finset.univ} {s : D.Node} {X C : Finset V} {home : V → D.Node} (hhome : ∀ x ∈ X, x ∈ D.bag (home x)) (hC : IsComponent H X C) (hsC : ∀ v ∈ D.bag s, v ∉ C) (t : D.Node) (a : V) : a ∈ X → ∀ b ∈ D.bag s, ∀ (p : H.Walk a b), ∃ x ∈ p.support, x ∈ rerootSep D s X C home t

The Menger-free separation lemma (blueprint §4, Lemma ST-Sep). Screened exhaustively over all configurations with |V| ≤ 4 and |T| ≤ 3 (680496 of them) and randomly to |V| = 7 before being written down.

Discharge plan. Suppose a walk from a ∈ X to b ∈ bag s avoids rerootSep t. Pass to a path P meeting X only in its first vertex x and bag s only in its last vertex v (Walk.dropUntil at the last X-vertex, then Walk.takeUntil at the first bag s-vertex; both preserve avoidance). Then x ∉ rerootSep t forces x ∈ Z t and x ∉ bag t.

• If t = s: v ∈ bag s = bag t, and avoidance puts v ∈ C ∪ X; v ∈ C contradicts hsC, and v ∈ X forces v = x, contradicting x ∉ bag t.
• Otherwise separates_of_mem_anc (with na := home x, nb := s, using anc_root for t ∉ Anc s s) puts a vertex y ∈ bag t on P; avoidance gives y ∈ C ∪ X; y ∈ X forces y = x, again impossible, so y ∈ C. But P starts outside C and ends outside C, so the successor of the last C-vertex of P is an H-neighbour of C outside C, hence in X by hC.closed, hence equal to x — impossible, since P is a path and x is its first vertex.

theorem Utilities.Treewidth.rerootBag_card_le {V : Type u} [Fintype V] [DecidableEq V] {H : SimpleGraph V} {D : PartialDecomposition H Finset.univ} {s : D.Node} {X C : Finset V} {home : V → D.Node} (𝔅 : Bramble H) (hXcov : 𝔅.IsHittingSet X) (hXmin : ∀ (S : Finset V), 𝔅.IsHittingSet S → X.card ≤ S.card) (hscov : 𝔅.IsHittingSet (D.bag s)) (hhome : ∀ x ∈ X, x ∈ D.bag (home x)) (hC : IsComponent H X C) (hsC : ∀ v ∈ D.bag s, v ∉ C) (t : D.Node) : (rerootBag D s X C home t).card ≤ (D.bag t).card

Lemma 2, Menger-free (blueprint §4, Lemma ST-Card).

Discharge plan: rerootSep_separates + Bramble.isHittingSet_of_separates (Lemma 4) make rerootSep t a cover of 𝔅, so hXmin gives X.card ≤ (rerootSep t).card. The two pieces of rerootSep t are disjoint, so this reads |Z t \ bag t| ≤ |bag t \ (C ∪ X)|; add |bag t ∩ (C ∪ X)| to both sides.

noncomputable def Utilities.Treewidth.rerootDecomp {V : Type u} [Fintype V] [DecidableEq V] {H : SimpleGraph V} {D : PartialDecomposition H Finset.univ} {s : D.Node} {X C : Finset V} {home : V → D.Node} (hhome : ∀ x ∈ X, x ∈ D.bag (home x)) (_hsC : ∀ v ∈ D.bag s, v ∉ C) (_hC : IsComponent H X C) : PartialDecomposition H (C ∪ X)

𝒟_s(H): the same tree, the same isTree, only the bags change. This is why the campaign never needs to re-root a tree.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Utilities.Treewidth.rerootDecomp_bag {V : Type u} [Fintype V] [DecidableEq V] {H : SimpleGraph V} {D : PartialDecomposition H Finset.univ} {s : D.Node} {X C : Finset V} {home : V → D.Node} (hhome : ∀ x ∈ X, x ∈ D.bag (home x)) (hsC : ∀ v ∈ D.bag s, v ∉ C) (hC : IsComponent H X C) (t : D.Node) : (rerootDecomp hhome hsC hC).bag t = rerootBag D s X C home t

theorem Utilities.Treewidth.rerootBag_root {V : Type u} [Fintype V] [DecidableEq V] {H : SimpleGraph V} {D : PartialDecomposition H Finset.univ} {s : D.Node} {X C : Finset V} {home : V → D.Node} (_hhome : ∀ x ∈ X, x ∈ D.bag (home x)) (hsC : ∀ v ∈ D.bag s, v ∉ C) : rerootBag D s X C home s = X

W_s = X.

The per-component step

theorem Utilities.Treewidth.component_step {V : Type u} [Fintype V] [DecidableEq V] {H : SimpleGraph V} (k : ℕ) (𝔅 : Bramble H) (IH : ∀ (𝔅' : Bramble H), 𝔅.members.card < 𝔅'.members.card → ∃ (D : PartialDecomposition H Finset.univ), Bramble.Admissible k 𝔅' D) (hno : ¬∃ (D : PartialDecomposition H Finset.univ), Bramble.Admissible k 𝔅 D) (X : Finset V) (hXcov : 𝔅.IsHittingSet X) (hXmin : ∀ (S : Finset V), 𝔅.IsHittingSet S → X.card ≤ S.card) (hXk : X.card ≤ k) (C : Finset V) (hC : IsComponent H X C) : ∃ (D : PartialDecomposition H (C ∪ X)), Bramble.Admissible k 𝔅 D ∧ ∃ (r : D.Node), D.bag r = X

The paper's (∗), with the "there is nothing more to show" escape already discharged by the ambient hno.

Discharge plan. Put 𝔅' := 𝔅 ∪ {C}.

• If some B ∈ 𝔅.members fails to touch C, then Y := C ∪ N(C) misses B, so PartialDecomposition.pairDecomp H X Y is admissible (Bramble.admissible_pairDecomp), and N(C) ⊆ X makes X ∪ Y = C ∪ X.
• Otherwise 𝔅' is a bramble with strictly more members (C ∉ 𝔅.members because X covers 𝔅 and C ∩ X = ∅), so IH gives a 𝔅'-admissible 𝒟. By hno, 𝒟 is not 𝔅-admissible: some bag s with k < |bag s| covers 𝔅. Since 𝒟 is 𝔅'-admissible, bag s misses C. Then rerootDecomp is the required decomposition: rerootBag_root gives the X part, and admissibility is the paper's last paragraph — a bag W t with k < |W t| meets C, so V t meets C, so V t misses some B ∈ 𝔅 (𝔅'-admissibility of 𝒟 and k < |W t| ≤ |V t| by rerootBag_card_le); and W t misses that same B, since a vertex of W t ∩ B outside V t lies in X, making B a connected set meeting bag s and bag (home x) but not bag t, contradicting separates_of_mem_anc.

Gluing over the components

theorem Utilities.Treewidth.exists_admissible_of_closed {V : Type u} [DecidableEq V] {H : SimpleGraph V} (k : ℕ) (𝔅 : Bramble H) (X : Finset V) (hXk : X.card ≤ k) (hstep : ∀ (C : Finset V), IsComponent H X C → ∃ (D : PartialDecomposition H (C ∪ X)), Bramble.Admissible k 𝔅 D ∧ ∃ (r : D.Node), D.bag r = X) (n : ℕ) (R : Finset V) : R.card ≤ n → IsClosedAway H X R → ∃ (D : PartialDecomposition H (R ∪ X)), Bramble.Admissible k 𝔅 D ∧ ∃ (r : D.Node), D.bag r = X

Fold PartialDecomposition.join over a closed set of vertices, one component at a time.

Discharge plan: strong induction on R.card. R = ∅ is PartialDecomposition.single H X (Bramble.admissible_single). Otherwise pick v ∈ R, put C := compOf H X R v (a component by isComponent_compOf, inside R by compOf_subset), apply hstep to C and the induction hypothesis to R \ C (closed by isClosedAway_sdiff, smaller by card_sdiff_compOf_lt), and join them along X. hcap holds because C and R \ C are disjoint and both miss X; hsep holds because hC.closed forbids H-edges from C to R \ C.

The induction, and its consequence for the treewidth

theorem Utilities.Treewidth.exists_admissible {V : Type u} [Fintype V] [DecidableEq V] {H : SimpleGraph V} (k : ℕ) (hk : ∀ (𝔅 : Bramble H), 𝔅.order ≤ k) (𝔅 : Bramble H) : ∃ (D : PartialDecomposition H Finset.univ), Bramble.Admissible k 𝔅 D

Theorem 5, forward direction. If no bramble of H has order > k, then every bramble has an admissible decomposition.

Discharge plan: induction on n bounding Fintype.card (Finset V) − 𝔅.members.card. by_contra hno; take X a minimum cover of 𝔅 (Bramble.exists_isHittingSet_card_eq_order plus Bramble.order_le_card_of_isHittingSet), note X.card = 𝔅.order ≤ k by hk; feed component_step into exists_admissible_of_closed with R := Finset.univ \ X, and rewrite (Finset.univ \ X) ∪ X = Finset.univ.

theorem Utilities.Treewidth.treewidth_le_of_forall_order_le {V : Type u} [DecidableEq V] {H : SimpleGraph V} [Finite V] (k : ℕ) (hk : ∀ (𝔅 : Bramble H), 𝔅.order ≤ k) : treewidth H ≤ k - 1

Applying exists_admissible to the empty bramble bounds the treewidth.

Discharge plan: admissibility for Bramble.empty says no bag has more than k vertices (every set covers the empty bramble, Bramble.isHittingSet_empty), so width ≤ k − 1; then treewidth_le_width on toTreeDecomposition.

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

The hard half of Seymour--Thomas duality: some bramble has order at least treewidth H + 1.

Discharge plan: apply treewidth_le_of_forall_order_le with k := treewidth H. If every bramble had order ≤ treewidth H we would get treewidth H ≤ treewidth H − 1, impossible unless treewidth H = 0; and treewidth H = 0 is excluded because Bramble.singletonBramble H v has order ≥ 1 (this is where Nonempty V is used).