Reconstruction Conjecture — Minimal separators are cliques

The capstone of the chordal structure layer: in a chordal graph, an inclusion-minimal separator is a clique. The proof contradicts chordality by exhibiting an induced cycle of length ≥ 4: take two non-adjacent vertices x, y of the separator S; by minimality each has a neighbour in two distinct components A, B of G − S; the two shortest x–y paths confined to A ∪ {x,y} and B ∪ {x,y} are chordless arcs sharing only x, y, with no cross-edges, so they glue (inducedCycleEmbedding_of_paths) into an induced cycle — impossible in a chordal graph.

Main results

• SimpleGraph.exists_chordless_arc — a chordless x–y arc through a prescribed component (a geodesic in the induced subgraph on that component plus x, y).

theorem SimpleGraph.exists_chordless_arc {V : Type u_1} {G : SimpleGraph V} {S : Set V} {x y : V} (hxy : x ≠ y) (hnadj : ¬G.Adj x y) {u₀ : V} (hu₀ : u₀ ∉ S) (hax : ∃ (a : V) (ha : a ∉ S), (induce Sᶜ G).connectedComponentMk ⟨a, ha⟩ = (induce Sᶜ G).connectedComponentMk ⟨u₀, hu₀⟩ ∧ G.Adj x a) (hay : ∃ (a : V) (ha : a ∉ S), (induce Sᶜ G).connectedComponentMk ⟨a, ha⟩ = (induce Sᶜ G).connectedComponentMk ⟨u₀, hu₀⟩ ∧ G.Adj y a) : ∃ (P : G.Walk x y), P.IsPath ∧ 2 ≤ P.length ∧ (∀ (i j : ℕ), i + 1 < j → j ≤ P.length → ¬G.Adj (P.getVert i) (P.getVert j)) ∧ ∀ (i : ℕ), 0 < i → i < P.length → ∃ (h : P.getVert i ∉ S), (induce Sᶜ G).connectedComponentMk ⟨P.getVert i, h⟩ = (induce Sᶜ G).connectedComponentMk ⟨u₀, hu₀⟩

A chordless arc through a component. Given non-adjacent x ≠ y, a component of G − S represented by u₀ ∉ S, and neighbours of x and of y in that component, there is a chordless x–y path P of length ≥ 2 whose interior lies entirely in that component. It is a shortest path in the induced subgraph on the component together with x, y; being a geodesic makes it chordless (geodesic_not_adj_of_lt), and the induced subgraph confines its interior to the component.

theorem SimpleGraph.minimalSeparatorClique {V : Type u_1} : MinimalSeparatorClique V

Minimal separators are cliques (Dirac's lemma — the chordal-structure crux). In a chordal graph, an inclusion-minimal separator induces a clique: two non-adjacent separator vertices would, by minimality, have neighbours in two distinct components of G − S, and the two shortest paths confined to those components glue into an induced cycle of length ≥ 4, impossible in a chordal graph.