Reconstruction Conjecture — Separator Decomposition

This module begins the separator-decomposition programme (see research/attacks/separator-decomposition.md): reconstruct graphs class by class up a ladder of separator size, reusing the component-decomposition machinery already proved in Reconstruction.Disconnected.

The bottom rung — decomposition along the empty separator (connected components) — is the disconnected-graph theorem SimpleGraph.SameDeck.iso_of_not_connected. This file provides the next layer of vocabulary, missing entirely from Mathlib (v4.28.0): vertex separators, cut vertices, and 2-connectivity.

Main definitions

• SimpleGraph.IsSeparator G S — deleting the vertex set S from the connected graph G leaves a nonempty, disconnected remainder.
• SimpleGraph.IsCutVertex G v — v is an articulation point: IsSeparator G {v}.
• SimpleGraph.NoCutVertex, SimpleGraph.TwoConnected — connected with no cut vertex.
• SimpleGraph.MinDegreeTwo — every vertex has two distinct neighbours (no pendant vertex); stated without Fintype/degree so it is instance-free.

Isomorphism invariance (proved)

• SimpleGraph.IsSeparator.map, IsCutVertex.map, MinDegreeTwo.map, TwoConnected.map — all the programme's predicates are isomorphism invariants, via Iso.induceImage (an isomorphism restricts to the induced subgraphs on s ↦ e '' s). This is the first ingredient any reconstruction argument needs, since the deck only determines structure up to isomorphism.

The separator reassembly engine (proved)

• SimpleGraph.SamePiece — u, w lie in a common piece of G over S.
• SimpleGraph.adj_samePiece — every edge lies within a single piece (the separator structural lemma: no edges run between distinct G − S components).
• SimpleGraph.isoOfSamePiece / isoOfSamePiece' — the engine: a vertex bijection that preserves adjacency within pieces and matches G's pieces to H's pieces is a global isomorphism G ≃g H. This is the amalgamation-over- S analogue of isoOfComponentIsoEquiv (the S = ∅ case).
• SimpleGraph.mem_iff_of_fixOn — fixing S pointwise preserves S-membership (used when assembling the bijection from per-piece data).

Staged targets (stated as Prop, not proved)

• SimpleGraph.BondySeparableReconstructible — Bondy's 1969 theorem: a graph with a cut vertex and no pendant vertex is reconstructible.
• SimpleGraph.TwoConnectedReconstructible — the class to which Bondy–Yongzhi reduces the whole conjecture.

The next Lean task is the application of the engine: assemble the bijection φ for the cut-vertex case (S = {v}) from a bijection of G − v components and per-component isomorphisms fixing v, discharging isoOfSamePiece's two hypotheses. The remaining deck-theoretic content — recovering those pieces and their attachment to v from the deck — is the Bondy 1969 argument proper.

References

• Bondy, J. A. (1969). "On Ulam's conjecture for separable graphs".
• Yongzhi, H. (1988). "On the Reconstruction Conjecture" (reduction to 2-connected graphs).

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

S separates G: the graph is connected, its complement Sᶜ is nonempty, and the induced subgraph on Sᶜ is not connected. Equivalently, deleting the vertices of S leaves at least two nonempty pieces.

This is the general (multi-vertex) separator notion. The |S| = 1 case is a cut vertex; the S = ∅ case never holds for a connected G (the complement is all of V, whose induced graph is connected), which is exactly why the empty-separator rung is the connected vs disconnected dichotomy handled in Reconstruction.Disconnected.

Equations

• G.IsSeparator S = (G.Connected ∧ Sᶜ.Nonempty ∧ ¬(SimpleGraph.induce Sᶜ G).Connected)

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

v is a cut vertex (articulation point) of G: deleting it from the connected graph G disconnects the (nonempty) remainder. Defined as the singleton-separator case so that all separator lemmas specialize to it.

Equations

• G.IsCutVertex v = G.IsSeparator {v}

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

G has no cut vertex.

Equations

• G.NoCutVertex = ∀ (v : V), ¬G.IsCutVertex v

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

G is 2-connected: connected and free of cut vertices. (Some authors additionally require 3 ≤ |V|; we keep that side condition explicit at use sites, e.g. in the reconstruction targets which already assume 3 ≤ |V|.)

Equations

• G.TwoConnected = (G.Connected ∧ G.NoCutVertex)

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

G has minimum degree at least 2 (no pendant or isolated vertex): every vertex has two distinct neighbours. Stated combinatorially so it needs no Fintype/DecidableRel instances.

Equations

• G.MinDegreeTwo = ∀ (v : V), ∃ (a : V) (b : V), a ≠ b ∧ G.Adj v a ∧ G.Adj v b

