Reconstruction Conjecture — Regular Graphs #
Regular graphs are a reconstructible graph class: if G is d-regular and
has the same deck as H (on ≥ 3 vertices), then H is also d-regular.
Main results #
SimpleGraph.SameDeck.isRegularOfDegree— regularity is reconstructible
References #
- Kelly, P. J. (1942). "On isometric transformations".
theorem
SimpleGraph.SameDeck.isRegularOfDegree
{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)
{d : ℕ}
(hreg : G.IsRegularOfDegree d)
:
Regular graphs are reconstructible. If G is d-regular and has the same
deck as H (on ≥ 3 vertices), then H is also d-regular.
The degree multiset of a d-regular graph consists entirely of d's. Since the
degree multiset is reconstructible (SameDeck.degreeMultiset_eq), H has the same
degree multiset, hence is also d-regular.