From ccee8571e30d4e043b3825a48c1019e9b2d769df Mon Sep 17 00:00:00 2001
From: Robin Langer <langer.robin@gmail.com>
Date: Tue, 19 May 2026 00:26:43 +1000
Subject: [PATCH 01/14] feat(Combinatorics/SimpleGraph): group actions on
 simple graphs
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This adds the first connection between Mathlib's `MulAction` and `SimpleGraph` libraries, defining what it means for a group action to preserve adjacency and providing the standard transitivity predicates used in algebraic graph theory.

The `GraphAction` class asserts that `g • u` is adjacent to `g • v` whenever `u` is adjacent to `v`. For group actions this is automatically an iff (`adj_smul_iff`), and each group element induces a graph isomorphism (`toIso`). On top of this, `IsVertexTransitive` combines `GraphAction` with `IsPretransitive`, and `IsArcTransitive` requires transitivity on ordered adjacent pairs.

The main result is the characterization theorem: a vertex-transitive graph that is locally transitive (the stabilizer of each vertex acts transitively on its neighbors) is arc-transitive, and conversely an arc-transitive graph with no isolated vertices is vertex-transitive. This is the standard equivalence between arc-transitivity and the combination of vertex-transitivity with local transitivity, used throughout the theory of symmetric graphs.
---
 Mathlib/Combinatorics/SimpleGraph/Action.lean | 129 ++++++++++++++++++
 1 file changed, 129 insertions(+)
 create mode 100644 Mathlib/Combinatorics/SimpleGraph/Action.lean

diff --git a/Mathlib/Combinatorics/SimpleGraph/Action.lean b/Mathlib/Combinatorics/SimpleGraph/Action.lean
new file mode 100644
index 00000000000000..0b7875c8109f46
--- /dev/null
+++ b/Mathlib/Combinatorics/SimpleGraph/Action.lean
@@ -0,0 +1,129 @@
+/-
+Copyright (c) 2026 Robin Langer. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Robin Langer
+-/
+module
+
+public import Mathlib.Combinatorics.SimpleGraph.Maps
+public import Mathlib.GroupTheory.GroupAction.Basic
+
+/-!
+# Group actions on simple graphs
+
+Given a group `G` acting on a type `V` via `MulAction G V`, and a simple graph `Γ : SimpleGraph V`,
+we say the action is a *graph action* if it preserves adjacency: `Γ.Adj u v → Γ.Adj (g • u) (g • v)`
+for all `g : G`.
+
+## Main definitions
+
+* `GraphAction G Γ` — the action of `G` on `V` preserves the adjacency relation of `Γ`
+* `GraphAction.adj_smul_iff` — for groups, adjacency is an iff (not just an implication)
+* `GraphAction.toIso` — each `g : G` induces a graph isomorphism `Γ ≃g Γ`
+* `IsVertexTransitive G Γ` — the action is a graph action and is transitive
+* `IsArcTransitive G Γ` — the action is transitive on ordered adjacent pairs
+* `IsLocallyTransitive G Γ v` — the stabilizer of `v` acts transitively on its neighbors
+
+## Main results
+
+* `isArcTransitive_of_vertexTransitive_locallyTransitive` — vertex-transitive + locally
+  transitive implies arc-transitive
+-/
+
+@[expose] public section
+
+variable {G V : Type*}
+
+/-- A group action on `V` is a *graph action* on `Γ : SimpleGraph V` if it preserves adjacency. -/
+class GraphAction (G : Type*) (V : Type*) [Group G] [MulAction G V]
+    (Γ : SimpleGraph V) : Prop where
+  /-- The action preserves adjacency. -/
+  adj_smul : ∀ (g : G) (u v : V), Γ.Adj u v → Γ.Adj (g • u) (g • v)
+
+namespace GraphAction
+
+variable [Group G] [MulAction G V] {Γ : SimpleGraph V} [GraphAction G V Γ]
+
+/-- For group actions, adjacency is preserved in both directions:
+`Γ.Adj (g • u) (g • v) ↔ Γ.Adj u v`. -/
+theorem adj_smul_iff (g : G) (u v : V) : Γ.Adj (g • u) (g • v) ↔ Γ.Adj u v := by
+  constructor
+  · intro h
+    have h' := adj_smul g⁻¹ (g • u) (g • v) h
+    simp only [inv_smul_smul] at h'
+    exact h'
+  · exact adj_smul g u v
+
+/-- Each group element `g` induces a graph isomorphism `Γ ≃g Γ`. -/
+noncomputable def toIso (g : G) : Γ ≃g Γ where
+  toEquiv := MulAction.toPerm g
+  map_rel_iff' := adj_smul_iff g _ _
+
+@[simp]
+theorem toIso_apply (g : G) (v : V) : (toIso g : Γ ≃g Γ) v = g • v := rfl
+
+@[simp]
+theorem toIso_symm (g : G) : (toIso g : Γ ≃g Γ).symm = toIso g⁻¹ := by
+  ext v
+  simp [toIso]
+
+theorem toIso_mul (g h : G) :
+    (toIso (g * h) : Γ ≃g Γ) = (toIso h : Γ ≃g Γ).trans (toIso g) := by
+  ext v
+  simp [toIso, mul_smul]
+
+end GraphAction
+
+/-- A graph `Γ` is *vertex-transitive* under the action of `G` if `G` preserves adjacency
+and acts transitively on the vertices. -/
+class IsVertexTransitive (G : Type*) (V : Type*) [Group G] [MulAction G V]
+    (Γ : SimpleGraph V) : Prop extends GraphAction G V Γ where
+  /-- The action is transitive on vertices. -/
+  pretransitive : MulAction.IsPretransitive G V
+
+attribute [instance] IsVertexTransitive.pretransitive
+
+/-- A graph `Γ` is *arc-transitive* under the action of `G` if for any two arcs
+`(u₁, v₁)` and `(u₂, v₂)`, there exists `g ∈ G` sending `u₁ ↦ u₂` and `v₁ ↦ v₂`. -/
+class IsArcTransitive (G : Type*) (V : Type*) [Group G] [MulAction G V]
+    (Γ : SimpleGraph V) : Prop extends GraphAction G V Γ where
+  /-- The action is transitive on arcs (ordered adjacent pairs). -/
+  arc_transitive : ∀ u₁ v₁ u₂ v₂ : V, Γ.Adj u₁ v₁ → Γ.Adj u₂ v₂ →
+    ∃ g : G, g • u₁ = u₂ ∧ g • v₁ = v₂
+
+namespace IsArcTransitive
+
+variable [Group G] [MulAction G V] {Γ : SimpleGraph V} [IsArcTransitive G V Γ]
+
+/-- An arc-transitive graph with no isolated vertices is vertex-transitive. -/
+theorem isVertexTransitive (hne : ∀ v : V, ∃ w : V, Γ.Adj v w) :
+    IsVertexTransitive G V Γ where
+  pretransitive := ⟨by
+    intro x y
+    obtain ⟨x', hx'⟩ := hne x
+    obtain ⟨y', hy'⟩ := hne y
+    obtain ⟨g, hg, _⟩ := @arc_transitive G V _ _ Γ _ x x' y y' hx' hy'
+    exact ⟨g, hg⟩⟩
+
+end IsArcTransitive
+
+/-- A graph is *locally transitive* at `v` if the stabilizer of `v` acts transitively
+on the neighbors of `v`. -/
+def IsLocallyTransitive (G : Type*) (V : Type*) [Group G] [MulAction G V]
+    (Γ : SimpleGraph V) (v : V) : Prop :=
+  ∀ w₁ w₂ : V, Γ.Adj v w₁ → Γ.Adj v w₂ →
+    ∃ g : G, g • v = v ∧ g • w₁ = w₂
+
+/-- A vertex-transitive, locally transitive graph is arc-transitive. -/
+theorem isArcTransitive_of_vertexTransitive_locallyTransitive
+    [Group G] [MulAction G V] (Γ : SimpleGraph V) [IsVertexTransitive G V Γ]
+    (hlocal : ∀ v : V, IsLocallyTransitive G V Γ v) :
+    IsArcTransitive G V Γ where
+  arc_transitive := by
+    intro u₁ v₁ u₂ v₂ h₁ h₂
+    obtain ⟨g, hg⟩ := MulAction.exists_smul_eq G u₁ u₂
+    have hadj : Γ.Adj u₂ (g • v₁) := by
+      rw [← hg]
+      exact GraphAction.adj_smul g u₁ v₁ h₁
+    obtain ⟨h, hhu₂, hhv⟩ := hlocal u₂ (g • v₁) v₂ hadj h₂
+    exact ⟨h * g, by rw [mul_smul, hg, hhu₂], by rw [mul_smul, hhv]⟩

From a2a550510498047aa7dc13a3deb7f375f5287646 Mon Sep 17 00:00:00 2001
From: Robin Langer <langer.robin@gmail.com>
Date: Tue, 19 May 2026 05:52:48 +1000
Subject: [PATCH 02/14] chore: add Action.lean to Mathlib.lean

---
 Mathlib.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib.lean b/Mathlib.lean
index 51a2d9e682d0ca..ce3cedcbd862ef 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -3574,6 +3574,7 @@ public import Mathlib.Combinatorics.SetFamily.KruskalKatona
 public import Mathlib.Combinatorics.SetFamily.LYM
 public import Mathlib.Combinatorics.SetFamily.Shadow
 public import Mathlib.Combinatorics.SetFamily.Shatter
+public import Mathlib.Combinatorics.SimpleGraph.Action
 public import Mathlib.Combinatorics.SimpleGraph.Acyclic
 public import Mathlib.Combinatorics.SimpleGraph.AdjMatrix
 public import Mathlib.Combinatorics.SimpleGraph.Basic

From bca5030e9ed40c2544c17f4e12e8289bf92db7fb Mon Sep 17 00:00:00 2001
From: Robin Langer <langer.robin@gmail.com>
Date: Tue, 19 May 2026 05:59:30 +1000
Subject: [PATCH 03/14] feat(Combinatorics/SimpleGraph): coset graphs
 (Sabidussi construction)

---
 Mathlib.lean                                  |   1 +
 .../Combinatorics/SimpleGraph/CosetGraph.lean | 128 ++++++++++++++++++
 2 files changed, 129 insertions(+)
 create mode 100644 Mathlib/Combinatorics/SimpleGraph/CosetGraph.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index ce3cedcbd862ef..597c17fbe8133f 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -3592,6 +3592,7 @@ public import Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
 public import Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents
 public import Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
 public import Mathlib.Combinatorics.SimpleGraph.Copy
+public import Mathlib.Combinatorics.SimpleGraph.CosetGraph
 public import Mathlib.Combinatorics.SimpleGraph.Dart
 public import Mathlib.Combinatorics.SimpleGraph.DegreeSum
 public import Mathlib.Combinatorics.SimpleGraph.DeleteEdges
