Separation: Bellenbaum--Diestel's Lemma 1 and Lemma 4, and components

Three independent ingredients of the Seymour--Thomas induction:

• separates_of_mem_anc — Lemma 1 in the shape the proof uses: if t lies on the tree path from a node holding a to the distinguished node s, while no node holding b is below t, then every walk from a to b inside U meets bag t.
• Bramble.isHittingSet_of_separates — Lemma 4: a set separating two covers of a bramble covers it. (One line on paper; the Lean proof has to produce the walk inside a member.)
• awayGraph, compOf, IsComponent — the components of H − X, kept on the ambient vertex type V so that no subtype coercion enters the recursion. There is deliberately no "finset of all components": the gluing induction of SeymourThomasInduction.lean peels one component off a closed set at a time.

Lemma 1

theorem Utilities.Treewidth.separates_of_mem_anc {V : Type u} {H : SimpleGraph V} {U : Finset V} (D : PartialDecomposition H U) (s t : D.Node) {a b : V} (ha : a ∈ U) (_hb : b ∈ U) {na nb : D.Node} (hna : a ∈ D.bag na) (hnb : b ∈ D.bag nb) (h1 : t ∈ Anc ⋯ s na) (h2 : t ∉ Anc ⋯ s nb) (p : H.Walk a b) (hp : ∀ x ∈ p.support, x ∈ U) : ∃ x ∈ p.support, x ∈ D.bag t

Bellenbaum--Diestel Lemma 1, in the only shape the duality proof uses.

na is a node holding a and lying below t (that is, t is on the tree path from na to s); nb is a node holding b and not below t. Then bag t separates a from b inside U.

Note that no t ≠ s hypothesis is needed: s ∈ Anc hT s nb always, so h2 already forces t ≠ s.

Discharge plan (the σ-colouring argument of the blueprint §3.4). For u ∈ U with u ∉ bag t, D.coherent makes S u := {n | u ∈ bag n} connected and it misses t, so subset_below_or_disjoint puts it wholly inside Below or wholly outside. Along an H-edge inside U, D.cover_edge supplies a node in both S u and S u', so the side is the same at both ends; induct along the walk. The two endpoints have opposite sides by h1/h2.

Lemma 4

theorem Utilities.Treewidth.Bramble.isHittingSet_of_separates {V : Type u} {H : SimpleGraph V} [DecidableEq V] (𝔅 : Bramble H) {A B S : Finset V} (hA : 𝔅.IsHittingSet A) (hB : 𝔅.IsHittingSet B) (hsep : ∀ a ∈ A, ∀ b ∈ B, ∀ (p : H.Walk a b), ∃ x ∈ p.support, x ∈ S) : 𝔅.IsHittingSet S

Bellenbaum--Diestel Lemma 4. Any set separating two covers of a bramble also covers that bramble.

"Separating" is spelled walk-wise, which is the form SeymourThomasInduction.lean produces and the form that avoids introducing a separator predicate.

Discharge plan: for M ∈ 𝔅.members, hA/hB give a ∈ M ∩ A and b ∈ M ∩ B; 𝔅.connected_mem M gives a walk between them in H.induce ↑M, which maps down to an H-walk with support inside M (SimpleGraph.Embedding.induce); hsep puts a vertex of S on it, and that vertex is in M.

Components of H − X

def Utilities.Treewidth.awayGraph {V : Type u} (H : SimpleGraph V) (X : Finset V) : SimpleGraph V

H with every vertex of X isolated. Its connected components on V \ X are the components of H − X, but the construction never leaves the type V.

Equations

• Utilities.Treewidth.awayGraph H X = { Adj := fun (a b : V) => H.Adj a b ∧ a ∉ X ∧ b ∉ X, symm := ⋯, loopless := ⋯ }

theorem Utilities.Treewidth.awayGraph_le {V : Type u} (H : SimpleGraph V) (X : Finset V) : awayGraph H X ≤ H

structure Utilities.Treewidth.IsComponent {V : Type u} (H : SimpleGraph V) (X C : Finset V) : Prop

C is a connected component of H − X: nonempty, disjoint from X, inducing a connected subgraph of H, and closed under taking H-neighbours outside X.

• notMem (v : V) : v ∈ C → v ∉ X

  No vertex of C lies in X.

• nonempty : C.Nonempty

  C is nonempty.

• connected : (SimpleGraph.induce (↑C) H).Connected

  C induces a connected subgraph of H.

• closed (a : V) : a ∈ C → ∀ (b : V), H.Adj a b → b ∉ X → b ∈ C

  Every H-neighbour of a vertex of C lies in C or in X; that is, N(C) ⊆ X.

noncomputable def Utilities.Treewidth.compOf {V : Type u} (H : SimpleGraph V) (X R : Finset V) (v : V) : Finset V

The component of v inside a set R. R is intended to be closed under awayGraph H X-adjacency, in which case the filter by R is vacuous and this is the full component of v.

Equations

• Utilities.Treewidth.compOf H X R v = {w ∈ R | (Utilities.Treewidth.awayGraph H X).Reachable v w}

theorem Utilities.Treewidth.mem_compOf_iff {V : Type u} (H : SimpleGraph V) (X R : Finset V) (v w : V) : w ∈ compOf H X R v ↔ w ∈ R ∧ (awayGraph H X).Reachable v w

theorem Utilities.Treewidth.compOf_subset {V : Type u} (H : SimpleGraph V) (X R : Finset V) (v : V) : compOf H X R v ⊆ R

theorem Utilities.Treewidth.mem_compOf_self {V : Type u} {H : SimpleGraph V} {X R : Finset V} {v : V} (hv : v ∈ R) : v ∈ compOf H X R v

def Utilities.Treewidth.IsClosedAway {V : Type u} (H : SimpleGraph V) (X R : Finset V) : Prop

A set of vertices outside X closed under awayGraph-adjacency.

Equations

• Utilities.Treewidth.IsClosedAway H X R = ((∀ v ∈ R, v ∉ X) ∧ ∀ a ∈ R, ∀ (b : V), (Utilities.Treewidth.awayGraph H X).Adj a b → b ∈ R)

theorem Utilities.Treewidth.isComponent_compOf {V : Type u} {H : SimpleGraph V} {X R : Finset V} (hR : IsClosedAway H X R) {v : V} (hv : v ∈ R) : IsComponent H X (compOf H X R v)

Inside a closed set, compOf really is a component.

Discharge plan: notMem from IsClosedAway.1 and compOf_subset; nonempty from mem_compOf_self; closed because an H-edge out of C to a vertex outside X is an awayGraph edge, so the target is reachable and (by closure of R) in R; connected by transporting awayGraph-walks with SimpleGraph.Walk.mapLe (awayGraph_le H X) and then SimpleGraph.Walk.induce, the support staying inside C because reachability is transitive.

theorem Utilities.Treewidth.isClosedAway_sdiff {V : Type u} [DecidableEq V] {H : SimpleGraph V} {X R : Finset V} (hR : IsClosedAway H X R) (v : V) : IsClosedAway H X (R \ compOf H X R v)

Removing a component from a closed set leaves a closed set.

theorem Utilities.Treewidth.card_sdiff_compOf_lt {V : Type u} [DecidableEq V] {H : SimpleGraph V} {X R : Finset V} {v : V} (hv : v ∈ R) : (R \ compOf H X R v).card < R.card

A component is nonempty, so removing it strictly shrinks the set.