Reconstruction Conjecture — Multi-vertex Separator Reassembly

This module generalizes the cut-vertex reassembly constructor (Reconstruction.Separator.isoOfDeleteVertIso / nonempty_iso_of_cutVertex_pieces, the S = {v} case) to an arbitrary separator set S. It is the structural core of the higher rungs of the separator-decomposition programme: it is exactly the reassembly half of Heinrich et al.'s "Reconstruction-by-Separation" (Lemma 24) for interval graphs, and the same statement is what chordal-graph reconstruction would consume once a clique separator is located.

Main definitions

• SimpleGraph.extendFixingSet S ψ — extend a permutation ψ of the non-separator vertices Sᶜ to a permutation of all of V that fixes S pointwise.

Main results

• SimpleGraph.nonempty_iso_of_induce_compl_iso — a card isomorphism ψ : G − S ≃g H − S (an isomorphism of the separator-deleted graphs) that preserves the separator's internal edges (hSadj) and the attachment of S to Sᶜ (hattach) extends to a global isomorphism G ≃g H. The structural generalization of isoOfDeleteVertIso from |S| = 1 to arbitrary S.
• SimpleGraph.nonempty_iso_of_separator_pieces — the same conclusion from per-component data: a bijection of (G − S)-components, per-component isomorphisms, the separator-edge match, and the attachment match. The card isomorphism is assembled with componentIso. This is the multi-vertex generalization of nonempty_iso_of_cutVertex_pieces.

In both, S is shared between G and H and the assembled isomorphism fixes S pointwise (the natural "common separator" form, mirroring the cut-vertex case where the deleted vertex is shared). The remaining work for any concrete class is the deck-theoretic recovery of the separator, the component matching, and the attachment data — none of which lives here.

References

• Heinrich, Kiyomi, Otachi, Schweitzer (2025). "Interval graphs are reconstructible." arXiv:2504.02353 (Reconstruction-by-Separation, Lemma 24).

def SimpleGraph.extendFixingSet {V : Type u_1} (S : Set V) [DecidablePred fun (x : V) => x ∈ S] (ψ : ↑Sᶜ ≃ ↑Sᶜ) : V ≃ V

Extend a permutation ψ of the non-separator vertices Sᶜ to a permutation of all of V that fixes every vertex of S.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SimpleGraph.extendFixingSet_apply_mem {V : Type u_1} {S : Set V} [DecidablePred fun (x : V) => x ∈ S] (ψ : ↑Sᶜ ≃ ↑Sᶜ) {x : V} (h : x ∈ S) : (extendFixingSet S ψ) x = x

theorem SimpleGraph.extendFixingSet_apply_not_mem {V : Type u_1} {S : Set V} [DecidablePred fun (x : V) => x ∈ S] (ψ : ↑Sᶜ ≃ ↑Sᶜ) {x : V} (h : x ∉ S) : (extendFixingSet S ψ) x = ↑(ψ ⟨x, h⟩)

theorem SimpleGraph.nonempty_iso_of_induce_compl_iso {V : Type u_1} {G H : SimpleGraph V} {S : Set V} (ψ : induce Sᶜ G ≃g induce Sᶜ H) (hSadj : ∀ (u w : V), u ∈ S → w ∈ S → (G.Adj u w ↔ H.Adj u w)) (hattach : ∀ u ∈ S, ∀ (x : ↑Sᶜ), G.Adj u ↑x ↔ H.Adj u ↑(ψ x)) : Nonempty (G ≃g H)

Multi-vertex separator reassembly (card-isomorphism form). A graph isomorphism ψ : G − S ≃g H − S of the separator-deleted graphs that

• preserves the separator's internal edges (hSadj), and
• preserves the attachment of each separator vertex to Sᶜ (hattach),

extends to a global isomorphism G ≃g H fixing S pointwise. The within-Sᶜ adjacency is handled automatically because ψ is a card isomorphism (any two non-separator vertices are adjacent in G iff adjacent in G − S).

theorem SimpleGraph.nonempty_iso_of_separator_pieces {V : Type u_1} {G H : SimpleGraph V} {S : Set V} (e : (induce Sᶜ G).ConnectedComponent ≃ (induce Sᶜ H).ConnectedComponent) (ι : (c : (induce Sᶜ G).ConnectedComponent) → induce c.supp (induce Sᶜ G) ≃g induce (e c).supp (induce Sᶜ H)) (hSadj : ∀ (u w : V), u ∈ S → w ∈ S → (G.Adj u w ↔ H.Adj u w)) (hattach : ∀ u ∈ S, ∀ (c : (induce Sᶜ G).ConnectedComponent) (x : ↑c.supp), G.Adj u ↑↑x ↔ H.Adj u ↑↑((ι c) x)) : Nonempty (G ≃g H)

Multi-vertex separator reassembly (per-component form). Given a bijection e of the components of G − S with those of H − S, per-component isomorphisms ι, a separator-edge match (hSadj), and an attachment match (hattach, phrased per component), the graphs G and H are isomorphic. The card isomorphism is assembled with componentIso; the conclusion is then nonempty_iso_of_induce_compl_iso.

This is the multi-vertex generalization of nonempty_iso_of_cutVertex_pieces and the structural core of Heinrich et al.'s Lemma 24.