Paths to a fixed node of a tree

Bellenbaum--Diestel's Lemma 1 is stated for an edge t₁t₂ of the decomposition tree and the two components of T − t₁t₂. The Seymour--Thomas proof uses it only in one shape: a node t lying on the tree path from a home node t_x to a distinguished node s. This module supplies exactly that shape, and nothing else — in particular no edge deletion, no bridges, and no direct use of acyclicity.

The cut argument follows from

Anc s a ⊆ (support of any walk a ⟶ b) ∪ Anc s b,

which in turn is just uniqueness of paths in a tree applied to the concatenation (a ⟶ b) ++ (b ⟶ s).

Anc hT s n is the paper's n T s, the set of nodes on the tree path from n to s. The name is short for "ancestors": thinking of s as the root, it is the set of ancestors of n, and Below hT s t = {n | t ∈ Anc hT s n} is the subtree hanging below t.

noncomputable def Utilities.Treewidth.treePath {N : Type v} {T : SimpleGraph N} (hT : T.IsTree) (n s : N) : T.Walk n s

The unique path from n to s in a tree.

Equations

• Utilities.Treewidth.treePath hT n s = Exists.choose ⋯

theorem Utilities.Treewidth.treePath_isPath {N : Type v} {T : SimpleGraph N} (hT : T.IsTree) (n s : N) : (treePath hT n s).IsPath

theorem Utilities.Treewidth.eq_treePath {N : Type v} {T : SimpleGraph N} (hT : T.IsTree) {n s : N} (p : T.Walk n s) (hp : p.IsPath) : p = treePath hT n s

Any path from n to s in a tree is treePath.

def Utilities.Treewidth.Anc {N : Type v} {T : SimpleGraph N} (hT : T.IsTree) (s n : N) : Set N

The paper's n T s: the set of nodes on the tree path from n to s. With s thought of as a root, this is the set of ancestors of n.

Equations

• Utilities.Treewidth.Anc hT s n = {u : N | u ∈ (Utilities.Treewidth.treePath hT n s).support}

def Utilities.Treewidth.Below {N : Type v} {T : SimpleGraph N} (hT : T.IsTree) (s t : N) : Set N

With s thought of as a root, the subtree hanging below t.

Equations

• Utilities.Treewidth.Below hT s t = {n : N | t ∈ Utilities.Treewidth.Anc hT s n}

theorem Utilities.Treewidth.self_mem_anc {N : Type v} {T : SimpleGraph N} (hT : T.IsTree) (s n : N) : n ∈ Anc hT s n

theorem Utilities.Treewidth.root_mem_anc {N : Type v} {T : SimpleGraph N} (hT : T.IsTree) (s n : N) : s ∈ Anc hT s n

theorem Utilities.Treewidth.anc_root {N : Type v} {T : SimpleGraph N} (hT : T.IsTree) (s : N) : Anc hT s s = {s}

The path from the root to itself is trivial.

theorem Utilities.Treewidth.mem_below_iff {N : Type v} {T : SimpleGraph N} (hT : T.IsTree) (s t n : N) : n ∈ Below hT s t ↔ t ∈ Anc hT s n

Membership in Below is membership of the root's path set.

theorem Utilities.Treewidth.root_notMem_below {N : Type v} {T : SimpleGraph N} (hT : T.IsTree) {s t : N} (h : t ≠ s) : s ∉ Below hT s t

The root is below nothing but itself.

theorem Utilities.Treewidth.anc_connected {N : Type v} {T : SimpleGraph N} (hT : T.IsTree) (s n : N) : (SimpleGraph.induce (Anc hT s n) T).Connected

Anc hT s n is connected in the tree: it is the support of a walk.

theorem Utilities.Treewidth.anc_subset_of_walk {N : Type v} {T : SimpleGraph N} (hT : T.IsTree) (s : N) {a b : N} (p : T.Walk a b) : Anc hT s a ⊆ {x : N | x ∈ p.support} ∪ Anc hT s b

The cut inequality. The path from a to the root is contained in the union of (the support of) any walk from a to b with the path from b to the root.

Discharge plan: (p.append (treePath hT b s)).toPath is a path from a to s, hence equals treePath hT a s by eq_treePath; then Walk.support_toPath_subset_support and Walk.support_append.

theorem Utilities.Treewidth.mem_of_connected_cross {N : Type v} {T : SimpleGraph N} (hT : T.IsTree) {s t : N} {S : Set N} (hS : (SimpleGraph.induce S T).Connected) {a b : N} (ha : a ∈ S) (hb : b ∈ S) (hta : t ∈ Anc hT s a) (htb : t ∉ Anc hT s b) : t ∈ S

The cut lemma, in the only form the proof uses. A connected node set meeting both Below hT s t and its complement contains t.

This replaces Bellenbaum--Diestel's "let T₁ and T₂ be the components of T − t₁t₂" entirely.

Discharge plan: hS.preconnected gives a walk inside S from a to b; push it down to T along SimpleGraph.Embedding.induce; apply anc_subset_of_walk.

theorem Utilities.Treewidth.subset_below_or_disjoint {N : Type v} {T : SimpleGraph N} (hT : T.IsTree) {s t : N} {S : Set N} (hS : (SimpleGraph.induce S T).Connected) (ht : t ∉ S) : S ⊆ Below hT s t ∨ Disjoint S (Below hT s t)

The dichotomy actually consumed by the separation lemma: a connected set of nodes avoiding t lies entirely below t or entirely outside.