Reconstruction Conjecture — Dirac's theorem (corollaries of the clique-separator lemma)

The two structural corollaries of minimalSeparatorClique (a minimal separator of a chordal graph is a clique):

• SimpleGraph.diracCliqueSeparator — a finite chordal connected non-complete graph has a clique separator. Proof: a non-complete connected graph has a separator ({a,b}ᶜ for a non-adjacent pair a, b); a ⊆-minimal one exists (finite), and it is a clique by minimalSeparatorClique.
• SimpleGraph.diracSimplicial — a finite nonempty chordal graph has a simplicial vertex (Dirac 1961). Proof by strong induction on |V|, peeling off a component across a clique separator.

DiracCliqueSeparator V (the target Prop) is stated without finiteness; it is provable only for finite V (Dirac's theorem fails for infinite graphs), so the theorem carries a [Fintype V] instance.

theorem SimpleGraph.exists_minimal_separator {V : Type u_1} {G : SimpleGraph V} [Finite V] (hconn : G.Connected) (hne : G ≠ ⊤) : ∃ (S : Set V), G.IsSeparator S ∧ ∀ T ⊂ S, ¬G.IsSeparator T

A finite connected non-complete graph has an inclusion-minimal separator.

theorem SimpleGraph.diracCliqueSeparator {V : Type u_1} [Finite V] : DiracCliqueSeparator V

Dirac's clique-separator theorem. A finite chordal connected non-complete graph has a separator that induces a clique.

theorem SimpleGraph.isSimplicial_of_induce {V : Type u_1} {G : SimpleGraph V} {T : Set V} {v : V} (hv : v ∈ T) (hsub : G.neighborSet v ⊆ T) (h : (induce T G).IsSimplicial ⟨v, hv⟩) : G.IsSimplicial v

Simplicial-vertex transfer. If every G-neighbour of v lies in T and v is simplicial in the induced subgraph G[T], then v is simplicial in G. This is the bridge that turns a simplicial vertex found by induction on a smaller induced subgraph into a simplicial vertex of the whole graph.

theorem SimpleGraph.exists_simplicial_of_induce_disj {V : Type u_1} {G : SimpleGraph V} {T T' : Set V} (hT'T : T' ⊆ T) (hT'ne : T'.Nonempty) (hnbhd : ∀ v ∈ T', G.neighborSet v ⊆ T) (hclique : ∀ p ∈ T, ∀ q ∈ T, p ∉ T' → q ∉ T' → p ≠ q → G.Adj p q) (hdisj : induce T G = ⊤ ∨ ∃ (a : ↑T) (b : ↑T), a ≠ b ∧ ¬(induce T G).Adj a b ∧ (induce T G).IsSimplicial a ∧ (induce T G).IsSimplicial b) : ∃ v ∈ T', G.IsSimplicial v

Extracting a simplicial vertex from the induction hypothesis. Suppose G[T] is complete or has two non-adjacent simplicial vertices (the inductive dichotomy), T' ⊆ T is nonempty, every T'-vertex keeps its G-neighbours in T, and T \ T' is a clique. Then some vertex of T' is simplicial in G. (In the complete case any T'-vertex works; otherwise the two non-adjacent simplicial vertices cannot both avoid T', since T \ T' is a clique.)

theorem SimpleGraph.dirac_aux (n : ℕ) (W : Type u) [Fintype W] (H : SimpleGraph W) : Fintype.card W ≤ n → H.IsChordal → H = ⊤ ∨ ∃ (a : W) (b : W), a ≠ b ∧ ¬H.Adj a b ∧ H.IsSimplicial a ∧ H.IsSimplicial b

The strong inductive form of Dirac's theorem, on a card-bounded family of graphs (one universe, so the induced-subgraph recursion stays in type): a finite chordal graph is complete or has two non-adjacent simplicial vertices.

theorem SimpleGraph.diracSimplicial {V : Type u_1} [Fintype V] : DiracSimplicial V

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