Reconstruction Conjecture — Perfect elimination orderings

A perfect elimination ordering (PEO) of G lists the vertices so that for every vertex v, the neighbours of v appearing later in the list form a clique. Dirac's theorem (diracSimplicial) gives the main direction of the classical characterization: every finite chordal graph has a PEO, obtained by repeatedly peeling off a simplicial vertex.

Main results

• SimpleGraph.IsPEO / SimpleGraph.HasPEO — the definition.
• SimpleGraph.isClique_neighbors_of_isSimplicial_induce — a vertex simplicial in G[s] has its s-neighbourhood a clique in G.
• SimpleGraph.hasPEO_of_chordal — every finite chordal graph has a PEO.

def SimpleGraph.IsPEO {V : Type u_1} (G : SimpleGraph V) (l : List V) : Prop

l is a perfect elimination ordering of G: it lists every vertex once, and for each suffix v :: rest, the later neighbours of v (those in rest) form a clique.

Equations

• G.IsPEO l = (l.Nodup ∧ (∀ (v : V), v ∈ l) ∧ ∀ (v : V) (rest : List V), v :: rest <:+ l → G.IsClique {w : V | w ∈ rest ∧ G.Adj v w})

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

G has a perfect elimination ordering.

Equations

• G.HasPEO = ∃ (l : List V), G.IsPEO l

theorem SimpleGraph.isClique_neighbors_of_isSimplicial_induce {V : Type u_1} {G : SimpleGraph V} {s : Set V} {v : V} (hv : v ∈ s) (h : (induce s G).IsSimplicial ⟨v, hv⟩) : G.IsClique {w : V | w ∈ s ∧ G.Adj v w}

A vertex simplicial in the induced subgraph G[s] has its s-neighbourhood a clique in G (induced adjacency is G-adjacency).

theorem SimpleGraph.peo_aux {V : Type u_1} {G : SimpleGraph V} (hchord : G.IsChordal) (n : ℕ) (s : Finset V) : s.card ≤ n → ∃ (l : List V), l.Nodup ∧ (∀ (x : V), x ∈ l ↔ x ∈ s) ∧ ∀ (v : V) (rest : List V), v :: rest <:+ l → G.IsClique {w : V | w ∈ rest ∧ G.Adj v w}

The inductive core: on any Finset s of vertices, peeling off simplicial vertices (Dirac) yields a list enumerating s whose every suffix v :: rest has v's later neighbours forming a clique.

theorem SimpleGraph.hasPEO_of_chordal {V : Type u_1} {G : SimpleGraph V} [Finite V] (hchord : G.IsChordal) : G.HasPEO

Every finite chordal graph has a perfect elimination ordering. The main direction of the Dirac/Fulkerson–Gross characterization of chordal graphs.

The converse: a perfect elimination ordering implies chordality

theorem SimpleGraph.exists_earliest_suffix {V : Type u_1} (l : List V) : l.Nodup → ∀ (S : Set V), S.Nonempty → (∀ a ∈ S, a ∈ l) → ∃ (v : V) (rest : List V), v ∈ S ∧ v :: rest <:+ l ∧ ∀ a ∈ S, a ≠ v → a ∈ rest

In a Nodup list l, a nonempty set S of its elements has an earliest member v: the suffix v :: rest of l starting at v contains every other element of S.

theorem SimpleGraph.cycleGraph_adj_succ {n : ℕ} [NeZero n] (hn : 2 ≤ n) (i : Fin n) : (cycleGraph n).Adj i (i + 1)

In cycleGraph n (n ≥ 2), each vertex is adjacent to its successor.

theorem SimpleGraph.cycleGraph_adj_pred {n : ℕ} [NeZero n] (hn : 2 ≤ n) (i : Fin n) : (cycleGraph n).Adj i (i - 1)

In cycleGraph n (n ≥ 2), each vertex is adjacent to its predecessor.

theorem SimpleGraph.cycleGraph_not_adj_pred_succ {n : ℕ} [NeZero n] (hn : 4 ≤ n) (i : Fin n) : ¬(cycleGraph n).Adj (i - 1) (i + 1)

In cycleGraph n (n ≥ 4), the two neighbours i - 1 and i + 1 of a vertex are non-adjacent — the chordless property of a cycle of length ≥ 4.

theorem SimpleGraph.isChordal_of_hasPEO {V : Type u_1} {G : SimpleGraph V} (h : G.HasPEO) : G.IsChordal

The converse: a graph with a perfect elimination ordering is chordal. In an induced ≥ 4-cycle, the PEO-earliest vertex v has both its cycle neighbours later in the order, so the PEO forces them adjacent — contradicting the chordlessness of the cycle.

theorem SimpleGraph.isChordal_iff_hasPEO {V : Type u_1} {G : SimpleGraph V} [Finite V] : G.IsChordal ↔ G.HasPEO

Chordal ⟺ has a perfect elimination ordering (Dirac/Fulkerson–Gross).