Chordal graphs

A simple graph is chordal if every cycle of length at least four has a chord — an edge of the graph joining two vertices of the cycle that is not itself one of the cycle's edges.

This module is a reusable byproduct extracted from the verified formalization accompanying Paper II, Complete-Split Extremizers for a Fractional Triangle-Cover Functional on Chordal Graphs. It is self-contained and depends only on Mathlib.

Main definitions

• SimpleGraph.IsChordal
• SimpleGraph.IsSimplicial
• SimpleGraph.Separates, SimpleGraph.IsMinimalSeparator

Main results

• SimpleGraph.IsChordal.comap — chordality pulls back along an injective vertex map
• SimpleGraph.IsChordal.minimalSeparator_isClique — finite minimal separators of fixed vertex pairs are cliques
• SimpleGraph.IsChordal.exists_isSimplicial — Dirac (1961): a nonempty finite chordal graph has a simplicial vertex
• SimpleGraph.IsChordal.exists_two_nonadj_isSimplicial — a connected non-complete finite chordal graph has two non-adjacent simplicial vertices

def SimpleGraph.IsChordal {V : Type u_1} (G : SimpleGraph V) : Prop

A graph is chordal if every cycle of length ≥ 4 has a chord: an adjacency between two vertices of the cycle whose edge is not one of the cycle's own edges.

Equations

• G.IsChordal = ∀ ⦃v : V⦄ (c : G.Walk v v), c.IsCycle → 4 ≤ c.length → ∃ (x : V) (y : V), x ∈ c.support ∧ y ∈ c.support ∧ G.Adj x y ∧ s(x, y) ∉ c.edges

def SimpleGraph.IsSimplicial {V : Type u_1} (G : SimpleGraph V) (v : V) : Prop

A vertex is simplicial if its neighbourhood induces a clique.

Equations

• G.IsSimplicial v = G.IsClique (G.neighborSet v)

def SimpleGraph.Separates {V : Type u_1} (G : SimpleGraph V) (S : Set V) (a b : V) : Prop

S separates a from b if neither lies in S and every walk a → b meets S.

Equations

• G.Separates S a b = (a ∉ S ∧ b ∉ S ∧ ¬Relation.ReflTransGen (fun (p q : V) => p ∉ S ∧ q ∉ S ∧ G.Adj p q) a b)

def SimpleGraph.IsMinimalSeparator {V : Type u_1} (G : SimpleGraph V) (S : Set V) (a b : V) : Prop

S is a minimal a–b separator: it separates them and no proper subset does.

Equations

• G.IsMinimalSeparator S a b = (G.Separates S a b ∧ ∀ T ⊂ S, ¬G.Separates T a b)

theorem SimpleGraph.IsChordal.comap {V : Type u_1} {G : SimpleGraph V} {W : Type u_2} (hG : G.IsChordal) (f : W ↪ V) : (SimpleGraph.comap (⇑f) G).IsChordal

Chordality pulls back along an injective vertex map. In particular, every induced subgraph of a chordal graph is chordal.

theorem SimpleGraph.IsChordal.induce {V : Type u_1} {G : SimpleGraph V} (hG : G.IsChordal) (W : Set V) : (SimpleGraph.induce W G).IsChordal

Every induced subgraph of a chordal graph is chordal.

Private helpers (ported from a verified development; self-contained).

Dirac helpers (private)

Bridges between the Finset-based and Set-based separator notions.

theorem SimpleGraph.IsChordal.minimalSeparator_isClique {V : Type u_1} {G : SimpleGraph V} (hG : G.IsChordal) {S : Finset V} {a b : V} (hS : G.IsMinimalSeparator (↑S) a b) : G.IsClique ↑S

In a chordal graph, every finite minimal separator of two fixed vertices is a clique.

theorem SimpleGraph.IsChordal.exists_isSimplicial {V : Type u_1} {G : SimpleGraph V} [Finite V] [Nonempty V] (hG : G.IsChordal) : ∃ (v : V), G.IsSimplicial v

Dirac's theorem (1961). A nonempty finite chordal graph has a simplicial vertex.

theorem SimpleGraph.IsChordal.exists_two_nonadj_isSimplicial {V : Type u_1} {G : SimpleGraph V} [Finite V] (hG : G.IsChordal) (hconn : G.Connected) (hnc : ¬∀ (u v : V), u ≠ v → G.Adj u v) : ∃ (x : V) (y : V), x ≠ y ∧ ¬G.Adj x y ∧ G.IsSimplicial x ∧ G.IsSimplicial y

Connected case of Dirac's two-vertex conclusion. A connected non-complete finite chordal graph has two distinct non-adjacent simplicial vertices.