Reconstruction Conjecture — Edge Count

We prove that the number of edges is a reconstructible graph invariant: if two graphs on the same finite vertex set (≥ 3 vertices) have the same deck, they have the same number of edges.

Main results

• SimpleGraph.deleteVert_edgeFinset_card_add_degree — |E(G - v)| + deg(v) = |E(G)|
• SimpleGraph.degree_eq_card_edgeFinset_sub_deleteVert — deg(v) = |E(G)| - |E(G-v)|
• SimpleGraph.sum_card_edgeFinset_deleteVert_add — ∑ v, |E(G-v)| + 2|E(G)| = n · |E(G)|
• SimpleGraph.sum_card_edgeFinset_deleteVert — ∑ v, |E(G-v)| = (n - 2)|E(G)|
• SimpleGraph.SameDeck.card_edgeFinset_eq — same deck → same edge count

References

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

theorem SimpleGraph.deleteVert_edgeFinset_card_add_degree {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (v : V) : (G.deleteVert v).edgeFinset.card + G.degree v = G.edgeFinset.card

Deleting vertex v removes exactly deg(v) edges: |E(G - v)| + deg_G(v) = |E(G)|.

theorem SimpleGraph.degree_eq_card_edgeFinset_sub_deleteVert {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (v : V) : G.degree v = G.edgeFinset.card - (G.deleteVert v).edgeFinset.card

The degree of a deleted vertex is the difference between the original edge count and the edge count of its vertex-deleted card.

theorem SimpleGraph.sum_card_edgeFinset_deleteVert_add {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : ∑ v : V, (G.deleteVert v).edgeFinset.card + 2 * G.edgeFinset.card = Fintype.card V * G.edgeFinset.card

Summing the per-vertex edge count formula over all vertices: ∑ v, |E(G - v)| + 2|E(G)| = |V| · |E(G)|.

Equivalently, each edge appears in exactly |V| - 2 of the |V| cards.

theorem SimpleGraph.sum_card_edgeFinset_deleteVert {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hV : 2 ≤ Fintype.card V) : ∑ v : V, (G.deleteVert v).edgeFinset.card = (Fintype.card V - 2) * G.edgeFinset.card

The deck-sum edge count formula: ∑ v, |E(G-v)| = (|V| - 2) * |E(G)|.

Thus, for graphs with at least three vertices, the original edge count is recoverable from the multiset of vertex-deleted cards.

theorem SimpleGraph.SameDeck.card_edgeFinset_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.edgeFinset.card = H.edgeFinset.card

Edge count is reconstructible. If two graphs on ≥ 3 vertices have the same deck, they have the same number of edges.

This is a consequence of Kelly's counting lemma: each edge appears in exactly n - 2 of the n vertex-deleted subgraphs.