diff --git a/Mathlib/Combinatorics/SimpleGraph/CosetGraph.lean b/Mathlib/Combinatorics/SimpleGraph/CosetGraph.lean
new file mode 100644
index 00000000000000..c2ffaf6692651a
--- /dev/null
+++ b/Mathlib/Combinatorics/SimpleGraph/CosetGraph.lean
@@ -0,0 +1,128 @@
+/-
+Copyright (c) 2026 Robin Langer. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Robin Langer
+-/
+module
+
+public import Mathlib.Combinatorics.SimpleGraph.Action
+public import Mathlib.GroupTheory.GroupAction.Quotient
+public import Mathlib.GroupTheory.DoubleCoset
+public import Mathlib.Tactic.Group
+
+/-!
+# Coset graphs (Sabidussi construction)
+
+Given a group `G`, a subgroup `H`, and a *connection set* `D ⊆ G` that is a union of
+`(H, H)`-double cosets, is symmetric (`D = D⁻¹`), and is disjoint from `H`, we define the
+**coset graph** `Sab(G, H, D)` whose vertices are the left cosets `G ⧸ H` and whose edges
+connect `xH` to `yH` whenever `x⁻¹y ∈ D`.
+
+This is Sabidussi's generalization of Cayley graphs: when `H = ⊥`, the coset graph on
+`G ⧸ ⊥ ≃ G` recovers the Cayley graph `Cay(G, D)`.
+
+## Main definitions
+
+* `IsConnectionSet H D` — `D` is a union of `(H, H)`-double cosets, closed under inversion,
+  and disjoint from `H`
+* `SimpleGraph.cosetGraph H D` — the coset graph `Sab(G, H, D)` as a `SimpleGraph (G ⧸ H)`
+
+## Main results
+
+* `SimpleGraph.cosetGraph.adj_mk` — adjacency is characterized by `x⁻¹y ∈ D`
+* `SimpleGraph.cosetGraph.graphAction` — `G` acts on the coset graph preserving adjacency
+* `SimpleGraph.cosetGraph.isVertexTransitive` — coset graphs are vertex-transitive
+
+## References
+
+* Robin Langer, *Symmetric Graphs and their Quotients*, arXiv:1306.4798, Chapter 2 §2.
+* Sabidussi, *Vertex-transitive graphs*, Monatsh. Math. 68 (1964), 426–438.
+-/
+
+@[expose] public section
+
+variable {G : Type*} [Group G]
+
+/-- A set `D ⊆ G` is a *connection set* for the subgroup `H` if it is stable under
+left and right multiplication by `H` (i.e., a union of `(H,H)`-double cosets),
+is closed under inversion, and is disjoint from `H`. -/
+structure IsConnectionSet (H : Subgroup G) (D : Set G) : Prop where
+  /-- `D` is stable under left and right multiplication by elements of `H`. -/
+  double_coset_stable : ∀ d ∈ D, ∀ h₁ ∈ (H : Set G), ∀ h₂ ∈ (H : Set G), h₁ * d * h₂ ∈ D
+  /-- `D` is closed under inversion. -/
+  inv_mem : ∀ d ∈ D, d⁻¹ ∈ D
+  /-- `D` is disjoint from `H`. -/
+  disjoint : Disjoint D ↑H
+
+namespace IsConnectionSet
+
+variable {H : Subgroup G} {D : Set G}
+
+theorem one_not_mem (hD : IsConnectionSet H D) : (1 : G) ∉ D :=
+  fun h => Set.disjoint_left.mp hD.disjoint h (Subgroup.one_mem H)
+
+end IsConnectionSet
+
+/-- The **coset graph** `Sab(G, H, D)`. Vertices are the left cosets `G ⧸ H`,
+and two cosets `xH, yH` are adjacent iff `x⁻¹y ∈ D`.
+
+This is Sabidussi's generalization of Cayley graphs: when `H = ⊥`,
+the coset graph on `G ⧸ ⊥ ≃ G` recovers the Cayley graph `Cay(G, D)`. -/
+noncomputable def SimpleGraph.cosetGraph (H : Subgroup G) (D : Set G)
+    (hD : IsConnectionSet H D) : SimpleGraph (G ⧸ H) where
+  Adj q₁ q₂ := Quotient.liftOn₂ q₁ q₂ (fun x y => x⁻¹ * y ∈ D)
+    (fun a₁ b₁ a₂ b₂ h₁ h₂ => by
+      have ha : a₁⁻¹ * a₂ ∈ (H : Set G) := QuotientGroup.leftRel_apply.mp h₁
+      have hb : b₁⁻¹ * b₂ ∈ (H : Set G) := QuotientGroup.leftRel_apply.mp h₂
+      apply propext; change a₁⁻¹ * b₁ ∈ D ↔ a₂⁻¹ * b₂ ∈ D; constructor
+      · intro h
+        have key : a₂⁻¹ * b₂ = (a₂⁻¹ * a₁) * (a₁⁻¹ * b₁) * (b₁⁻¹ * b₂) := by group
+        rw [key]
+        refine hD.double_coset_stable _ h _ ?_ _ hb
+        have : (a₁⁻¹ * a₂)⁻¹ ∈ (H : Set G) := H.inv_mem ha
+        rwa [mul_inv_rev, inv_inv] at this
+      · intro h
+        have key : a₁⁻¹ * b₁ = (a₁⁻¹ * a₂) * (a₂⁻¹ * b₂) * (b₂⁻¹ * b₁) := by group
+        rw [key]
+        refine hD.double_coset_stable _ h _ ha _ ?_
+        have : (b₁⁻¹ * b₂)⁻¹ ∈ (H : Set G) := H.inv_mem hb
+        rwa [mul_inv_rev, inv_inv] at this)
+  symm := by
+    intro q₁ q₂
+    refine Quotient.inductionOn₂ q₁ q₂ fun x y => ?_
+    simp only [Quotient.liftOn₂_mk]
+    intro h
+    have hmem := hD.inv_mem _ h
+    rwa [mul_inv_rev, inv_inv] at hmem
+  loopless := ⟨by
+    intro q
+    refine Quotient.inductionOn q fun x => ?_
+    simp only [Quotient.liftOn₂_mk]
+    show ¬(x⁻¹ * x ∈ D)
+    rw [inv_mul_cancel]
+    exact hD.one_not_mem⟩
+
+namespace SimpleGraph.cosetGraph
+
+variable (H : Subgroup G) (D : Set G) (hD : IsConnectionSet H D)
+
+/-- Adjacency in the coset graph is characterized by membership of `x⁻¹y` in `D`. -/
+@[simp]
+theorem adj_mk (x y : G) :
+    (cosetGraph H D hD).Adj (QuotientGroup.mk x) (QuotientGroup.mk y) ↔ x⁻¹ * y ∈ D :=
+  Iff.rfl
+
+/-- The left multiplication action of `G` on `G ⧸ H` preserves coset graph adjacency. -/
+instance graphAction : GraphAction G (G ⧸ H) (cosetGraph H D hD) where
+  adj_smul g q₁ q₂ := by
+    refine Quotient.inductionOn₂ q₁ q₂ fun x y => ?_
+    intro h
+    change (g * x)⁻¹ * (g * y) ∈ D
+    rw [mul_inv_rev, mul_assoc, inv_mul_cancel_left]
+    exact h
+
+/-- Coset graphs are vertex-transitive under the natural action of `G`. -/
+instance isVertexTransitive : IsVertexTransitive G (G ⧸ H) (cosetGraph H D hD) where
+  pretransitive := MulAction.isPretransitive_quotient G H
+
+end SimpleGraph.cosetGraph

From 908c301624478b0b7314b99f0b584e1b46855c13 Mon Sep 17 00:00:00 2001
From: Robin Langer <langer.robin@gmail.com>
Date: Tue, 19 May 2026 06:04:16 +1000
Subject: [PATCH 04/14] feat(Combinatorics/SimpleGraph): Sabidussi
 representation theorem

---
 Mathlib.lean                                  |   1 +
 .../SimpleGraph/Representation.lean           | 161 ++++++++++++++++++
 2 files changed, 162 insertions(+)
 create mode 100644 Mathlib/Combinatorics/SimpleGraph/Representation.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 597c17fbe8133f..4bcf38b25f4bdb 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -3628,6 +3628,7 @@ public import Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
 public import Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
 public import Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma
 public import Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
+public import Mathlib.Combinatorics.SimpleGraph.Representation
 public import Mathlib.Combinatorics.SimpleGraph.StronglyRegular
 public import Mathlib.Combinatorics.SimpleGraph.Subgraph
 public import Mathlib.Combinatorics.SimpleGraph.Sum
