Reconstruction Conjecture — Clique Separators and Simplicial Vertices

This module adds the clique-separator vocabulary on top of the general separator theory in Reconstruction.Separator. Clique separators are the structural input for the higher rungs of the separator-decomposition programme: in a chordal graph every minimal vertex separator induces a clique (Dirac), and in the interval-graph reconstruction of Heinrich–Kiyomi–Otachi–Schweitzer (2025) the "clean clique separations" are exactly separations whose separator is a clique. Combined with the reassembly engine isoOfSamePiece, a clique separator is precisely the situation the engine reassembles.

Main definitions

• SimpleGraph.IsSimplicial G v — the neighbourhood of v is a clique.
• SimpleGraph.IsCliqueSeparator G S — S is a separator that induces a clique.

Main results

• SimpleGraph.IsSimplicial.map, SimpleGraph.IsCliqueSeparator.map — both are isomorphism invariants (clique structure transports across ≃g).
• SimpleGraph.IsCliqueSeparator.adj_of_mem — distinct separator vertices are adjacent. This is the extra ingredient (beyond isoOfSamePiece) needed to glue the two sides of a clean clique separation: within the separator, adjacency is forced, so a piece-matching that fixes the separator automatically matches the separator's internal edges.

References

• Dirac, G. A. (1961). "On rigid circuit graphs." (Minimal separators of chordal graphs are cliques.)
• Heinrich, Kiyomi, Otachi, Schweitzer (2025). "Interval graphs are reconstructible." arXiv:2504.02353. (Clean clique separations.)

theorem SimpleGraph.isClique_image_of_iso {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} {S : Set V} (e : G ≃g H) (h : G.IsClique S) : H.IsClique (⇑e '' S)

A graph isomorphism transports cliques: the image of a clique under e is a clique in the target graph. (Mathlib's IsClique.map is stated for pushforwards SimpleGraph.map f G; this is the cross-graph ≃g version.)

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

v is a simplicial vertex of G: its neighbourhood induces a clique. Simplicial vertices drive the perfect-elimination view of chordal graphs.

Equations

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

theorem SimpleGraph.IsSimplicial.map {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} {v : V} (e : G ≃g H) (h : G.IsSimplicial v) : H.IsSimplicial (e v)

Simplicial vertices are isomorphism invariants.

def SimpleGraph.IsCliqueSeparator {V : Type u_1} (G : SimpleGraph V) (S : Set V) : Prop

S is a clique separator of G: it separates G and induces a clique. This is the separation hypothesis of the reassembly engine specialized to the case that arises for chordal and interval graphs.

Equations

• G.IsCliqueSeparator S = (G.IsClique S ∧ G.IsSeparator S)

theorem SimpleGraph.IsCliqueSeparator.isClique {V : Type u_1} {G : SimpleGraph V} {S : Set V} (h : G.IsCliqueSeparator S) : G.IsClique S

theorem SimpleGraph.IsCliqueSeparator.isSeparator {V : Type u_1} {G : SimpleGraph V} {S : Set V} (h : G.IsCliqueSeparator S) : G.IsSeparator S

theorem SimpleGraph.IsCliqueSeparator.map {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} {S : Set V} (e : G ≃g H) (h : G.IsCliqueSeparator S) : H.IsCliqueSeparator (⇑e '' S)

Clique separators are isomorphism invariants (clique part via isClique_image_of_iso, separator part via IsSeparator.map).

theorem SimpleGraph.IsCliqueSeparator.adj_of_mem {V : Type u_1} {G : SimpleGraph V} {S : Set V} {u w : V} (h : G.IsCliqueSeparator S) (hu : u ∈ S) (hw : w ∈ S) (hne : u ≠ w) : G.Adj u w

Distinct vertices of a clique separator are adjacent. Within the separator, adjacency is forced; this is what lets a piece-matching that fixes the separator match the separator's internal edges for free, completing the clean-clique- separation gluing on top of isoOfSamePiece.