Twins and Twin Transpositions

Step (i) of the twin-flexible rung of the symmetry-breaking programme (research/attacks/symmetry-breaking.md): two vertices are twins if they have the same neighbours apart from each other, and the transposition of a twin pair is a graph automorphism (twinSwapIso).

In the marking picture: if a mixed card-degree class consists of pairwise twins, the choice of which class members are the deleted vertex's neighbours can be re-pointed freely by composing twin transpositions — the ambiguity that mixed classes leave (after SameDeck.nbrCount_eq fixes their sizes) is absorbed by card automorphisms. The class-by-class assembly is the next layer; this module provides the verified swap.

def SimpleGraph.AreTwinVertices {V : Type u_1} (G : SimpleGraph V) (u u' : V) : Prop

Two vertices are twins if every other vertex sees them identically. No condition is placed on the edge between them, so this covers both twin flavours at once.

Equations

• G.AreTwinVertices u u' = ∀ (z : V), z ≠ u → z ≠ u' → (G.Adj u z ↔ G.Adj u' z)

theorem SimpleGraph.AreTwinVertices.symm {V : Type u_1} {G : SimpleGraph V} {u u' : V} (h : G.AreTwinVertices u u') : G.AreTwinVertices u' u

def SimpleGraph.twinSwapIso {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] {u u' : V} (h : G.AreTwinVertices u u') : G ≃g G

A twin transposition is an automorphism. Swapping a twin pair preserves adjacency: pairs disjoint from {u, u'} are untouched, the pair (u, u') maps to (u', u) (symmetry), and a mixed pair (u, z) maps to (u', z) (twin property).

Equations

• SimpleGraph.twinSwapIso h = { toEquiv := Equiv.swap u u', map_rel_iff' := ⋯ }

@[simp]

theorem SimpleGraph.twinSwapIso_apply {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] {u u' : V} (h : G.AreTwinVertices u u') (x : V) : (twinSwapIso h) x = (Equiv.swap u u') x

Twin-supported involutions are automorphisms

theorem SimpleGraph.twin_involution_map_rel {V : Type u_1} {G : SimpleGraph V} {f : V → V} (hinv : Function.Involutive f) (hmove : ∀ (x : V), f x ≠ x → G.AreTwinVertices x (f x)) (x y : V) : G.Adj (f x) (f y) ↔ G.Adj x y

An involution that only moves vertices to their twins preserves adjacency. The generalization of twinSwapIso from one transposition to any twin-supported involution; involutivity closes the corner where the two moved pairs collide (y = f x forces f y = x).

def SimpleGraph.twinInvolutionIso {V : Type u_1} {G : SimpleGraph V} {f : V → V} (hinv : Function.Involutive f) (hmove : ∀ (x : V), f x ≠ x → G.AreTwinVertices x (f x)) : G ≃g G

Package a twin-supported involution as a graph automorphism.

Equations

• SimpleGraph.twinInvolutionIso hinv hmove = { toEquiv := Function.Involutive.toPerm f hinv, map_rel_iff' := ⋯ }