Reconstruction Conjecture — Connected Components

The number of connected components and the property of being connected are reconstructible graph invariants.

Main results

• SimpleGraph.SameDeck.connected — connectivity is reconstructible
• SimpleGraph.SameDeck.numComponents_eq — number of components is reconstructible

References

• Kelly, P. J. (1942). "On isometric transformations".

def SimpleGraph.numComponents {V : Type u_1} (G : SimpleGraph V) : ℕ

The number of connected components of a graph.

Equations

• G.numComponents = Nat.card G.ConnectedComponent

theorem SimpleGraph.numComponents_eq_fintype_card {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : G.numComponents = Fintype.card G.ConnectedComponent

theorem SimpleGraph.SameDeck.connected {V : Type u_1} [Fintype V] {G H : SimpleGraph V} (h : G.SameDeck H) (hV : 3 ≤ Fintype.card V) (hconn : G.Connected) : H.Connected

Connectivity is reconstructible. If G is connected and has the same deck as H (on ≥ 3 vertices), then H is connected.

The proof finds a non-cut vertex v in G (which exists in any connected graph on ≥ 2 vertices). The deck isomorphism gives G - v ≅ H - σ(v), so H - σ(v) is connected. Since every vertex of H has positive degree (degree sequence is reconstructible), σ(v) has a neighbor in H, and we can extend connectivity of H - σ(v) to all of H.

theorem SimpleGraph.SameDeck.numComponents_eq {V : Type u_1} [Fintype V] [DecidableEq V] {G H : SimpleGraph V} [DecidableRel G.Adj] [DecidableRel H.Adj] (h : G.SameDeck H) (hV : 3 ≤ Fintype.card V) : G.numComponents = H.numComponents

Number of connected components is reconstructible. If G and H on ≥ 3 vertices share the same deck, they have the same number of connected components.

Proof strategy (three-way case split):

1. If G is connected, then H is connected (by SameDeck.connected), so both have 1 component.
2. If G has an isolated vertex v, the deck iso G - v ≃g H - σ v gives (G-v).numComponents = (H - σ v).numComponents. Since degrees match under σ, σ v is isolated in H. Thus G.numComponents = (G-v).numComponents + 1 = (H - σ v).numComponents + 1 = H.numComponents.
3. Otherwise every vertex has positive degree in both graphs. Pick any vertex v; then G.numComponents ≤ (G-v).numComponents = (H - σ v).numComponents, and symmetrically for the reverse. So both are equal to (G-v).numComponents.