Reconstruction Conjecture — Trees

Being a tree is a reconstructible graph property: if G is a tree and has the same deck as H (on ≥ 3 vertices), then H is also a tree.

Main results

• SimpleGraph.SameDeck.isTree — tree property is reconstructible

Proof outline

1. Trees have |E| = |V| - 1 edges (IsTree.card_edgeFinset).
2. Edge count is reconstructible (SameDeck.card_edgeFinset_eq), so |E(H)| = |V| - 1.
3. Trees are connected; connectivity is reconstructible (SameDeck.connected).
4. A connected graph with |V| - 1 edges is a tree (isTree_iff_connected_and_card).

References

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

theorem SimpleGraph.SameDeck.isTree {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) (htree : G.IsTree) : H.IsTree

The tree property is reconstructible. If G is a tree and has the same deck as H (on ≥ 3 vertices), then H is also a tree.

The proof combines three reconstructible invariants:

• Edge count: |E(G)| = |E(H)|, and trees have |E| + 1 = |V|
• Connectivity: trees are connected, and connectivity is reconstructible
• Characterization: a connected graph with |V| - 1 edges is a tree