Basic projections

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

theorem SimpleGraph.IsSeparator.compl_nonempty {V : Type u_1} {G : SimpleGraph V} {S : Set V} (h : G.IsSeparator S) : Sᶜ.Nonempty

theorem SimpleGraph.IsSeparator.not_connected_induce_compl {V : Type u_1} {G : SimpleGraph V} {S : Set V} (h : G.IsSeparator S) : ¬(induce Sᶜ G).Connected

theorem SimpleGraph.IsCutVertex.connected {V : Type u_1} {G : SimpleGraph V} {v : V} (h : G.IsCutVertex v) : G.Connected

theorem SimpleGraph.IsCutVertex.exists_ne {V : Type u_1} {G : SimpleGraph V} {v : V} (h : G.IsCutVertex v) : ∃ (w : V), w ≠ v

theorem SimpleGraph.TwoConnected.connected {V : Type u_1} {G : SimpleGraph V} (h : G.TwoConnected) : G.Connected

theorem SimpleGraph.TwoConnected.noCutVertex {V : Type u_1} {G : SimpleGraph V} (h : G.TwoConnected) : G.NoCutVertex

Separators are isomorphism invariants

The deck determines a graph only up to isomorphism, so every reconstruction argument needs its structural predicates to be isomorphism invariants. We prove this for separators (hence for cut vertices and 2-connectivity) by restricting an isomorphism to the relevant induced subgraphs.

