Reconstruction Conjecture — Chordal graphs are perfect (χ ≤ ω) #
Greedy colouring along a simplicial elimination: a finite chordal graph with no
(k+1)-clique is k-colourable. Combined with the trivial ω ≤ χ
(IsClique.card_le_of_colorable), this is the perfect-graph identity χ = ω for
chordal graphs (Berge / Hajnal–Surányi / Dirac).
Main result #
SimpleGraph.chordal_colorable— a finite chordalGwithG.CliqueFree (k+1)isG.Colorable k.
theorem
SimpleGraph.chordal_colorable_aux
{k : ℕ}
(n : ℕ)
(W : Type u)
[Fintype W]
(H : SimpleGraph W)
:
Fintype.card W ≤ n → H.IsChordal → H.CliqueFree (k + 1) → H.Colorable k
Inductive core: a finite chordal graph with no (k+1)-clique is
k-colourable. Strong induction on |V|, peeling a simplicial vertex v
(diracSimplicial): its neighbourhood is a clique of size < k, so after
colouring G − v it has a free colour.
theorem
SimpleGraph.chordal_colorable
{V : Type u_1}
{G : SimpleGraph V}
[Finite V]
{k : ℕ}
(hchord : G.IsChordal)
(hcf : G.CliqueFree (k + 1))
:
G.Colorable k
Chordal graphs are perfect (χ ≤ ω). A finite chordal graph with no
(k+1)-clique is k-colourable. With IsClique.card_le_of_colorable (the
trivial ω ≤ χ) this gives χ = ω for chordal graphs.