diff --git a/Mathlib/Combinatorics/SimpleGraph/Representation.lean b/Mathlib/Combinatorics/SimpleGraph/Representation.lean
new file mode 100644
index 00000000000000..020db8d31abfb8
--- /dev/null
+++ b/Mathlib/Combinatorics/SimpleGraph/Representation.lean
@@ -0,0 +1,161 @@
+/-
+Copyright (c) 2026 Robin Langer. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Robin Langer
+-/
+module
+
+public import Mathlib.Combinatorics.SimpleGraph.CosetGraph
+public import Mathlib.GroupTheory.GroupAction.Quotient
+public import Mathlib.Tactic.Group
+
+/-!
+# The Sabidussi representation theorem
+
+Every vertex-transitive graph is isomorphic to a coset graph. More precisely,
+if `G` acts vertex-transitively on a graph `Γ`, then for any basepoint `v`,
+the orbit-stabilizer equivalence `V ≃ G ⧸ stabilizer G v` is a graph
+isomorphism from `Γ` to `Sab(G, Gᵥ, D)`, where `D = {g ∈ G : Γ.Adj v (g • v)}`.
+
+## Main definitions
+
+* `connectionSet G Γ v` — the set of group elements moving `v` to a neighbor
+* `connectionSet.isConnectionSet` — the connection set satisfies the axioms
+* `sabidussiEquiv` — the equivalence `V ≃ G ⧸ stabilizer G v` for transitive actions
+* `sabidussiIso` — the graph isomorphism `Γ ≃g cosetGraph (stabilizer G v) D`
+
+## References
+
+* Robin Langer, *Symmetric Graphs and their Quotients*, arXiv:1306.4798, Chapter 2 §2.
+* Sabidussi, *Vertex-transitive graphs*, Monatsh. Math. 68 (1964), 426–438.
+-/
+
+@[expose] public section
+
+variable {G V : Type*} [Group G] [MulAction G V] {Γ : SimpleGraph V}
+
+/-! ### The connection set -/
+
+/-- The *connection set* of a basepoint `v` in a graph action: the set of group elements
+that move `v` to one of its neighbors. -/
+def connectionSet (G : Type*) [Group G] [MulAction G V]
+    (Γ : SimpleGraph V) [GraphAction G V Γ] (v : V) : Set G :=
+  {g : G | Γ.Adj v (g • v)}
+
+namespace connectionSet
+
+variable [GraphAction G V Γ] (v : V)
+
+theorem one_not_mem : (1 : G) ∉ connectionSet G Γ v := by
+  simp [connectionSet]
+
+theorem inv_mem {g : G} (hg : g ∈ connectionSet G Γ v) :
+    g⁻¹ ∈ connectionSet G Γ v := by
+  simp only [connectionSet, Set.mem_setOf_eq] at hg ⊢
+  have h := Γ.symm hg
+  rwa [← GraphAction.adj_smul_iff g⁻¹, inv_smul_smul] at h
+
+theorem double_coset_stable {g : G} (hg : g ∈ connectionSet G Γ v)
+    {h₁ : G} (hh₁ : h₁ ∈ MulAction.stabilizer G v)
+    {h₂ : G} (hh₂ : h₂ ∈ MulAction.stabilizer G v) :
+    h₁ * g * h₂ ∈ connectionSet G Γ v := by
+  simp only [connectionSet, Set.mem_setOf_eq] at hg ⊢
+  rw [mul_smul, mul_smul, MulAction.mem_stabilizer_iff.mp hh₂]
+  have := GraphAction.adj_smul h₁ v (g • v) hg
+  rwa [MulAction.mem_stabilizer_iff.mp hh₁] at this
+
+theorem disjoint_stabilizer :
+    Disjoint (connectionSet G Γ v) ↑(MulAction.stabilizer G v) := by
+  rw [Set.disjoint_left]
+  intro g hg hstab
+  simp only [connectionSet, Set.mem_setOf_eq] at hg
+  rw [SetLike.mem_coe, MulAction.mem_stabilizer_iff] at hstab
+  rw [hstab] at hg
+  exact (Γ.loopless.irrefl v) hg
+
+/-- The connection set forms a valid `IsConnectionSet` for the stabilizer subgroup. -/
+theorem isConnectionSet :
+    IsConnectionSet (MulAction.stabilizer G v) (connectionSet G Γ v) where
+  double_coset_stable _ hd _ hh₁ _ hh₂ := double_coset_stable v hd hh₁ hh₂
+  inv_mem _ hd := inv_mem v hd
+  disjoint := disjoint_stabilizer v
+
+end connectionSet
+
+/-! ### The orbit-stabilizer equivalence -/
+
+section SabidussiRepresentation
+
+variable [GraphAction G V Γ] [MulAction.IsPretransitive G V] (v : V)
+
+/-- The equivalence `V ≃ G ⧸ stabilizer G v` for a transitive action.
+
+The forward map sends `u` to the coset `gH` where `g • v = u`.
+The inverse map sends `⟦g⟧` to `g • v`. -/
+noncomputable def sabidussiEquiv : V ≃ G ⧸ MulAction.stabilizer G v where
+  toFun u := QuotientGroup.mk (MulAction.exists_smul_eq G v u).choose
+  invFun := Quotient.lift (· • v) (by
+    intro a b hab
+    have hmem : (a⁻¹ * b) • v = v :=
+      MulAction.mem_stabilizer_iff.mp (QuotientGroup.leftRel_apply.mp hab)
+    calc a • v = a • ((a⁻¹ * b) • v) := by rw [hmem]
+      _ = (a * (a⁻¹ * b)) • v := (mul_smul a (a⁻¹ * b) v).symm
+      _ = b • v := by rw [mul_inv_cancel_left])
+  left_inv u := by
+    simp only
+    exact (MulAction.exists_smul_eq G v u).choose_spec
+  right_inv := by
+    intro q
+    refine Quotient.inductionOn q fun g => ?_
+    simp only [Quotient.lift_mk]
+    apply QuotientGroup.eq.mpr
+    rw [MulAction.mem_stabilizer_iff, mul_smul]
+    set g' := (MulAction.exists_smul_eq G v (g • v)).choose
+    have hspec : g' • v = g • v := (MulAction.exists_smul_eq G v (g • v)).choose_spec
+    calc g'⁻¹ • (g • v) = g'⁻¹ • (g' • v) := by rw [hspec]
+      _ = v := inv_smul_smul g' v
+
+@[simp]
+theorem sabidussiEquiv_smul (g : G) :
+    sabidussiEquiv v (g • v) = (g : G ⧸ MulAction.stabilizer G v) := by
+  simp only [sabidussiEquiv]
+  apply QuotientGroup.eq.mpr
+  rw [MulAction.mem_stabilizer_iff, mul_smul]
+  set g' := (MulAction.exists_smul_eq G v (g • v)).choose
+  have hspec : g' • v = g • v := (MulAction.exists_smul_eq G v (g • v)).choose_spec
+  calc g'⁻¹ • (g • v) = g'⁻¹ • (g' • v) := by rw [hspec]
+    _ = v := inv_smul_smul g' v
+
+@[simp]
+theorem sabidussiEquiv_symm_mk (g : G) :
+    (sabidussiEquiv v).symm (QuotientGroup.mk g) = g • v := by
+  rfl
+
+/-- **Sabidussi's Representation Theorem**: Every vertex-transitive graph is
+isomorphic to a coset graph.
+
+The orbit-stabilizer equivalence `V ≃ G ⧸ stabilizer G v` is a graph isomorphism
+from `Γ` to `cosetGraph (stabilizer G v) (connectionSet G Γ v)`. -/
+noncomputable def sabidussiIso :
+    Γ ≃g SimpleGraph.cosetGraph (MulAction.stabilizer G v)
+      (connectionSet G Γ v) (connectionSet.isConnectionSet v) where
+  toEquiv := sabidussiEquiv v
+  map_rel_iff' := by
+    intro u w
+    set g₁ := (MulAction.exists_smul_eq G v u).choose
+    set g₂ := (MulAction.exists_smul_eq G v w).choose
+    have hu : g₁ • v = u := (MulAction.exists_smul_eq G v u).choose_spec
+    have hw : g₂ • v = w := (MulAction.exists_smul_eq G v w).choose_spec
+    change g₁⁻¹ * g₂ ∈ connectionSet G Γ v ↔ Γ.Adj u w
+    rw [← hu, ← hw]
+    simp only [connectionSet, Set.mem_setOf_eq, mul_smul]
+    constructor
+    · intro h
+      have := (@GraphAction.adj_smul_iff G V _ _ Γ _ g₁⁻¹ (g₁ • v) (g₂ • v)).mp
+        (by rwa [inv_smul_smul])
+      exact this
+    · intro h
+      have := (@GraphAction.adj_smul_iff G V _ _ Γ _ g₁⁻¹ (g₁ • v) (g₂ • v)).mpr h
+      rwa [inv_smul_smul] at this
+
+end SabidussiRepresentation

From f3269af1a17e7cbe079977a1eb1bf1d922d1d9e4 Mon Sep 17 00:00:00 2001
From: Robin Langer <langer.robin@gmail.com>
Date: Tue, 19 May 2026 06:16:10 +1000
Subject: [PATCH 05/14] feat(Combinatorics/SimpleGraph): Lorimer's theorem and
 quotient graphs

---
 Mathlib.lean                                  |   2 +
 .../SimpleGraph/QuotientGraph.lean            | 134 ++++++++++++
 .../Combinatorics/SimpleGraph/Symmetric.lean  | 195 ++++++++++++++++++
 3 files changed, 331 insertions(+)
 create mode 100644 Mathlib/Combinatorics/SimpleGraph/QuotientGraph.lean
 create mode 100644 Mathlib/Combinatorics/SimpleGraph/Symmetric.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 4bcf38b25f4bdb..100ccd502ff9dd 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -3621,6 +3621,7 @@ public import Mathlib.Combinatorics.SimpleGraph.Operations
 public import Mathlib.Combinatorics.SimpleGraph.Partition
 public import Mathlib.Combinatorics.SimpleGraph.Paths
 public import Mathlib.Combinatorics.SimpleGraph.Prod
+public import Mathlib.Combinatorics.SimpleGraph.QuotientGraph
 public import Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
 public import Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
 public import Mathlib.Combinatorics.SimpleGraph.Regularity.Energy
@@ -3632,6 +3633,7 @@ public import Mathlib.Combinatorics.SimpleGraph.Representation
 public import Mathlib.Combinatorics.SimpleGraph.StronglyRegular
 public import Mathlib.Combinatorics.SimpleGraph.Subgraph
 public import Mathlib.Combinatorics.SimpleGraph.Sum
+public import Mathlib.Combinatorics.SimpleGraph.Symmetric
 public import Mathlib.Combinatorics.SimpleGraph.Trails
 public import Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
 public import Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
diff --git a/Mathlib/Combinatorics/SimpleGraph/QuotientGraph.lean b/Mathlib/Combinatorics/SimpleGraph/QuotientGraph.lean
new file mode 100644
index 00000000000000..420b6dffab698e
--- /dev/null
+++ b/Mathlib/Combinatorics/SimpleGraph/QuotientGraph.lean
@@ -0,0 +1,134 @@
+/-
+Copyright (c) 2026 Robin Langer. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Robin Langer
+-/
+module
+
+public import Mathlib.Combinatorics.SimpleGraph.Symmetric
+public import Mathlib.GroupTheory.GroupAction.Blocks
+
+/-!
+# Quotient graphs and the Lorimer quotient theorem
+
+The quotient of a symmetric graph `Sab(G, H, HaH)` by a `G`-invariant partition
+is again a symmetric graph `Sab(G, K, KaK)` for some overgroup `H ≤ K ≤ G`.
+
+## Main definitions
+
+* `SimpleGraph.quotientGraph` — quotient of a graph by a surjection (partition)
+* `cosetQuotientMap` — the natural map `G ⧸ H → G ⧸ K` for `H ≤ K`
+* `expandConnectionSet` — the expanded connection set `KDK` for an overgroup `K`
+
+## Main results
+
+* `quotient_cosetGraph_iso` — the quotient of `Sab(G,H,D)` is isomorphic to `Sab(G,K,KDK)`
+
+## References
+
+* Robin Langer, *Symmetric Graphs and their Quotients*, arXiv:1306.4798, Chapter 2 §4.
+-/
+
+@[expose] public section
+
+variable {G : Type*} [Group G]
+
+/-! ### Quotient graph construction -/
+
+/-- The **quotient graph** of `Γ` with respect to a surjection `π : V → ι`. -/
+def SimpleGraph.quotientGraph {V ι : Type*} (Γ : SimpleGraph V) (π : V → ι) :
+    SimpleGraph ι where
+  Adj i j := i ≠ j ∧ ∃ u v : V, π u = i ∧ π v = j ∧ Γ.Adj u v
+  symm := by
+    intro i j ⟨hne, u, v, hui, hvj, hadj⟩
+    exact ⟨hne.symm, v, u, hvj, hui, Γ.symm hadj⟩
+  loopless := ⟨fun i ⟨hne, _⟩ => hne rfl⟩
+
+/-! ### The coset quotient map -/
+
+/-- The natural map `G ⧸ H → G ⧸ K` for `H ≤ K`, sending `gH ↦ gK`. -/
+noncomputable def cosetQuotientMap (H K : Subgroup G) (hHK : H ≤ K) :
+    G ⧸ H → G ⧸ K :=
+  Quotient.map' id (fun _ _ h => QuotientGroup.leftRel_apply.mpr
+    (hHK (QuotientGroup.leftRel_apply.mp h)))
+
+@[simp]
+theorem cosetQuotientMap_mk (H K : Subgroup G) (hHK : H ≤ K) (g : G) :
+    cosetQuotientMap H K hHK (QuotientGroup.mk g) = QuotientGroup.mk g :=
+  rfl
+
+/-! ### Expanded connection set KDK -/
+
+/-- The expanded connection set `KDK` for an overgroup `K`. -/
+def expandConnectionSet (K : Subgroup G) (D : Set G) : Set G :=
+  {g : G | ∃ k₁ ∈ (K : Set G), ∃ d ∈ D, ∃ k₂ ∈ (K : Set G), g = k₁ * d * k₂}
+
+/-- `KDK` is a valid connection set for `K` when `D ∩ K = ∅`. -/
+theorem expandConnectionSet_isConnectionSet (H K : Subgroup G) (D : Set G)
+    (hD : IsConnectionSet H D) (hDK : Disjoint D ↑K) :
+    IsConnectionSet K (expandConnectionSet K D) where
+  double_coset_stable := by
+    intro d hd m₁ hm₁ m₂ hm₂
+    obtain ⟨k₁, hk₁, e, he, k₂, hk₂, rfl⟩ := hd
+    exact ⟨m₁ * k₁, K.mul_mem hm₁ hk₁, e, he, k₂ * m₂, K.mul_mem hk₂ hm₂, by group⟩
+  inv_mem := by
+    intro d hd
+    obtain ⟨k₁, hk₁, e, he, k₂, hk₂, rfl⟩ := hd
+    exact ⟨k₂⁻¹, K.inv_mem hk₂, e⁻¹, hD.inv_mem e he, k₁⁻¹, K.inv_mem hk₁, by group⟩
+  disjoint := by
+    rw [Set.disjoint_left]
+    intro g hg hgK
+    obtain ⟨k₁, hk₁, d, hd, k₂, hk₂, rfl⟩ := hg
+    have : d ∈ (K : Set G) := by
+      have := K.mul_mem (K.mul_mem (K.inv_mem hk₁) hgK) (K.inv_mem hk₂)
+      convert this using 1; group
+    exact Set.disjoint_left.mp hDK hd this
+
+/-! ### The Lorimer quotient theorem -/
+
+/-- **Lorimer's Quotient Theorem**: The quotient of `Sab(G, H, D)` by the overgroup
+`K ≥ H` (with `D ∩ K = ∅`) is isomorphic to `Sab(G, K, KDK)`.
+
+The quotient map `G ⧸ H → G ⧸ K` (sending `gH ↦ gK`) induces a graph
+isomorphism from the quotient graph to the coset graph with expanded
+connection set. -/
+noncomputable def quotient_cosetGraph_iso (H K : Subgroup G) (D : Set G)
+    (hD : IsConnectionSet H D) (hHK : H ≤ K)
+    (hDK : Disjoint D ↑K) :
+    SimpleGraph.quotientGraph (SimpleGraph.cosetGraph H D hD) (cosetQuotientMap H K hHK) ≃g
+      SimpleGraph.cosetGraph K (expandConnectionSet K D)
+        (expandConnectionSet_isConnectionSet H K D hD hDK) where
+  toEquiv := Equiv.refl _
+  map_rel_iff' := by
+    intro q₁ q₂
+    refine Quotient.inductionOn₂ q₁ q₂ fun x y => ?_
+    simp only [Equiv.refl_apply]
+    rw [SimpleGraph.cosetGraph.adj_mk]
+    constructor
+    · intro ⟨k₁, hk₁, d, hd, k₂, hk₂, heq⟩
+      refine ⟨?_, QuotientGroup.mk (x * k₁),
+             QuotientGroup.mk (x * k₁ * d), ?_, ?_, ?_⟩
+      · intro heq'
+        have : d ∈ (K : Set G) := by
+          have hK : k₁ * d * k₂ ∈ (K : Set G) := heq ▸ QuotientGroup.eq.mp heq'
+          have := K.mul_mem (K.mul_mem (K.inv_mem hk₁) hK) (K.inv_mem hk₂)
+          convert this using 1; group
+        exact Set.disjoint_left.mp hDK hd this
+      · simp only [cosetQuotientMap_mk, QuotientGroup.eq]
+        have : (x * k₁)⁻¹ * x = k₁⁻¹ := by group
+        rw [this]; exact K.inv_mem hk₁
+      · simp only [cosetQuotientMap_mk, QuotientGroup.eq]
+        have hy : y = x * (k₁ * d * k₂) := by rw [← heq]; group
+        have : (x * k₁ * d)⁻¹ * (x * (k₁ * d * k₂)) = k₂ := by group
+        rw [hy, this]; exact hk₂
+      · convert hd using 1
+        simp [mul_inv_rev, mul_assoc, inv_mul_cancel_left]
+    · intro ⟨_, u, v, hu, hv, hadj⟩
+      revert hu hv hadj
+      refine Quotient.inductionOn₂ u v fun x' y' hx' hy' (hadj : x'⁻¹ * y' ∈ D) => ?_
+      simp only [cosetQuotientMap_mk] at hx' hy'
+      have hxK : x⁻¹ * x' ∈ (K : Set G) := by
+        have := K.inv_mem (QuotientGroup.eq.mp hx' : x'⁻¹ * x ∈ K)
+        rwa [mul_inv_rev, inv_inv] at this
+      have hyK : y'⁻¹ * y ∈ (K : Set G) := QuotientGroup.eq.mp hy'
+      exact ⟨x⁻¹ * x', hxK, x'⁻¹ * y', hadj, y'⁻¹ * y, hyK, by group⟩
diff --git a/Mathlib/Combinatorics/SimpleGraph/Symmetric.lean b/Mathlib/Combinatorics/SimpleGraph/Symmetric.lean
new file mode 100644
index 00000000000000..d39246b2bf7bf2
--- /dev/null
+++ b/Mathlib/Combinatorics/SimpleGraph/Symmetric.lean
@@ -0,0 +1,195 @@
+/-
+Copyright (c) 2026 Robin Langer. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Robin Langer
+-/
+module
+
+public import Mathlib.Combinatorics.SimpleGraph.Representation
+public import Mathlib.GroupTheory.DoubleCoset
+public import Mathlib.Tactic.Group
+
+/-!
+# Symmetric graphs and Lorimer's theorem
+
+A *symmetric* (arc-transitive) graph is a coset graph `Sab(G, H, HaH)` where `a` is an
+involution not in `H`. This file proves both directions of Lorimer's theorem:
+the forward direction shows `Sab(G, H, HaH)` is arc-transitive when `a² = 1` and `a ∉ H`,
+and the reverse direction shows every arc-transitive graph's connection set is a single
+double coset `HaH` where `a` swaps an arc.
+
+## Main definitions
+
+* `doubleCoset_isConnectionSet` — `HaH` is a valid connection set when `a² = 1, a ∉ H`
+* `sabidussiSymmetricGraph` — the coset graph `Sab(G, H, HaH)`
+
+## Main results
+
+* `lorimer_forward` — `Sab(G, H, HaH)` is arc-transitive when `a² = 1, a ∉ H`
+* `connectionSet_eq_doubleCoset` — under arc-transitivity, the connection set is a single
+  double coset
+* `lorimer_reverse` — every arc-transitive graph has an arc-swapping involution `a` with
+  `a ∉ Gᵥ`, `a² ∈ Gᵥ`, and `D = GᵥaGᵥ`
+
+## References
+
+* Robin Langer, *Symmetric Graphs and their Quotients*, arXiv:1306.4798, Chapter 2 §§3–4.
+* Lorimer, *Vertex-transitive graphs*, 1984.
+-/
+
+@[expose] public section
+
+variable {G : Type*} [Group G]
+
+private theorem inv_eq_self_of_sq_eq_one {a : G} (ha : a ^ 2 = 1) : a⁻¹ = a :=
+  inv_eq_of_mul_eq_one_left (by rwa [← sq])
+
+open DoubleCoset in
+/-- `HaH` is a valid connection set when `a² = 1` and `a ∉ H`. -/
+theorem doubleCoset_isConnectionSet (H : Subgroup G) (a : G)
+    (ha_sq : a ^ 2 = 1) (ha_not : a ∉ H) :
+    IsConnectionSet H (doubleCoset a (H : Set G) H) where
+  double_coset_stable := by
+    intro d hd k₁ hk₁ k₂ hk₂
+    obtain ⟨h₁, hh₁, h₂, hh₂, rfl⟩ := mem_doubleCoset.mp hd
+    exact mem_doubleCoset.mpr
+      ⟨k₁ * h₁, H.mul_mem hk₁ hh₁, h₂ * k₂, H.mul_mem hh₂ hk₂, by group⟩
+  inv_mem := by
+    intro d hd
+    obtain ⟨h₁, hh₁, h₂, hh₂, rfl⟩ := mem_doubleCoset.mp hd
+    have ha_inv := inv_eq_self_of_sq_eq_one ha_sq
+    refine mem_doubleCoset.mpr ⟨h₂⁻¹, H.inv_mem hh₂, h₁⁻¹, H.inv_mem hh₁, ?_⟩
+    calc (h₁ * a * h₂)⁻¹ = h₂⁻¹ * a⁻¹ * h₁⁻¹ := by group
+      _ = h₂⁻¹ * a * h₁⁻¹ := by rw [ha_inv]
+  disjoint := by
+    rw [Set.disjoint_left]
+    intro g hg hgH
+    obtain ⟨h₁, hh₁, h₂, hh₂, rfl⟩ := mem_doubleCoset.mp hg
+    have : a = h₁⁻¹ * (h₁ * a * h₂) * h₂⁻¹ := by group
+    rw [this] at ha_not
+    exact ha_not (H.mul_mem (H.mul_mem (H.inv_mem hh₁) hgH) (H.inv_mem hh₂))
+
+section Lorimer
+
+variable (H : Subgroup G) (a : G) (ha_sq : a ^ 2 = 1) (ha_not : a ∉ H)
+
+noncomputable abbrev sabidussiSymmetricGraph :=
+  SimpleGraph.cosetGraph H (DoubleCoset.doubleCoset a (H : Set G) H)
+    (doubleCoset_isConnectionSet H a ha_sq ha_not)
+
+/-- Local transitivity at the identity coset. -/
+private theorem locallyTransitive_at_one :
+    IsLocallyTransitive G (G ⧸ H) (sabidussiSymmetricGraph H a ha_sq ha_not)
+      ((1 : G) : G ⧸ H) := by
+  intro w₁ w₂ hw₁ hw₂
+  revert hw₁ hw₂
+  refine Quotient.inductionOn₂ w₁ w₂ fun y₁ y₂ hy₁ hy₂ => ?_
+  change (1 : G)⁻¹ * y₁ ∈ _ at hy₁; change (1 : G)⁻¹ * y₂ ∈ _ at hy₂
+  simp only [inv_one, one_mul] at hy₁ hy₂
+  obtain ⟨h₁, hh₁, k₁, hk₁, rfl⟩ := DoubleCoset.mem_doubleCoset.mp hy₁
+  obtain ⟨h₂, hh₂, k₂, hk₂, rfl⟩ := DoubleCoset.mem_doubleCoset.mp hy₂
+  refine ⟨h₂ * h₁⁻¹, ?_, ?_⟩
+  · change (h₂ * h₁⁻¹) • ((1 : G) : G ⧸ H) = (1 : G)
+    rw [MulAction.Quotient.smul_coe, smul_eq_mul, mul_one]
+    apply QuotientGroup.eq.mpr
+    show (h₂ * h₁⁻¹)⁻¹ * 1 ∈ H
+    simp only [mul_one, mul_inv_rev, inv_inv]
+    exact H.mul_mem hh₁ (H.inv_mem hh₂)
+  · change (h₂ * h₁⁻¹) • ((h₁ * a * k₁ : G) : G ⧸ H) = (h₂ * a * k₂ : G)
+    rw [MulAction.Quotient.smul_coe, smul_eq_mul, QuotientGroup.eq]
+    have ha_inv := inv_eq_self_of_sq_eq_one ha_sq
+    suffices h : (h₂ * h₁⁻¹ * (h₁ * a * k₁))⁻¹ * (h₂ * a * k₂) = k₁⁻¹ * k₂ by
+      rw [h]; exact H.mul_mem (H.inv_mem hk₁) hk₂
+    calc (h₂ * h₁⁻¹ * (h₁ * a * k₁))⁻¹ * (h₂ * a * k₂)
+        = (h₂ * a * k₁)⁻¹ * (h₂ * a * k₂) := by congr 1; group
+      _ = k₁⁻¹ * a⁻¹ * (h₂⁻¹ * (h₂ * a * k₂)) := by group
+      _ = k₁⁻¹ * a⁻¹ * (a * k₂) := by rw [show h₂⁻¹ * (h₂ * a * k₂) = a * k₂ from by group]
+      _ = k₁⁻¹ * (a⁻¹ * a) * k₂ := by group
+      _ = k₁⁻¹ * k₂ := by rw [ha_inv]; simp [← sq, ha_sq]
+
+/-- Local transitivity at any vertex, transported from `⟦1⟧`. -/
+private theorem locallyTransitive_everywhere :
+    ∀ q : G ⧸ H,
+      IsLocallyTransitive G (G ⧸ H) (sabidussiSymmetricGraph H a ha_sq ha_not) q := by
+  intro q w₁ w₂ hw₁ hw₂
+  set Γ := sabidussiSymmetricGraph H a ha_sq ha_not
+  obtain ⟨g, hg⟩ := MulAction.exists_smul_eq G ((1 : G) : G ⧸ H) q
+  have hw₁' : Γ.Adj ((1 : G) : G ⧸ H) (g⁻¹ • w₁) := by
+    have := (@GraphAction.adj_smul_iff G _ _ _ Γ _ g⁻¹ q w₁).mpr hw₁
+    rwa [← hg, inv_smul_smul] at this
+  have hw₂' : Γ.Adj ((1 : G) : G ⧸ H) (g⁻¹ • w₂) := by
+    have := (@GraphAction.adj_smul_iff G _ _ _ Γ _ g⁻¹ q w₂).mpr hw₂
+    rwa [← hg, inv_smul_smul] at this
+  obtain ⟨h, hfix, hsend⟩ :=
+    locallyTransitive_at_one H a ha_sq ha_not (g⁻¹ • w₁) (g⁻¹ • w₂) hw₁' hw₂'
+  refine ⟨g * h * g⁻¹, ?_, ?_⟩
+  · calc (g * h * g⁻¹) • q = g • (h • (g⁻¹ • q)) := by simp [mul_smul]
+      _ = g • (h • ((1 : G) : G ⧸ H)) := by rw [← hg, inv_smul_smul]
+      _ = g • ((1 : G) : G ⧸ H) := by rw [hfix]
+      _ = q := hg
+  · calc (g * h * g⁻¹) • w₁ = g • (h • (g⁻¹ • w₁)) := by simp [mul_smul]
+      _ = g • (g⁻¹ • w₂) := by rw [hsend]
+      _ = w₂ := smul_inv_smul g w₂
+
+/-- **Lorimer's Theorem (forward direction)**: `Sab(G, H, HaH)` is arc-transitive
+when `a² = 1` and `a ∉ H`. -/
+theorem lorimer_forward :
+    IsArcTransitive G (G ⧸ H) (sabidussiSymmetricGraph H a ha_sq ha_not) :=
+  isArcTransitive_of_vertexTransitive_locallyTransitive _
+    (locallyTransitive_everywhere H a ha_sq ha_not)
+
+end Lorimer
+
+/-! ### Lorimer's theorem (reverse direction) -/
+
+/-- Under arc-transitivity, the stabilizer acts transitively on neighbors. -/
+theorem stabilizer_transitive_on_neighbors {V : Type*} [MulAction G V]
+    (Γ : SimpleGraph V) [IsArcTransitive G V Γ]
+    (v : V) {w u : V} (hw : Γ.Adj v w) (hu : Γ.Adj v u) :
+    ∃ h ∈ MulAction.stabilizer G v, h • w = u := by
+  obtain ⟨g, hgv, hgw⟩ := @IsArcTransitive.arc_transitive G V _ _ Γ _ v w v u hw hu
+  exact ⟨g, MulAction.mem_stabilizer_iff.mpr hgv, hgw⟩
+
+/-- Under arc-transitivity, the connection set is a single double coset `HaH`. -/
+theorem connectionSet_eq_doubleCoset {V : Type*} [MulAction G V]
+    (Γ : SimpleGraph V) [IsArcTransitive G V Γ]
+    (v : V) {a : G} (ha : a ∈ connectionSet G Γ v) :
+    connectionSet G Γ v =
+      DoubleCoset.doubleCoset a (MulAction.stabilizer G v : Set G)
+        (MulAction.stabilizer G v) := by
+  ext g
+  constructor
+  · intro hg
+    obtain ⟨h, hh, hhw⟩ := @stabilizer_transitive_on_neighbors G _ V _ Γ _ v _ _ ha hg
+    rw [DoubleCoset.mem_doubleCoset]
+    exact ⟨h, hh, (g⁻¹ * (h * a))⁻¹,
+      (MulAction.stabilizer G v).inv_mem (by
+        rw [MulAction.mem_stabilizer_iff, mul_smul, mul_smul, hhw, inv_smul_smul]),
+      by group⟩
+  · intro hg
+    obtain ⟨h₁, hh₁, h₂, hh₂, rfl⟩ := DoubleCoset.mem_doubleCoset.mp hg
+    exact connectionSet.double_coset_stable v ha hh₁ hh₂
+
+/-- **Lorimer's Theorem (reverse direction)**: Every arc-transitive graph's connection
+set is a single `(H,H)`-double coset, determined by the arc-swapping element.
+
+Combined with `sabidussiIso`, this shows every arc-transitive graph
+is `Sab(G, stabilizer G v, HaH)` where `a` swaps an arc `(v,w)`. -/
+theorem lorimer_reverse {V : Type*} [MulAction G V]
+    (Γ : SimpleGraph V) [IsArcTransitive G V Γ]
+    (v w : V) (hvw : Γ.Adj v w) :
+    ∃ a : G, a • v = w ∧ a • w = v ∧ a ∉ MulAction.stabilizer G v ∧
+      a ^ 2 ∈ MulAction.stabilizer G v ∧
+      connectionSet G Γ v =
+        DoubleCoset.doubleCoset a (MulAction.stabilizer G v : Set G)
+          (MulAction.stabilizer G v) := by
+  obtain ⟨a, hav, haw⟩ :=
+    @IsArcTransitive.arc_transitive G V _ _ Γ _ v w w v hvw (Γ.symm hvw)
+  refine ⟨a, hav, haw, ?_, ?_, ?_⟩
+  · intro hmem
+    rw [MulAction.mem_stabilizer_iff] at hmem
+    rw [hmem] at hav
+    exact Γ.loopless.irrefl v (hav ▸ hvw)
+  · rw [MulAction.mem_stabilizer_iff, sq, mul_smul, hav, haw]
+  · exact connectionSet_eq_doubleCoset Γ v (by
+      simp only [connectionSet, Set.mem_setOf_eq, hav]; exact hvw)

From b4614a0982a897547bb1130929fe1b109a9d4a50 Mon Sep 17 00:00:00 2001
From: Robin Langer <langer.robin@gmail.com>
Date: Tue, 19 May 2026 06:21:39 +1000
Subject: [PATCH 06/14] fix: drop unused GraphAction from connectionSet, add
 omit annotations

---
 Mathlib/Combinatorics/SimpleGraph/Representation.lean | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Combinatorics/SimpleGraph/Representation.lean b/Mathlib/Combinatorics/SimpleGraph/Representation.lean
index 020db8d31abfb8..b1faf6b2f9bd21 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Representation.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Representation.lean
@@ -36,16 +36,17 @@ variable {G V : Type*} [Group G] [MulAction G V] {Γ : SimpleGraph V}
 
 /-! ### The connection set -/
 
-/-- The *connection set* of a basepoint `v` in a graph action: the set of group elements
+/-- The *connection set* of a basepoint `v`: the set of group elements
 that move `v` to one of its neighbors. -/
 def connectionSet (G : Type*) [Group G] [MulAction G V]
-    (Γ : SimpleGraph V) [GraphAction G V Γ] (v : V) : Set G :=
+    (Γ : SimpleGraph V) (v : V) : Set G :=
   {g : G | Γ.Adj v (g • v)}
 
 namespace connectionSet
 
 variable [GraphAction G V Γ] (v : V)
 
+omit [GraphAction G V Γ] in
 theorem one_not_mem : (1 : G) ∉ connectionSet G Γ v := by
   simp [connectionSet]
 
@@ -64,6 +65,7 @@ theorem double_coset_stable {g : G} (hg : g ∈ connectionSet G Γ v)
   have := GraphAction.adj_smul h₁ v (g • v) hg
   rwa [MulAction.mem_stabilizer_iff.mp hh₁] at this
 
+omit [GraphAction G V Γ] in
 theorem disjoint_stabilizer :
     Disjoint (connectionSet G Γ v) ↑(MulAction.stabilizer G v) := by
   rw [Set.disjoint_left]

From 1510488e02333555a137df65ad963566f649d0de Mon Sep 17 00:00:00 2001
From: Robin Langer <langer.robin@gmail.com>
Date: Tue, 19 May 2026 06:42:28 +1000
Subject: [PATCH 07/14] doc: add docstring to sabidussiSymmetricGraph

---
 Mathlib/Combinatorics/SimpleGraph/Symmetric.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib/Combinatorics/SimpleGraph/Symmetric.lean b/Mathlib/Combinatorics/SimpleGraph/Symmetric.lean
index d39246b2bf7bf2..396baa0b54a598 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Symmetric.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Symmetric.lean
@@ -73,6 +73,7 @@ section Lorimer
 
 variable (H : Subgroup G) (a : G) (ha_sq : a ^ 2 = 1) (ha_not : a ∉ H)
 
+/-- The coset graph `Sab(G, H, HaH)` for an involution `a ∉ H`. -/
 noncomputable abbrev sabidussiSymmetricGraph :=
   SimpleGraph.cosetGraph H (DoubleCoset.doubleCoset a (H : Set G) H)
     (doubleCoset_isConnectionSet H a ha_sq ha_not)

From b1df4dc13d4fa9f377c1d2e8e71409270416e5e8 Mon Sep 17 00:00:00 2001
From: Robin Langer <langer.robin@gmail.com>
Date: Thu, 21 May 2026 19:23:41 +1000
Subject: [PATCH 08/14] feat(Archive): dodecahedron, Petersen graph, 3-cube,
 and antipodal quotients
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Defines the dodecahedron (Fin 20), Petersen graph (Fin 10), 3-cube Q₃
(Fin 8), and their antipodal quotient relationships. The Petersen graph
is the quotient of the dodecahedron by the antipodal involution. The
quotient of the 3-cube by bitwise complement is K₄.
---
 Archive.lean             |   1 +
 Archive/NamedGraphs.lean | 149 +++++++++++++++++++++++++++++++++++++++
 2 files changed, 150 insertions(+)
 create mode 100644 Archive/NamedGraphs.lean

diff --git a/Archive.lean b/Archive.lean
index 8ca03e8bc806d9..ba164d9fec8608 100644
--- a/Archive.lean
+++ b/Archive.lean
@@ -62,6 +62,7 @@ import Archive.Imo.Imo2024Q6
 import Archive.Imo.Imo2025Q3
 import Archive.Kuratowski
 import Archive.MinimalSheffer
+import Archive.NamedGraphs
 import Archive.MiuLanguage.Basic
 import Archive.MiuLanguage.DecisionNec
 import Archive.MiuLanguage.DecisionSuf
diff --git a/Archive/NamedGraphs.lean b/Archive/NamedGraphs.lean
new file mode 100644
index 00000000000000..328e6a36d72021
--- /dev/null
+++ b/Archive/NamedGraphs.lean
@@ -0,0 +1,149 @@
+/-
+Copyright (c) 2026 Robin Langer. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Robin Langer
+-/
+import Mathlib.Combinatorics.SimpleGraph.QuotientGraph
+
+/-!
+# Named graphs and antipodal quotients
+
+The dodecahedron has an antipodal involution (distance 5) whose quotient is the
+Petersen graph. The 3-cube has an antipodal involution (bitwise complement, distance 3)
+whose quotient is K₄.
+
+## Main definitions
+
+* `dodecahedronGraph` — the dodecahedron on `Fin 20`, 3-regular, 30 edges
+* `petersenGraph` — the Petersen graph on `Fin 10`, as `dodecahedronGraph.quotientGraph`
+* `cubeGraph` — the 3-cube Q₃ on `Fin 8`, 3-regular, 12 edges
+
+## Main results
+
+* `dodecahedronGraph_regular` — the dodecahedron is 3-regular
+* `petersenGraph_regular` — the Petersen graph is 3-regular
+* `cubeQuotient_eq_top` — the antipodal quotient of the cube is K₄
+
+## References
+
+* Robin Langer, *Symmetric Graphs and their Quotients*, arXiv:1306.4798
+-/
+
+set_option linter.style.nativeDecide false
+
+open SimpleGraph
+
+/-! ### The dodecahedron graph -/
+
+private def dodecAdjBool (u v : Fin 20) : Bool :=
+  let edges : List (Fin 20 × Fin 20) := [
+    (0, 1), (0, 4), (0, 5), (1, 2), (1, 7), (2, 3), (2, 9), (3, 4), (3, 11), (4, 13),
+    (5, 6), (5, 14), (6, 7), (6, 15), (7, 8), (8, 9), (8, 16), (9, 10), (10, 11), (10, 17),
+    (11, 12), (12, 13), (12, 18), (13, 14), (14, 19), (15, 16), (15, 19), (16, 17), (17, 18),
+    (18, 19)]
+  edges.any fun (a, b) => (u == a && v == b) || (u == b && v == a)
+
+/-- The **dodecahedron graph**, the 1-skeleton of the regular dodecahedron. -/
+def dodecahedronGraph : SimpleGraph (Fin 20) where
+  Adj u v := dodecAdjBool u v
+  symm u v := by simp only [dodecAdjBool]; revert u v; native_decide
+  loopless := ⟨fun u => by simp only [dodecAdjBool]; revert u; native_decide⟩
+
+instance : DecidableRel dodecahedronGraph.Adj :=
+  fun u v => inferInstanceAs (Decidable (dodecAdjBool u v))
+
+/-! ### The antipodal quotient map -/
+
+private def dodecAntipodalData : List (Fin 10) :=
+  [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 5, 6, 7, 8, 9, 3, 4, 0, 1, 2]
+
+private theorem dodecAntipodalData_length : dodecAntipodalData.length = 20 := by native_decide
+
+/-- The antipodal quotient map: `Fin 20 → Fin 10`. -/
+def dodecAntipodalMap (v : Fin 20) : Fin 10 :=
+  dodecAntipodalData.get (v.cast dodecAntipodalData_length.symm)
+
+/-! ### The Petersen graph -/
+
+/-- The **Petersen graph**, the antipodal quotient of the dodecahedron. -/
+def petersenGraph : SimpleGraph (Fin 10) :=
+  dodecahedronGraph.quotientGraph dodecAntipodalMap
+
+instance : DecidableRel petersenGraph.Adj := by
+  intro i j; unfold petersenGraph quotientGraph; simp only; exact instDecidableAnd
+
+/-- The dodecahedron is 3-regular. -/
+theorem dodecahedronGraph_regular :
+    ∀ v : Fin 20, (Finset.univ.filter fun w => dodecahedronGraph.Adj v w).card = 3 := by
+  native_decide
+
+/-- The dodecahedron has 30 edges. -/
+theorem dodecahedronGraph_edgeCount :
+    (Finset.univ.filter fun p : Fin 20 × Fin 20 =>
+      p.1 < p.2 ∧ dodecahedronGraph.Adj p.1 p.2).card = 30 := by
+  native_decide
+
+/-- The Petersen graph is 3-regular. -/
+theorem petersenGraph_regular :
+    ∀ v : Fin 10, (Finset.univ.filter fun w => petersenGraph.Adj v w).card = 3 := by
+  native_decide
+
+/-- The Petersen graph has 15 edges. -/
+theorem petersenGraph_edgeCount :
+    (Finset.univ.filter fun p : Fin 10 × Fin 10 =>
+      p.1 < p.2 ∧ petersenGraph.Adj p.1 p.2).card = 15 := by
+  native_decide
+
+/-! ### The 3-cube graph -/
+
+private def cubeAdjBool (u v : Fin 8) : Bool :=
+  let edges : List (Fin 8 × Fin 8) := [
+    (0, 1), (0, 2), (0, 4), (1, 3), (1, 5), (2, 3), (2, 6), (3, 7),
+    (4, 5), (4, 6), (5, 7), (6, 7)]
+  edges.any fun (a, b) => (u == a && v == b) || (u == b && v == a)
+
+/-- The **3-cube graph** Q₃, the 1-skeleton of the 3-dimensional hypercube. -/
+def cubeGraph : SimpleGraph (Fin 8) where
+  Adj u v := cubeAdjBool u v
+  symm u v := by simp only [cubeAdjBool]; revert u v; native_decide
+  loopless := ⟨fun u => by simp only [cubeAdjBool]; revert u; native_decide⟩
+
+instance : DecidableRel cubeGraph.Adj :=
+  fun u v => inferInstanceAs (Decidable (cubeAdjBool u v))
+
+/-! ### The cube antipodal quotient -/
+
+private def cubeAntipodalData : List (Fin 4) := [0, 1, 2, 3, 3, 2, 1, 0]
+
+private theorem cubeAntipodalData_length : cubeAntipodalData.length = 8 := by native_decide
+
+/-- The antipodal quotient map on Q₃: `Fin 8 → Fin 4`. -/
+def cubeAntipodalMap (v : Fin 8) : Fin 4 :=
+  cubeAntipodalData.get (v.cast cubeAntipodalData_length.symm)
+
+/-- The antipodal quotient of the 3-cube. -/
+def cubeQuotientGraph : SimpleGraph (Fin 4) :=
+  cubeGraph.quotientGraph cubeAntipodalMap
+
+instance : DecidableRel cubeQuotientGraph.Adj := by
+  intro i j; unfold cubeQuotientGraph quotientGraph; simp only; exact instDecidableAnd
+
+/-- The 3-cube is 3-regular. -/
+theorem cubeGraph_regular :
+    ∀ v : Fin 8, (Finset.univ.filter fun w => cubeGraph.Adj v w).card = 3 := by
+  native_decide
+
+/-- The 3-cube has 12 edges. -/
+theorem cubeGraph_edgeCount :
+    (Finset.univ.filter fun p : Fin 8 × Fin 8 =>
+      p.1 < p.2 ∧ cubeGraph.Adj p.1 p.2).card = 12 := by
+  native_decide
+
+/-- The antipodal quotient of the 3-cube is 3-regular. -/
+theorem cubeQuotientGraph_regular :
+    ∀ v : Fin 4, (Finset.univ.filter fun w => cubeQuotientGraph.Adj v w).card = 3 := by
+  native_decide
+
+/-- The antipodal quotient of the 3-cube is the complete graph K₄. -/
+theorem cubeQuotient_eq_top : cubeQuotientGraph = ⊤ := by
+  ext u v; revert u v; native_decide

From 96a7299f3780f9fd43ec4aa72796108d063a2ef5 Mon Sep 17 00:00:00 2001
From: Robin Langer <langer.robin@gmail.com>
Date: Thu, 21 May 2026 21:55:42 +1000
Subject: [PATCH 09/14] chore: fix Archive.lean import ordering for NamedGraphs

Move `import Archive.NamedGraphs` after `MiuLanguage` entries
to match the alphabetical ordering expected by `lake exe mk_all`.
---
 Archive.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Archive.lean b/Archive.lean
index ba164d9fec8608..33ef3d47c64494 100644
--- a/Archive.lean
+++ b/Archive.lean
@@ -62,10 +62,10 @@ import Archive.Imo.Imo2024Q6
 import Archive.Imo.Imo2025Q3
 import Archive.Kuratowski
 import Archive.MinimalSheffer
-import Archive.NamedGraphs
 import Archive.MiuLanguage.Basic
 import Archive.MiuLanguage.DecisionNec
 import Archive.MiuLanguage.DecisionSuf
+import Archive.NamedGraphs
 import Archive.OxfordInvariants.Summer2021.Week3P1
 import Archive.Sensitivity
 import Archive.Wiedijk100Theorems.AbelRuffini

From c5aed2d4069087818cb9d094a8bf0d6857b8eee3 Mon Sep 17 00:00:00 2001
From: Robin Langer <langer.robin@gmail.com>
Date: Fri, 22 May 2026 09:18:21 +1000
Subject: [PATCH 10/14] feat(Archive): dodecahedron and cube are Sabidussi
 coset graphs
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Add dodecahedronSabidussiIso and cubeSabidussiIso: both graphs are
proved isomorphic to coset graphs via the Sabidussi representation
theorem.

- Dodecahedron: Sab(A₅, C₃, D), 20 = 60/3 vertices
- Cube: Sab(S₄, C₃, D), 8 = 24/3 vertices

Generators computed by GAP (GRAPE AutGroupGraph), BFS witness words
verify transitivity. GraphAction proved via closure_induction with
the finiteness argument for inverses.
---
 Archive/NamedGraphs.lean | 140 +++++++++++++++++++++++++++++++++++++++
 1 file changed, 140 insertions(+)

diff --git a/Archive/NamedGraphs.lean b/Archive/NamedGraphs.lean
index 328e6a36d72021..24053e2644088a 100644
--- a/Archive/NamedGraphs.lean
+++ b/Archive/NamedGraphs.lean
@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robin Langer
 -/
 import Mathlib.Combinatorics.SimpleGraph.QuotientGraph
+import Mathlib.Combinatorics.SimpleGraph.Action
+import Mathlib.Combinatorics.SimpleGraph.Representation
 
 /-!
 # Named graphs and antipodal quotients
@@ -147,3 +149,141 @@ theorem cubeQuotientGraph_regular :
 /-- The antipodal quotient of the 3-cube is the complete graph K₄. -/
 theorem cubeQuotient_eq_top : cubeQuotientGraph = ⊤ := by
   ext u v; revert u v; native_decide
+
+/-! ## Sabidussi coset graph representations -/
+
+section WordMachinery
+variable {n k : ℕ}
+private def genOrInv' (gens : Fin k → Equiv.Perm (Fin n)) (i : Fin (2 * k)) :
+    Equiv.Perm (Fin n) :=
+  if h : i.val < k then gens ⟨i.val, h⟩ else (gens ⟨i.val - k, by omega⟩).symm
+private def applyWord' (gens : Fin k → Equiv.Perm (Fin n)) :
+    List (Fin (2 * k)) → Equiv.Perm (Fin n)
+  | [] => Equiv.refl _
+  | i :: rest => (genOrInv' gens i).trans (applyWord' gens rest)
+private theorem genOrInv'_mem (gens : Fin k → Equiv.Perm (Fin n)) (i : Fin (2 * k)) :
+    genOrInv' gens i ∈ Subgroup.closure (Set.range gens) := by
+  unfold genOrInv'; split
+  · exact Subgroup.subset_closure ⟨_, rfl⟩
+  · exact Subgroup.inv_mem _ (Subgroup.subset_closure ⟨_, rfl⟩)
+private theorem applyWord'_mem (gens : Fin k → Equiv.Perm (Fin n))
+    (w : List (Fin (2 * k))) : applyWord' gens w ∈ Subgroup.closure (Set.range gens) := by
+  induction w with
+  | nil => exact Subgroup.one_mem _
+  | cons i rest ih => exact Subgroup.mul_mem _ ih (genOrInv'_mem gens i)
+private theorem closureGraphAction {Γ : SimpleGraph (Fin n)}
+    (gens : Fin k → Equiv.Perm (Fin n))
+    (hadj : ∀ i u v, Γ.Adj u v → Γ.Adj (gens i u) (gens i v))
+    (σ : Equiv.Perm (Fin n)) (hσ : σ ∈ Subgroup.closure (Set.range gens))
+    (u v : Fin n) (h : Γ.Adj u v) : Γ.Adj (σ u) (σ v) := by
+  refine Subgroup.closure_induction
+    (p := fun σ _ => ∀ u v, Γ.Adj u v → Γ.Adj (σ u) (σ v)) ?_ ?_ ?_ ?_ hσ u v h
+  · intro x ⟨i, hi⟩; subst hi; exact hadj i
+  · intro u v h; simpa
+  · intro x y _ _ hx hy u v h; simp only [Equiv.Perm.mul_apply]; exact hx _ _ (hy u v h)
+  · intro x _ hx u v h
+    let f : { p : Fin n × Fin n // Γ.Adj p.1 p.2 } →
+            { p : Fin n × Fin n // Γ.Adj p.1 p.2 } :=
+      fun ⟨⟨a, b⟩, hab⟩ => ⟨⟨x a, x b⟩, hx a b hab⟩
+    have := (Finite.surjective_of_injective (fun ⟨⟨a₁,b₁⟩,_⟩ ⟨⟨a₂,b₂⟩,_⟩ h => by
+      simp only [f,Subtype.mk.injEq,Prod.mk.injEq] at h
+      exact Subtype.ext (Prod.ext (x.injective h.1) (x.injective h.2)))
+      : Function.Surjective f) ⟨⟨u,v⟩,h⟩
+    obtain ⟨⟨⟨a,b⟩,hab⟩,heq⟩ := this
+    simp only [f,Subtype.mk.injEq,Prod.mk.injEq] at heq
+    rw [show a = x⁻¹ u from by rw [← heq.1]; simp,
+        show b = x⁻¹ v from by rw [← heq.2]; simp] at hab; exact hab
+end WordMachinery
+
+section DodecahedronSabidussi
+private def dGen1Fwd : Array (Fin 20) := #[1,2,3,4,0,7,8,9,10,11,12,13,14,5,6,16,17,18,19,15]
+private def dGen1Inv : Array (Fin 20) := #[4,0,1,2,3,13,14,5,6,7,8,9,10,11,12,19,15,16,17,18]
+private def dGen2Fwd : Array (Fin 20) := #[0,4,13,14,5,1,2,3,11,12,18,19,15,6,7,9,10,17,16,8]
+private def dGen2Inv : Array (Fin 20) := #[0,5,6,7,1,4,13,14,19,15,16,8,9,2,3,12,18,17,10,11]
+private theorem dG1F_s : dGen1Fwd.size = 20 := by native_decide
+private theorem dG1I_s : dGen1Inv.size = 20 := by native_decide
+private theorem dG2F_s : dGen2Fwd.size = 20 := by native_decide
+private theorem dG2I_s : dGen2Inv.size = 20 := by native_decide
+private def dG1 : Equiv.Perm (Fin 20) where
+  toFun i := dGen1Fwd[i.val]'(by have := dG1F_s; omega)
+  invFun i := dGen1Inv[i.val]'(by have := dG1I_s; omega)
+  left_inv := by native_decide
+  right_inv := by native_decide
+private def dG2 : Equiv.Perm (Fin 20) where
+  toFun i := dGen2Fwd[i.val]'(by have := dG2F_s; omega)
+  invFun i := dGen2Inv[i.val]'(by have := dG2I_s; omega)
+  left_inv := by native_decide
+  right_inv := by native_decide
+private def dGens : Fin 2 → Equiv.Perm (Fin 20) | 0 => dG1 | 1 => dG2
+private def dGroup : Subgroup (Equiv.Perm (Fin 20)) := Subgroup.closure (Set.range dGens)
+private def dWitData : Array (List (Fin 4)) := #[
+  [],[0],[0,0],[2,2],[2],[0,3],[0,0,3],[0,3,0],[0,0,3,0],[0,3,0,0],
+  [0,0,3,0,0],[0,0,1,2],[2,2,1,2],[0,0,1],[2,2,1],
+  [0,3,0,0,3],[0,0,3,0,0,3],[0,0,1,2,1,2,2],[0,0,1,2,1,2],[0,0,1,2,1]]
+private theorem dWitData_s : dWitData.size = 20 := by native_decide
+private def dWit (v : Fin 20) : List (Fin 4) := dWitData[v.val]'(by have := dWitData_s; omega)
+private theorem dWit_ok : ∀ v : Fin 20, applyWord' dGens (dWit v) 0 = v := by native_decide
+private noncomputable instance : MulAction dGroup (Fin 20) := MulAction.compHom _ dGroup.subtype
+private noncomputable instance : GraphAction dGroup (Fin 20) dodecahedronGraph where
+  adj_smul g u v h := closureGraphAction dGens
+    (fun i => by match i with | 0 => exact (by native_decide) | 1 => exact (by native_decide))
+    g.1 g.2 u v h
+private noncomputable instance : MulAction.IsPretransitive dGroup (Fin 20) where
+  exists_smul_eq x y := ⟨⟨_, dGroup.mul_mem (applyWord'_mem dGens _)
+    (dGroup.inv_mem (applyWord'_mem dGens _))⟩, by
+    show ((applyWord' dGens (dWit x)).symm.trans (applyWord' dGens (dWit y))) x = y
+    simp only [Equiv.trans_apply]
+    rw [show (applyWord' dGens (dWit x)).symm x = 0 from by
+      rw [Equiv.symm_apply_eq]; exact (dWit_ok x).symm]; exact dWit_ok y⟩
+
+/-- **The dodecahedron is a Sabidussi coset graph**: `Sab(A₅, C₃, D)`. -/
+noncomputable def dodecahedronSabidussiIso :
+    dodecahedronGraph ≃g SimpleGraph.cosetGraph (MulAction.stabilizer dGroup (0 : Fin 20))
+      (connectionSet dGroup dodecahedronGraph 0) (connectionSet.isConnectionSet 0) :=
+  sabidussiIso 0
+end DodecahedronSabidussi
+
+section CubeSabidussi
+private def cG1F : Array (Fin 8) := #[2,3,6,7,0,1,4,5]
+private def cG1I : Array (Fin 8) := #[4,5,0,1,6,7,2,3]
+private def cG2F : Array (Fin 8) := #[0,2,4,6,1,3,5,7]
+private def cG2I : Array (Fin 8) := #[0,4,1,5,2,6,3,7]
+private theorem cG1F_s : cG1F.size = 8 := by native_decide
+private theorem cG1I_s : cG1I.size = 8 := by native_decide
+private theorem cG2F_s : cG2F.size = 8 := by native_decide
+private theorem cG2I_s : cG2I.size = 8 := by native_decide
+private def cG1 : Equiv.Perm (Fin 8) where
+  toFun i := cG1F[i.val]'(by have := cG1F_s; omega)
+  invFun i := cG1I[i.val]'(by have := cG1I_s; omega)
+  left_inv := by native_decide
+  right_inv := by native_decide
+private def cG2 : Equiv.Perm (Fin 8) where
+  toFun i := cG2F[i.val]'(by have := cG2F_s; omega)
+  invFun i := cG2I[i.val]'(by have := cG2I_s; omega)
+  left_inv := by native_decide
+  right_inv := by native_decide
+private def cGens : Fin 2 → Equiv.Perm (Fin 8) | 0 => cG1 | 1 => cG2
+private def cGroup : Subgroup (Equiv.Perm (Fin 8)) := Subgroup.closure (Set.range cGens)
+private def cWitData : Array (List (Fin 4)) := #[[],[0,3],[0],[0,0,3],[2],[0,0,1],[0,0],[0,0,1,2]]
+private theorem cWitData_s : cWitData.size = 8 := by native_decide
+private def cWit (v : Fin 8) : List (Fin 4) := cWitData[v.val]'(by have := cWitData_s; omega)
+private theorem cWit_ok : ∀ v : Fin 8, applyWord' cGens (cWit v) 0 = v := by native_decide
+private noncomputable instance : MulAction cGroup (Fin 8) := MulAction.compHom _ cGroup.subtype
+private noncomputable instance : GraphAction cGroup (Fin 8) cubeGraph where
+  adj_smul g u v h := closureGraphAction cGens
+    (fun i => by match i with | 0 => exact (by native_decide) | 1 => exact (by native_decide))
+    g.1 g.2 u v h
+private noncomputable instance : MulAction.IsPretransitive cGroup (Fin 8) where
+  exists_smul_eq x y := ⟨⟨_, cGroup.mul_mem (applyWord'_mem cGens _)
+    (cGroup.inv_mem (applyWord'_mem cGens _))⟩, by
+    show ((applyWord' cGens (cWit x)).symm.trans (applyWord' cGens (cWit y))) x = y
+    simp only [Equiv.trans_apply]
+    rw [show (applyWord' cGens (cWit x)).symm x = 0 from by
+      rw [Equiv.symm_apply_eq]; exact (cWit_ok x).symm]; exact cWit_ok y⟩
+
+/-- **The 3-cube is a Sabidussi coset graph**: `Sab(S₄, C₃, D)`. -/
+noncomputable def cubeSabidussiIso :
+    cubeGraph ≃g SimpleGraph.cosetGraph (MulAction.stabilizer cGroup (0 : Fin 8))
+      (connectionSet cGroup cubeGraph 0) (connectionSet.isConnectionSet 0) :=
+  sabidussiIso 0
+end CubeSabidussi

From 9dc2732ed9e44313edefe010aebb88ff110aa4d6 Mon Sep 17 00:00:00 2001
From: Robin Langer <langer.robin@gmail.com>
Date: Fri, 22 May 2026 09:42:22 +1000
Subject: [PATCH 11/14] =?UTF-8?q?style:=20show=20=E2=86=92=20change=20for?=
 =?UTF-8?q?=20linter.style.show?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Archive/NamedGraphs.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Archive/NamedGraphs.lean b/Archive/NamedGraphs.lean
index 24053e2644088a..81e5392812ee2c 100644
--- a/Archive/NamedGraphs.lean
+++ b/Archive/NamedGraphs.lean
@@ -231,7 +231,7 @@ private noncomputable instance : GraphAction dGroup (Fin 20) dodecahedronGraph w
 private noncomputable instance : MulAction.IsPretransitive dGroup (Fin 20) where
   exists_smul_eq x y := ⟨⟨_, dGroup.mul_mem (applyWord'_mem dGens _)
     (dGroup.inv_mem (applyWord'_mem dGens _))⟩, by
-    show ((applyWord' dGens (dWit x)).symm.trans (applyWord' dGens (dWit y))) x = y
+    change ((applyWord' dGens (dWit x)).symm.trans (applyWord' dGens (dWit y))) x = y
     simp only [Equiv.trans_apply]
     rw [show (applyWord' dGens (dWit x)).symm x = 0 from by
       rw [Equiv.symm_apply_eq]; exact (dWit_ok x).symm]; exact dWit_ok y⟩
@@ -276,7 +276,7 @@ private noncomputable instance : GraphAction cGroup (Fin 8) cubeGraph where
 private noncomputable instance : MulAction.IsPretransitive cGroup (Fin 8) where
   exists_smul_eq x y := ⟨⟨_, cGroup.mul_mem (applyWord'_mem cGens _)
     (cGroup.inv_mem (applyWord'_mem cGens _))⟩, by
-    show ((applyWord' cGens (cWit x)).symm.trans (applyWord' cGens (cWit y))) x = y
+    change ((applyWord' cGens (cWit x)).symm.trans (applyWord' cGens (cWit y))) x = y
     simp only [Equiv.trans_apply]
     rw [show (applyWord' cGens (cWit x)).symm x = 0 from by
       rw [Equiv.symm_apply_eq]; exact (cWit_ok x).symm]; exact cWit_ok y⟩

From 2ea9b7cdf217054a82c8f2b0582dbce983414c5d Mon Sep 17 00:00:00 2001
From: Robin Langer <langer.robin@gmail.com>
Date: Fri, 22 May 2026 10:11:47 +1000
Subject: [PATCH 12/14] feat(Archive): Petersen graph is a Sabidussi coset
 graph
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Add petersenSabidussiIso: the Petersen graph (defined as the antipodal
quotient of the dodecahedron) is isomorphic to a coset graph via the
Sabidussi representation theorem.

S₅ (order 120) acts vertex-transitively with stabilizer S₂×S₃:
  petersenGraph ≃g Sab(S₅, S₂×S₃, D) with 10 = 120/12 vertices.

Generators computed by GAP (GRAPE AutGroupGraph).
---
 Archive/NamedGraphs.lean | 47 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 47 insertions(+)

diff --git a/Archive/NamedGraphs.lean b/Archive/NamedGraphs.lean
index 81e5392812ee2c..5f4edcdfd8a583 100644
--- a/Archive/NamedGraphs.lean
+++ b/Archive/NamedGraphs.lean
@@ -287,3 +287,50 @@ noncomputable def cubeSabidussiIso :
       (connectionSet cGroup cubeGraph 0) (connectionSet.isConnectionSet 0) :=
   sabidussiIso 0
 end CubeSabidussi
+
+section PetersenSabidussi
+private def pG1F : Array (Fin 10) := #[2,1,7,6,3,9,5,0,4,8]
+private def pG1I : Array (Fin 10) := #[7,1,0,4,8,6,3,2,9,5]
+private def pG2F : Array (Fin 10) := #[3,4,0,5,6,2,9,8,7,1]
+private def pG2I : Array (Fin 10) := #[2,9,5,0,1,3,4,8,7,6]
+private theorem pG1F_s : pG1F.size = 10 := by native_decide
+private theorem pG1I_s : pG1I.size = 10 := by native_decide
+private theorem pG2F_s : pG2F.size = 10 := by native_decide
+private theorem pG2I_s : pG2I.size = 10 := by native_decide
+private def pG1 : Equiv.Perm (Fin 10) where
+  toFun i := pG1F[i.val]'(by have := pG1F_s; omega)
+  invFun i := pG1I[i.val]'(by have := pG1I_s; omega)
+  left_inv := by native_decide
+  right_inv := by native_decide
+private def pG2 : Equiv.Perm (Fin 10) where
+  toFun i := pG2F[i.val]'(by have := pG2F_s; omega)
+  invFun i := pG2I[i.val]'(by have := pG2I_s; omega)
+  left_inv := by native_decide
+  right_inv := by native_decide
+private def pGens : Fin 2 → Equiv.Perm (Fin 10) | 0 => pG1 | 1 => pG2
+private def pGroup : Subgroup (Equiv.Perm (Fin 10)) := Subgroup.closure (Set.range pGens)
+private def pWD : Array (List (Fin 4)) :=
+  #[[], [1,2,3], [0], [1], [1,2], [0,3], [1,0], [2], [2,1], [0,3,0]]
+private theorem pWD_s : pWD.size = 10 := by native_decide
+private def pWit (v : Fin 10) : List (Fin 4) := pWD[v.val]'(by have := pWD_s; omega)
+private theorem pWit_ok :
+    ∀ v : Fin 10, applyWord' pGens (pWit v) 0 = v := by native_decide
+private noncomputable instance : MulAction pGroup (Fin 10) := MulAction.compHom _ pGroup.subtype
+private noncomputable instance : GraphAction pGroup (Fin 10) petersenGraph where
+  adj_smul g u v h := closureGraphAction pGens
+    (fun i => by match i with | 0 => exact (by native_decide) | 1 => exact (by native_decide))
+    g.1 g.2 u v h
+private noncomputable instance : MulAction.IsPretransitive pGroup (Fin 10) where
+  exists_smul_eq x y :=
+    ⟨⟨_, pGroup.mul_mem (applyWord'_mem pGens _) (pGroup.inv_mem (applyWord'_mem pGens _))⟩, by
+      change ((applyWord' pGens (pWit x)).symm.trans (applyWord' pGens (pWit y))) x = y
+      simp only [Equiv.trans_apply]
+      rw [show (applyWord' pGens (pWit x)).symm x = 0 from by
+        rw [Equiv.symm_apply_eq]; exact (pWit_ok x).symm]; exact pWit_ok y⟩
+
+/-- **The Petersen graph is a Sabidussi coset graph**: `Sab(S₅, S₂×S₃, D)`. -/
+noncomputable def petersenSabidussiIso :
+    petersenGraph ≃g SimpleGraph.cosetGraph (MulAction.stabilizer pGroup (0 : Fin 10))
+      (connectionSet pGroup petersenGraph 0) (connectionSet.isConnectionSet 0) :=
+  sabidussiIso 0
+end PetersenSabidussi

From 56b58e1fbe696f14370197f970f1725a1be4f941 Mon Sep 17 00:00:00 2001
From: Robin Langer <langer.robin@gmail.com>
Date: Fri, 22 May 2026 18:10:49 +1000
Subject: [PATCH 13/14] =?UTF-8?q?Add=20dodecahedron=E2=86=92Petersen=20vis?=
 =?UTF-8?q?ualization=20link?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Archive/NamedGraphs.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/Archive/NamedGraphs.lean b/Archive/NamedGraphs.lean
index 5f4edcdfd8a583..e822e5c5f61ee4 100644
--- a/Archive/NamedGraphs.lean
+++ b/Archive/NamedGraphs.lean
@@ -26,6 +26,10 @@ whose quotient is K₄.
 * `petersenGraph_regular` — the Petersen graph is 3-regular
 * `cubeQuotient_eq_top` — the antipodal quotient of the cube is K₄
 
+## Visualizations
+
+* [Dodecahedron → Petersen quotient](https://raw.githubusercontent.com/RaggedR/symmetric-graphs/main/lean/named_graphs/dodecahedron-quotient-petersen.jpeg) — the Z₂ antipodal quotient, with fibers color-coded
+
 ## References
 
 * Robin Langer, *Symmetric Graphs and their Quotients*, arXiv:1306.4798

From 338b7d88505a98c1c12d5a4ca800fa30bed80906 Mon Sep 17 00:00:00 2001
From: Robin Langer <langer.robin@gmail.com>
Date: Fri, 22 May 2026 18:18:56 +1000
Subject: [PATCH 14/14] =?UTF-8?q?Add=20cube=E2=86=92K=E2=82=84=20visualiza?=
 =?UTF-8?q?tion=20link?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Archive/NamedGraphs.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Archive/NamedGraphs.lean b/Archive/NamedGraphs.lean
index e822e5c5f61ee4..eda6a741f3eb6e 100644
--- a/Archive/NamedGraphs.lean
+++ b/Archive/NamedGraphs.lean
@@ -29,6 +29,7 @@ whose quotient is K₄.
 ## Visualizations
 
 * [Dodecahedron → Petersen quotient](https://raw.githubusercontent.com/RaggedR/symmetric-graphs/main/lean/named_graphs/dodecahedron-quotient-petersen.jpeg) — the Z₂ antipodal quotient, with fibers color-coded
+* [3-Cube → K₄ quotient](https://raw.githubusercontent.com/RaggedR/symmetric-graphs/main/lean/named_graphs/cube-quotient-k4.jpeg) — the Z₂ antipodal quotient (bitwise complement)
 
 ## References