noncomputable def SimpleGraph.Iso.induceImage {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (e : G ≃g H) (s : Set V) : induce s G ≃g induce (⇑e '' s) H

An isomorphism e : G ≃g H restricts to an isomorphism between the subgraph induced on a set s and the subgraph induced on its image e '' s. This is the Set-based companion of KellyLemma.induceMapIso (which is Finset-based).

Equations

• e.induceImage s = { toEquiv := Equiv.Set.image (⇑e) s ⋯, map_rel_iff' := ⋯ }

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

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

Cut vertices are isomorphism invariants.

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

Minimum-degree-≥-2 is an isomorphism invariant.

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

2-connectivity is an isomorphism invariant; this makes TwoConnectedReconstructible a well-posed (isomorphism-stable) target.

The separator reassembly engine

This is the structural core of the programme: the generalization of isoOfComponentIsoEquiv (the S = ∅, disjoint-union case) to amalgamation over a shared separator S.

The key structural fact about a separator is that every edge of G lies inside a single "piece" — a pair of endpoints is either incident to S, or both endpoints avoid S and then (since deleting S cannot create edges) they lie in the same connected component of G − S. There are no edges between distinct (G − S)-components. Consequently a vertex bijection that preserves adjacency within each piece, and that matches G's pieces to H's pieces (so that cross-component non-edges map to cross-component non-edges), is already a global isomorphism.

def SimpleGraph.SamePiece {V : Type u_1} (G : SimpleGraph V) (S : Set V) (u w : V) : Prop

u and w lie in a common piece of G relative to S: at least one of them is in S, or both avoid S and lie in the same connected component of the separator-deleted graph G.induce Sᶜ. Every edge lies within a piece (adj_samePiece), and within a piece adjacency is "local".

Equations

• G.SamePiece S u w = (u ∈ S ∨ w ∈ S ∨ ∃ (hu : u ∉ S) (hw : w ∉ S), (SimpleGraph.induce Sᶜ G).connectedComponentMk ⟨u, hu⟩ = (SimpleGraph.induce Sᶜ G).connectedComponentMk ⟨w, hw⟩)

theorem SimpleGraph.adj_connectedComponentMk_eq {V : Type u_1} {G : SimpleGraph V} {S : Set V} {u w : V} (h : G.Adj u w) (hu : u ∉ S) (hw : w ∉ S) : (induce Sᶜ G).connectedComponentMk ⟨u, hu⟩ = (induce Sᶜ G).connectedComponentMk ⟨w, hw⟩

Adjacent vertices avoiding S lie in the same component of G − S: deleting a vertex set cannot turn a non-edge into an edge, so an edge between two complement vertices is already an edge of G.induce Sᶜ.

theorem SimpleGraph.adj_samePiece {V : Type u_1} {G : SimpleGraph V} {S : Set V} {u w : V} (h : G.Adj u w) : G.SamePiece S u w

Every edge lies within a single piece. This is the separator structural lemma in the form the reassembly engine consumes.

def SimpleGraph.isoOfSamePiece {V : Type u_1} {G H : SimpleGraph V} {S : Set V} (φ : V ≃ V) (hpiece : ∀ (u w : V), G.SamePiece S u w → (G.Adj u w ↔ H.Adj (φ u) (φ w))) (hreflect : ∀ (u w : V), H.SamePiece S (φ u) (φ w) → G.SamePiece S u w) : G ≃g H

Separator reassembly engine. A vertex bijection φ that (i) preserves adjacency on every pair lying in a common piece of G, and (ii) reflects H-pieces back to G-pieces, is a graph isomorphism G ≃g H.

This is the amalgamation-over-S analogue of isoOfComponentIsoEquiv: in the S = ∅ case a piece is just a connected component, hypothesis (i) is "componentwise isomorphism", and (ii) holds because φ matches components. In applications φ is assembled from a component bijection together with per-piece isomorphisms that agree on S; this lemma is the structural step that turns that local data into a global isomorphism.

Equations

• SimpleGraph.isoOfSamePiece φ hpiece hreflect = { toEquiv := φ, map_rel_iff' := ⋯ }

def SimpleGraph.isoOfSamePiece' {V : Type u_1} {G H : SimpleGraph V} {S : Set V} (φ : V ≃ V) (hpres : ∀ (u w : V), G.SamePiece S u w ↔ H.SamePiece S (φ u) (φ w)) (hadj : ∀ (u w : V), G.SamePiece S u w → (G.Adj u w ↔ H.Adj (φ u) (φ w))) : G ≃g H

Convenience form of the reassembly engine with a single symmetric piece-preservation hypothesis.

Equations

• SimpleGraph.isoOfSamePiece' φ hpres hadj = SimpleGraph.isoOfSamePiece φ hadj ⋯

theorem SimpleGraph.mem_iff_of_fixOn {V : Type u_1} {S : Set V} {φ : V ≃ V} (hfix : ∀ x ∈ S, φ x = x) (x : V) : x ∈ S ↔ φ x ∈ S

If a bijection fixes S pointwise it preserves membership in S in both directions. (When constructing the reassembly bijection from per-piece data, this discharges the "preserves the separator" obligation from the single assumption that the pieces agree on S.)

Rung 1: the deleted-vertex reassembly constructor

The reassembly engine specialized to a single deleted vertex (S = {v}). A card isomorphism ψ : G − v ≃g H − w that additionally matches the link of the deleted vertex (its neighbourhood) extends to a global isomorphism G ≃g H. This is the structural converse of vertex deletion: a graph is recovered from one card together with the deleted vertex's attachment. (For |S| = 1 the "no edge crosses a piece" content is subsumed by ψ being a card isomorphism: any pair of non-v vertices is adjacent in G iff adjacent in G − v.)

The deleted vertices v and w are allowed to differ, since a deck matching matches v to some σ v. The remaining, deck-theoretic, work for Bondy's theorem is to produce such a ψ from deck data — assembled from per-component pieces that agree on the deleted vertex.

def SimpleGraph.extendMap {V : Type u_1} [DecidableEq V] (v w : V) (ψ : { x : V // x ≠ v } ≃ { x : V // x ≠ w }) : V ≃ V

Extend a bijection ψ from the vertices ≠ v to the vertices ≠ w to a bijection of all of V sending v to w.

Equations

• SimpleGraph.extendMap v w ψ = { toFun := fun (x : V) => if h : x = v then w else ↑(ψ ⟨x, h⟩), invFun := fun (y : V) => if h : y = w then v else ↑(ψ.symm ⟨y, h⟩), left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem SimpleGraph.extendMap_apply_self {V : Type u_1} [DecidableEq V] (v w : V) (ψ : { x : V // x ≠ v } ≃ { x : V // x ≠ w }) : (extendMap v w ψ) v = w

theorem SimpleGraph.extendMap_apply_of_ne {V : Type u_1} [DecidableEq V] (v w : V) (ψ : { x : V // x ≠ v } ≃ { x : V // x ≠ w }) {x : V} (h : x ≠ v) : (extendMap v w ψ) x = ↑(ψ ⟨x, h⟩)

def SimpleGraph.isoOfDeleteVertIso {V : Type u_1} [DecidableEq V] {G H : SimpleGraph V} {v w : V} (ψ : G.deleteVert v ≃g H.deleteVert w) (hlink : ∀ (x : { x : V // x ≠ v }), G.Adj v ↑x ↔ H.Adj w ↑(ψ x)) : G ≃g H

Deleted-vertex reassembly. A card isomorphism ψ : G − v ≃g H − w that preserves the link (for every x ≠ v, v is adjacent to x in G iff w is adjacent to ψ x in H) extends to a global isomorphism G ≃g H sending v to w. The deleted vertices v, w may differ — exactly what a deck matching provides, since it matches v to some σ v rather than to v itself.

Equations

• SimpleGraph.isoOfDeleteVertIso ψ hlink = { toEquiv := SimpleGraph.extendMap v w ψ.toEquiv, map_rel_iff' := ⋯ }

theorem SimpleGraph.nonempty_iso_of_cutVertex_pieces {V : Type u_1} {G H : SimpleGraph V} {v : V} (e : (G.deleteVert v).ConnectedComponent ≃ (H.deleteVert v).ConnectedComponent) (ι : (c : (G.deleteVert v).ConnectedComponent) → induce c.supp (G.deleteVert v) ≃g induce (e c).supp (H.deleteVert v)) (hlink : ∀ (c : (G.deleteVert v).ConnectedComponent) (x : ↑c.supp), G.Adj v ↑↑x ↔ H.Adj v ↑↑((ι c) x)) : Nonempty (G ≃g H)

Cut-vertex reassembly from pieces. Given a bijection e between the components of G − v and those of H − v, per-component isomorphisms ι of the corresponding induced subgraphs, and the condition that each piece isomorphism preserves adjacency to v (the link condition), the graphs G and H are isomorphic.

This is the complete structural content of Bondy's cut-vertex reconstruction: it reduces G ≅ H to a matching of the (G − v)-pieces that agrees on v's attachment. The remaining work is the deck-theoretic recovery of such a matching from SameDeck. The card isomorphism is assembled with componentIso (whose vertex action is componentIso_apply), and the global isomorphism is produced by isoOfDeleteVertIso.

Application: dominating-vertex reconstruction

A first genuine deck-level reconstruction theorem from the reassembly machinery: a graph with a universal vertex (one adjacent to every other vertex) is reconstructible. This is the simplest case of Manvel's dominating-vertex method. The link condition is automatic — a universal vertex is adjacent to everything — and degree-preservation forces the matched card's vertex to be universal too, so isoOfDeleteVertIso applies directly.

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

v is a universal vertex of G: adjacent to every other vertex.

Equations

• G.IsUniversal v = ∀ (x : V), x ≠ v → G.Adj v x

theorem SimpleGraph.isUniversal_iff_degree {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] (v : V) : G.IsUniversal v ↔ G.degree v = Fintype.card V - 1

A vertex is universal iff its degree is |V| - 1.

theorem SimpleGraph.nonempty_iso_of_universal_card_iso {V : Type u_1} {G H : SimpleGraph V} {v w : V} (hv : G.IsUniversal v) (hw : H.IsUniversal w) (ψ : G.deleteVert v ≃g H.deleteVert w) : Nonempty (G ≃g H)

Two universal vertices with isomorphic cards give isomorphic graphs: the link condition holds vacuously, since both vertices are adjacent to everything.

theorem SimpleGraph.nonempty_iso_of_universal_vertex {V : Type u_1} [Fintype V] {G H : SimpleGraph V} {v : V} (hv : G.IsUniversal v) (hV : 3 ≤ Fintype.card V) (h : G.SameDeck H) : Nonempty (G ≃g H)

Graphs with a universal vertex are reconstructible. If G has a vertex adjacent to all others and H has the same deck (on ≥ 3 vertices), then G ≅ H. The matched-card vertex σ v is forced to be universal in H because degrees are deck-reconstructible, so nonempty_iso_of_universal_card_iso applies. (Manvel's dominating-vertex method, simplest case.)

Staged targets

These are the reconstruction theorems the programme aims at, stated as Props (the project convention for open/under-construction goals; no sorry).

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

TARGET — Bondy 1969. A graph with a cut vertex and no pendant vertex is reconstructible: if G has a cut vertex, has minimum degree ≥ 2, and H has the same deck, then G ≅ H. Together with SameDeck.iso_of_not_connected and the pendant-vertex (tree) case, this yields the Bondy–Yongzhi reduction.

Equations

• G.BondySeparableReconstructible = ((∃ (v : V), G.IsCutVertex v) → G.MinDegreeTwo → ∀ (H : SimpleGraph V), G.SameDeck H → Nonempty (G ≃g H))

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

TARGET — the class Bondy–Yongzhi reduces to. Every 2-connected graph is reconstructible from its deck. By Bondy 1969 (separable case) + Kelly 1942 (disconnected case) + the tree case, the full Reconstruction Conjecture for n ≥ 3 follows from this restricted statement.

Equations

• G.TwoConnectedReconstructible = (G.TwoConnected → ∀ (H : SimpleGraph V), G.SameDeck H → Nonempty (G ≃g H))