Tree decompositions and treewidth

Mathlib has no treewidth as of 2026-08-25, so this module introduces it from scratch, in the shape needed by the van Dobben de Bruyn--Gijswijt theorem treewidth ≤ gonality (TreewidthGonality/Gonality/TreewidthGonality.lean).

The connectivity convention (binds every downstream module)

Two conventions were available for "the vertex set S induces a connected subgraph of H": SimpleGraph.Subgraph connectivity, and the induced graph on the coercion of S to a Set. This library uses the induced-graph form throughout:

(H.induce (↑S : Set V)).Connected

for S : Finset V, and likewise for subsets of the tree's node type. Reasons:

• SimpleGraph.induce produces an honest SimpleGraph ↥s, so the whole SimpleGraph.Connected/Walk/Reachable API applies verbatim with no Subgraph.verts side conditions;
• SimpleGraph.Connected already bundles Nonempty, which is exactly the nonemptiness condition brambles need, so one field does two jobs;
• the coercion ↑S : Set V keeps the Finset bookkeeping (cardinalities, Finset.filter) available on the other side of the statement.

TreewidthGonality/Treewidth/Bramble.lean and TreewidthGonality/Gonality/BrambleGonality.lean use the same form. Do not mix in Subgraph.Connected without converting.

Multigraph note

Treewidth is defined for a SimpleGraph. For a chip-firing multigraph G the intended instantiation is underlyingSimpleGraph G: parallel edges and loops do not change treewidth, so nothing is lost.

Contents

• TreeDecomposition H — a bundled tree decomposition: a finite tree together with bags satisfying vertex coverage, edge coverage, and coherence.
• TreeDecomposition.width, treewidth (an sInf over ℕ).
• trivialDecomposition — the one-bag decomposition, which makes the set of achievable widths nonempty; treewidth_le_card_sub_one.

structure Utilities.Treewidth.TreeDecomposition {V : Type u} (H : SimpleGraph V) : Type (max 1 u)

A tree decomposition of a simple graph H: a finite tree tree on a node type Node, together with a bag of vertices at each node, such that

• cover_vertex — every vertex lies in some bag;
• cover_edge — the two endpoints of every edge lie in a common bag;
• coherent — for each vertex v the set of nodes whose bag contains v induces a connected (in particular nonempty) subtree.

coherent implies cover_vertex (connectedness bundles nonemptiness), but both are kept: cover_vertex is the field callers actually use, and stating it separately keeps the definition readable.

• Node : Type

  The nodes of the decomposition tree.

• nodeFintype : Fintype self.Node
• nodeDecidableEq : DecidableEq self.Node
• tree : SimpleGraph self.Node

  The decomposition tree.

• isTree : self.tree.IsTree

  tree really is a tree: connected and acyclic.

• bag : self.Node → Finset V

  The bag of vertices sitting at each node.

• cover_vertex (v : V) : ∃ (t : self.Node), v ∈ self.bag t

  Every vertex appears in some bag.

• cover_edge (v w : V) : H.Adj v w → ∃ (t : self.Node), v ∈ self.bag t ∧ w ∈ self.bag t

  Every edge has both endpoints in a common bag.

• coherent (v : V) : (SimpleGraph.induce {t : self.Node | v ∈ self.bag t} self.tree).Connected

  The nodes containing a fixed vertex form a connected subtree.

def Utilities.Treewidth.TreeDecomposition.width {V : Type u} {H : SimpleGraph V} (D : TreeDecomposition H) : ℕ

The width of a tree decomposition: one less than the largest bag size. The subtraction is truncated ℕ subtraction, which is harmless: sup (card - 1) and sup card - 1 agree in every case, including the degenerate all-bags-empty one.

Equations

• D.width = (Finset.univ.sup fun (t : D.Node) => (D.bag t).card) - 1

theorem Utilities.Treewidth.TreeDecomposition.card_bag_le_width_succ {V : Type u} {H : SimpleGraph V} (D : TreeDecomposition H) (t : D.Node) : (D.bag t).card ≤ D.width + 1

Every bag has at most width + 1 vertices.

theorem Utilities.Treewidth.TreeDecomposition.card_bag_le_card {V : Type u} {H : SimpleGraph V} [Fintype V] (D : TreeDecomposition H) (t : D.Node) : (D.bag t).card ≤ Fintype.card V

Every bag has at most Fintype.card V vertices.

def Utilities.Treewidth.widthSet {V : Type u} (H : SimpleGraph V) : Set ℕ

The set of widths realized by some tree decomposition of H.

Equations

• Utilities.Treewidth.widthSet H = {w : ℕ | ∃ (D : Utilities.Treewidth.TreeDecomposition H), D.width = w}

noncomputable def Utilities.Treewidth.treewidth {V : Type u} (H : SimpleGraph V) : ℕ

The treewidth of H: the least width of a tree decomposition.

This is an sInf over ℕ, which is total; widthSet_nonempty (via trivialDecomposition) is what makes the value meaningful rather than the sInf ∅ = 0 default.

Equations

• Utilities.Treewidth.treewidth H = sInf (Utilities.Treewidth.widthSet H)

def Utilities.Treewidth.trivialDecomposition {V : Type u} [Fintype V] (H : SimpleGraph V) : TreeDecomposition H

The trivial tree decomposition: a single node whose bag is all of V.

Equations

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

theorem Utilities.Treewidth.widthSet_nonempty {V : Type u} [Finite V] (H : SimpleGraph V) : (widthSet H).Nonempty

Some tree decomposition exists, so treewidth is an infimum over a nonempty set of naturals.

theorem Utilities.Treewidth.treewidth_le_width {V : Type u} {H : SimpleGraph V} (D : TreeDecomposition H) : treewidth H ≤ D.width

Any tree decomposition bounds the treewidth.

theorem Utilities.Treewidth.exists_treeDecomposition_width_eq_treewidth {V : Type u} [Finite V] (H : SimpleGraph V) : ∃ (D : TreeDecomposition H), D.width = treewidth H

The treewidth is realized by an actual decomposition.

theorem Utilities.Treewidth.treewidth_le_card_sub_one {V : Type u} [Fintype V] (H : SimpleGraph V) : treewidth H ≤ Fintype.card V - 1

treewidth H ≤ |V| - 1, from the one-bag decomposition.