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.

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.