Reconstruction Conjecture — Degree Sequence

We prove that the degree sequence (as a multiset) is a reconstructible graph invariant: if two graphs on ≥ 3 vertices have the same deck, they have the same degree multiset.

Main results

• SimpleGraph.SameDeck.degree_eq — same deck → matching degrees through σ
• SimpleGraph.SameDeck.degreeMultiset_eq — same deck → equal degree multisets

References

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

def SimpleGraph.degreeMultiset {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] : Multiset ℕ

The degree multiset of a graph: the multiset of all vertex degrees.

Equations

• G.degreeMultiset = Multiset.map (fun (v : V) => G.degree v) Finset.univ.val

theorem SimpleGraph.degree_eq_of_card_edgeFinset_eq_of_deleteVert_iso {V : Type u_1} [Fintype V] [DecidableEq V] {G H : SimpleGraph V} [DecidableRel G.Adj] [DecidableRel H.Adj] (he : G.edgeFinset.card = H.edgeFinset.card) {v w : V} (iso : G.deleteVert v ≃g H.deleteVert w) : G.degree v = H.degree w

If two graphs have equal edge counts and isomorphic vertex-deleted subgraphs at vertices v and w, then deg(v) = deg(w).

theorem SimpleGraph.SameDeck.degree_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) : ∃ (σ : V ≃ V), ∀ (v : V), G.degree v = H.degree (σ v)

Degrees are reconstructible. If two graphs on ≥ 3 vertices have the same deck via bijection σ, then deg_G(v) = deg_H(σ v) for all v.

theorem SimpleGraph.SameDeck.degreeMultiset_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.degreeMultiset = H.degreeMultiset

Degree multiset is reconstructible. If two graphs on ≥ 3 vertices have the same deck, their degree multisets are equal.