Cliques in arbitrary tree decompositions and exact chordal treewidth

Helly applies to vertex-occurrence subtrees in any tree decomposition. This gives the universal clique lower bound; the clique-forest adapter attains it for finite chordal graphs. The successor form excludes the empty vertex type.

theorem Utilities.Treewidth.TreeDecomposition.exists_clique_subset_bag {V : Type u_1} {G : SimpleGraph V} (D : TreeDecomposition G) {K : Finset V} (hK : G.IsClique ↑K) : ∃ (t : D.Node), K ⊆ D.bag t

Every finite clique is contained in one bag of any tree decomposition.

theorem Utilities.Treewidth.TreeDecomposition.cliqueNum_le_width_succ {V : Type u_1} {G : SimpleGraph V} [Finite V] (D : TreeDecomposition G) : G.cliqueNum ≤ D.width + 1

Clique number is a lower bound on the largest bag of every decomposition.

theorem Utilities.Treewidth.cliqueNum_le_treewidth_succ {V : Type u_1} [Finite V] (G : SimpleGraph V) : G.cliqueNum ≤ treewidth G + 1

Every finite graph has treewidth at least its clique number minus one.

theorem SimpleGraph.IsChordal.exists_optimal_treeDecomposition {V : Type} {G : SimpleGraph V} [Finite V] [Nonempty V] (hG : G.IsChordal) : ∃ (D : Utilities.Treewidth.TreeDecomposition G), D.width + 1 = G.cliqueNum

The clique decomposition of a finite nonempty chordal graph is optimal.

theorem SimpleGraph.IsChordal.treewidth_succ_eq_cliqueNum {V : Type} {G : SimpleGraph V} [Finite V] [Nonempty V] (hG : G.IsChordal) : Utilities.Treewidth.treewidth G + 1 = G.cliqueNum

Finite nonempty chordal graphs have treewidth exactly clique number minus one.