Reconstruction Conjecture — Statement and Basic Properties

The Reconstruction Conjecture states that every simple graph on at least 3 vertices is determined up to isomorphism by its deck — the multiset of vertex-deleted subgraphs considered up to isomorphism.

Main results

• SimpleGraph.SameDeck.refl — SameDeck is reflexive
• SimpleGraph.SameDeck.symm — SameDeck is symmetric
• SimpleGraph.SameDeck.trans — SameDeck is transitive
• reconstruction_conjecture — the conjecture statement (open problem, sorry)

References

• Kelly, P. J. (1942). "On isometric transformations".
• Ulam, S. M. (1960). A Collection of Mathematical Problems.

theorem SimpleGraph.SameDeck.refl {V : Type u_1} (G : SimpleGraph V) : G.SameDeck G

SameDeck is reflexive: every graph has the same deck as itself.

theorem SimpleGraph.SameDeck.symm {V : Type u_1} {G H : SimpleGraph V} (h : G.SameDeck H) : H.SameDeck G

SameDeck is symmetric.

theorem SimpleGraph.SameDeck.trans {V : Type u_1} {G H K : SimpleGraph V} (h₁ : G.SameDeck H) (h₂ : H.SameDeck K) : G.SameDeck K

SameDeck is transitive.

Complementation

Reconstructibility is closed under complementation: G is reconstructible iff its complement Gᶜ is. This is a classical observation (Bondy's "reconstructor's manual") and a basic tool — it lets every positive result be dualized (e.g. universal-vertex ↔ isolated-vertex, dense ↔ sparse).

def SimpleGraph.Iso.compl {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (e : G ≃g H) : Gᶜ ≃g Hᶜ

An isomorphism of graphs induces an isomorphism of their complements (same vertex map, adjacency negated).

Equations

• e.compl = { toEquiv := e.toEquiv, map_rel_iff' := ⋯ }

theorem SimpleGraph.compl_deleteVert {V : Type u_1} (G : SimpleGraph V) (v : V) : Gᶜ.deleteVert v = (G.deleteVert v)ᶜ

Deleting a vertex commutes with complementation: Gᶜ - v = (G - v)ᶜ.

theorem SimpleGraph.SameDeck.compl {V : Type u_1} {G H : SimpleGraph V} (h : G.SameDeck H) : Gᶜ.SameDeck Hᶜ

The complement deck is reconstructible. If G and H have the same deck, so do their complements. Hence reconstructibility is closed under complementation.

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

The Reconstruction Conjecture (Kelly 1942, Ulam 1960).

Every simple graph on a finite vertex set with at least 3 vertices is determined up to isomorphism by its deck: if G and H have the same deck, then G ≅ H.

This is one of the foremost open problems in graph theory.