Reconstruction Conjecture — Minimal separators: neighbours in each component

The delicate separator-side lemma behind MinimalSeparatorClique: in an inclusion-minimal separator S, every vertex x ∈ S has a neighbour in every component of G − S. Proof: if x had no neighbour in the component of u₀, then S \ {x} would still separate u₀ from w₀ (a walk from u₀ in G − (S \ {x}) can never leave that component — its only escape would be x, which has no neighbour there), contradicting minimality.

Main result

• SimpleGraph.exists_adj_mem_component — from minimality and a separated pair u₀, w₀, every x ∈ S has a neighbour in u₀'s component of G − S.

theorem SimpleGraph.exists_adj_mem_component {V : Type u_1} {G : SimpleGraph V} {S : Set V} (hconn : G.Connected) (hmin : ∀ T ⊂ S, ¬G.IsSeparator T) {x u₀ w₀ : V} (hx : x ∈ S) (hu₀ : u₀ ∉ S) (hw₀ : w₀ ∉ S) (hsep : ¬(induce Sᶜ G).Reachable ⟨u₀, hu₀⟩ ⟨w₀, hw₀⟩) : ∃ (a : V) (ha : a ∉ S), (induce Sᶜ G).connectedComponentMk ⟨a, ha⟩ = (induce Sᶜ G).connectedComponentMk ⟨u₀, hu₀⟩ ∧ G.Adj x a

A minimal separator's vertices reach every component. If S is inclusion-minimal among separators and u₀, w₀ are separated by S, then any x ∈ S has a neighbour a in the same G − S component as u₀.