Value-Separated Vertices are Rigid — the Telescoping Argument

Discovery B of the symmetry-breaking programme (research/attacks/symmetry-breaking.md): call a vertex v value-separated if no non-neighbour of v shares a card-degree with a neighbour of v. Then v is rigid, hence any graph possessing such a vertex is reconstructible — a strict extension of the regular case (where every card-degree class is trivially all-neighbours or all-non-neighbours).

The proof is the telescoping argument: for each card-degree value t, the counts of neighbours (nbrCount), non-neighbours (nonNbrCount), the full class (classCount), and the G-degree classes (fullDegCount) satisfy

• classCount t = nbrCount t + nonNbrCount t (partition);
• fullDegCount t = shiftNbrCount t + nonNbrCount t where shiftNbrCount (t+1) = nbrCount t, shiftNbrCount 0 = 0 (the deficit stamp, pointwise);

and the deck matches classCount (via the card isomorphism) and fullDegCount (via the degree multiset and the deleted degree) across the two graphs. Induction on t then forces the neighbour counts to agree classwise, and value-separation upgrades classwise agreement to the pointwise link condition.

Main results

• SimpleGraph.ValueSeparated — the separation predicate;
• SimpleGraph.ValueSeparated.rigidVertex — value-separated vertices are rigid;
• SimpleGraph.nonempty_iso_of_valueSeparated — graphs with a value-separated vertex are reconstructible.

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

v is value-separated if no non-neighbour shares a card-degree value with a neighbour: every card-degree class of G − v is all-neighbours or all-non-neighbours of v.

Equations

• G.ValueSeparated v = ∀ (x y : { w : V // w ≠ v }), ¬G.Adj v ↑x → G.Adj v ↑y → (G.deleteVert v).degree x ≠ (G.deleteVert v).degree y

Value-class counts on a card

def SimpleGraph.nbrCount {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (v : V) (t : ℕ) : ℕ

Number of neighbours of the deleted vertex with card-degree t.

Equations

• G.nbrCount v t = {x : { w : V // w ≠ v } | (G.deleteVert v).degree x = t ∧ G.Adj v ↑x}.card

def SimpleGraph.nonNbrCount {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (v : V) (t : ℕ) : ℕ

Number of non-neighbours of the deleted vertex with card-degree t.

Equations

• G.nonNbrCount v t = {x : { w : V // w ≠ v } | (G.deleteVert v).degree x = t ∧ ¬G.Adj v ↑x}.card

Transfer across a degree-matched card isomorphism

Value-separated vertices are rigid

theorem SimpleGraph.ValueSeparated.rigidVertex {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {v : V} (hsep : G.ValueSeparated v) : G.RigidVertex v

Value-separated vertices are rigid (Discovery B): classwise neighbour counts are forced by the telescoping recurrence, and value-separation makes classwise agreement pointwise — the identity correction works.

theorem SimpleGraph.SameDeck.nbrCount_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) (t : ℕ), G.nbrCount v t = H.nbrCount (σ v) t ∧ G.nonNbrCount v t = H.nonNbrCount (σ v) t

Discovery A, public deck form: the value-class neighbour profile of every matched card is deck-forced. For same-deck graphs there is a vertex matching σ such that, for every vertex v and every card-degree value t, the number of v-neighbours of card-degree t in G − v equals the number of σv-neighbours of card-degree t in H − σv (and likewise for non-neighbours). In particular the neighbour-degree multiset of v is deck-determined along the matching: the only labelling freedom the deck ever leaves is which vertices within a card-degree class are the neighbours. This is the formal content of the shift-recurrence discovery in research/attacks/symmetry-breaking.md.

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

Graphs with a value-separated vertex are reconstructible — Discovery B combined with the rigid-card criterion. Strictly extends nonempty_iso_of_regular.

theorem SimpleGraph.nonempty_iso_of_injective_card_degrees {V : Type u_1} [Fintype V] [DecidableEq V] {G H : SimpleGraph V} [DecidableRel G.Adj] {v : V} (hinj : Function.Injective fun (x : { w : V // w ≠ v }) => (G.deleteVert v).degree x) (h : G.SameDeck H) (hV : 3 ≤ Fintype.card V) : Nonempty (G ≃g H)

A card with pairwise-distinct degrees has no mixed class at all, so its deleted vertex is value-separated; a graph with an injective-degree card is reconstructible. A purely card-side recognizable criterion.

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

Every vertex of a regular graph is value-separated: non-neighbours keep card-degree d, neighbours drop to d − 1.