Regular Graphs are Reconstructible — Deficit Marking

Regular graphs are reconstructible (folklore, Kelly-era): if G is d-regular, then in any card G - v the neighbours of the deleted vertex are exactly the vertices of card-degree ≠ d (they lost one edge; everyone else still has degree d). The deleted vertex's attachment is therefore visible in the unlabeled card, and the card isomorphism supplied by SameDeck automatically preserves it, so isoOfDeleteVertIso reassembles a global isomorphism.

This is the base case of the deficit-marking mechanism for canonical symmetry breaking (see research/attacks/symmetry-breaking.md): deleting a vertex stamps its neighbourhood into the card as a degree deficit. In a regular graph the stamp is fully legible; the general programme is to characterize when the stamp can be canonically decoded (marking rigidity) in irregular graphs.

Main results

• SimpleGraph.degree_deleteVert — the degree of a card vertex drops by one exactly on the deleted vertex's neighbourhood;
• SimpleGraph.IsRegularOfDegree.adj_iff_degree_deleteVert_ne — in a d-regular graph, adjacency to the deleted vertex is equivalent to card-degree ≠ d (stated with ≠ so the edgeless case d = 0 needs no special handling);
• SimpleGraph.nonempty_iso_of_regular — regular graphs are reconstructible.

References

• Kelly, P. J. (1957). "A congruence theorem for trees" (the surrounding folklore); see also Bondy (1991), "A graph reconstructor's manual".

theorem SimpleGraph.degree_deleteVert {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (v : V) (x : { w : V // w ≠ v }) : (G.deleteVert v).degree x = if G.Adj (↑x) v then G.degree ↑x - 1 else G.degree ↑x

Deleting v lowers the degree of exactly its neighbours by one: the deficit stamp of the deleted vertex on its card.

theorem SimpleGraph.degree_deleteVert_of_not_adj {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {v : V} {x : { w : V // w ≠ v }} (h : ¬G.Adj v ↑x) : (G.deleteVert v).degree x = G.degree ↑x

Pointwise core of the shift recurrence (Discovery A, research/attacks/symmetry-breaking.md): a non-neighbour of the deleted vertex keeps its degree on the card.

theorem SimpleGraph.degree_deleteVert_add_one_of_adj {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {v : V} {x : { w : V // w ≠ v }} (h : G.Adj v ↑x) : (G.deleteVert v).degree x + 1 = G.degree ↑x

Pointwise core of the shift recurrence (Discovery A): a neighbour of the deleted vertex drops exactly one degree on the card. Stated additively (card-degree + 1 = degree) so no truncated subtraction appears.

theorem SimpleGraph.IsRegularOfDegree.adj_iff_degree_deleteVert_ne {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {d : ℕ} (hreg : G.IsRegularOfDegree d) (v : V) (x : { w : V // w ≠ v }) : G.Adj (↑x) v ↔ (G.deleteVert v).degree x ≠ d

In a d-regular graph the deficit stamp is fully legible: a card vertex is a neighbour of the deleted vertex iff its card-degree differs from d. Stated with ≠ d so that the edgeless case d = 0 (where d - 1 would wrap) is automatic.

theorem SimpleGraph.iso_degree_eq {V₁ : Type u_2} {V₂ : Type u_3} [Fintype V₁] [Fintype V₂] {A : SimpleGraph V₁} {B : SimpleGraph V₂} [DecidableRel A.Adj] [DecidableRel B.Adj] (φ : A ≃g B) (a : V₁) : B.degree (φ a) = A.degree a

Degree is invariant under graph isomorphisms (helper, by transporting the neighbour set along the isomorphism).

The rigid-card criterion

def SimpleGraph.RigidVertex {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (v : V) : Prop

A vertex v of G is rigid if every card isomorphism onto a card of a graph with the same degree data can be corrected by a card automorphism so that it respects the deleted vertices' attachments. Rigidity says the neighbour-marking of the card is canonical up to card automorphism — the symmetry-breaking property of the deficit-marking programme (research/attacks/symmetry-breaking.md).

Equations

• One or more equations did not get rendered due to their size.

theorem SimpleGraph.nonempty_iso_of_rigidVertex {V : Type u_1} [Fintype V] {G H : SimpleGraph V} [DecidableRel G.Adj] {v : V} (hrig : G.RigidVertex v) (h : G.SameDeck H) (hV : 3 ≤ Fintype.card V) : Nonempty (G ≃g H)

The rigid-card criterion: one rigid vertex suffices. If G has a rigid vertex, then any graph with the same deck is isomorphic to G: the deck supplies a card isomorphism with matching degree data (degree multisets and the deleted degree are reconstructible), rigidity corrects it to respect the attachments, and isoOfDeleteVertIso reassembles the global isomorphism.

theorem SimpleGraph.IsRegularOfDegree.rigidVertex {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {d : ℕ} (hreg : G.IsRegularOfDegree d) (v : V) : G.RigidVertex v

Every vertex of a regular graph is rigid: the deficit stamp makes the marking degree-forced, so no correcting automorphism is needed.

theorem SimpleGraph.nonempty_iso_of_regular {V : Type u_1} [Fintype V] {G H : SimpleGraph V} [DecidableRel G.Adj] {d : ℕ} (hreg : G.IsRegularOfDegree d) (h : G.SameDeck H) (hV : 3 ≤ Fintype.card V) : Nonempty (G ≃g H)

Regular graphs are reconstructible — the base case of the deficit-marking mechanism, now derived from the rigid-card criterion: in a regular graph every vertex is rigid (IsRegularOfDegree.rigidVertex).