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/10] 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/10] 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/10] 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/10] 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/10] 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/10] 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/10] 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 52e37f3354b221cceb1786a3740d3cb4cbef69fa Mon Sep 17 00:00:00 2001
From: Robin Langer <langer.robin@gmail.com>
Date: Thu, 21 May 2026 20:21:45 +1000
Subject: [PATCH 08/10] feat(Combinatorics): cellular surfaces, CSS codes, and
 k = 2g
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Defines CellularSurface (2-cell embedding of a graph on a closed
surface) with boundary operators ∂₁, ∂₂ over F₂ and proves the chain
complex condition ∂₁∘∂₂ = 0. Rank theorems rank(∂₁) = V-1 and
rank(∂₂) = F-1 via kernel characterisation of connected graphs.

Assembles into the CSS surface code theorem: a genus-g surface tiling
encodes k = 2g logical qubits (Breuckmann-Terhal, arXiv:1506.04029).
---
 Mathlib.lean                               |   1 +
 Mathlib/Combinatorics/CellularSurface.lean | 479 +++++++++++++++++++++
 2 files changed, 480 insertions(+)
 create mode 100644 Mathlib/Combinatorics/CellularSurface.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 100ccd502ff9dd..7215598808ea0e 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -3493,6 +3493,7 @@ public import Mathlib.Combinatorics.Additive.SubsetSum
 public import Mathlib.Combinatorics.Additive.VerySmallDoubling
 public import Mathlib.Combinatorics.Colex
 public import Mathlib.Combinatorics.Compactness
+public import Mathlib.Combinatorics.CellularSurface
 public import Mathlib.Combinatorics.Configuration
 public import Mathlib.Combinatorics.Derangements.Basic
 public import Mathlib.Combinatorics.Derangements.Exponential
diff --git a/Mathlib/Combinatorics/CellularSurface.lean b/Mathlib/Combinatorics/CellularSurface.lean
new file mode 100644
index 00000000000000..3a47c15e8580e8
--- /dev/null
+++ b/Mathlib/Combinatorics/CellularSurface.lean
@@ -0,0 +1,479 @@
+/-
+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.Data.ZMod.Basic
+public import Mathlib.LinearAlgebra.Matrix.Rank
+public import Mathlib.Algebra.BigOperators.Group.Finset.Basic
+public import Mathlib.Algebra.Field.ZMod
+public import Mathlib.LinearAlgebra.Dimension.Finite
+public import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
+public import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
+
+/-!
+# Cellular surfaces, CSS codes, and k = 2g
+
+A `CellularSurface` encodes the combinatorial data of a 2-cell embedding of a graph
+on a closed surface: vertices, edges with endpoints, and faces whose boundaries are
+closed directed trails. The boundary operators ∂₁ (vertex-edge) and ∂₂ (edge-face)
+are matrices over F₂, and the chain complex condition ∂₁ ∘ ∂₂ = 0 is proved from the
+closed walk axiom.
+
+The rank theorems `rank(∂₁) = V - 1` and `rank(∂₂) = F - 1` follow from kernel
+characterisations: for connected graphs, `ker(∂₁ᵀ) = span{1}` over F₂.
+
+A `SurfaceTiling` with genus g gives a CSS quantum error-correcting code encoding
+`k = 2g` logical qubits: the first Betti number of the surface. This follows from
+the rank theorems and Euler's formula `V - E + F = 2 - 2g`.
+
+## Main definitions
+
+* `CellularSurface` — combinatorial 2-cell embedding of a graph on a closed surface
+* `CellularSurface.d1` — the boundary operator ∂₁ (vertex-edge incidence over F₂)
+* `CellularSurface.d2` — the boundary operator ∂₂ (edge-face boundary over F₂)
+* `SurfaceTiling` — a surface tiling with Euler characteristic `2 - 2g`
+* `CSSFromTiling` — a CSS quantum code from a surface tiling
+
+## Main results
+
+* `CellularSurface.d1_mul_d2_eq_zero` — ∂₁ ∘ ∂₂ = 0
+* `CellularSurface.d1_rank_eq` — rank(∂₁) = V - 1 for connected graphs
+* `CellularSurface.d2_rank_eq` — rank(∂₂) = F - 1 for connected dual graphs
+* `css_k_eq_2g` — the CSS surface code encodes 2g logical qubits
+* `CellularSurface.css_k_eq_2g_from_surface` — end-to-end from combinatorial data
+
+## References
+
+* Breuckmann & Terhal, *Constructions and noise threshold of hyperbolic surface codes*,
+  IEEE Trans. Inf. Theory 62(6), 2016, arXiv:1506.04029
+* Robin Langer, *Symmetric Graphs and their Quotients*, arXiv:1306.4798
+-/
+
+@[expose] public section
+
+open Matrix Finset
+
+attribute [local instance] ZMod.instField
+
+/-! ## CellularSurface -/
+
+/-- A `CellularSurface` is the combinatorial data of a 2-cell embedding of a
+graph on a closed surface. Faces are given as closed directed trails:
+ordered sequences of directed edges forming closed walks in the graph. -/
+structure CellularSurface where
+  /-- Number of vertices (0-cells) -/
+  nV : ℕ
+  /-- Number of edges (1-cells) -/
+  nE : ℕ
+  /-- Number of faces (2-cells) -/
+  nF : ℕ
+  /-- Source vertex of each edge -/
+  edge_src : Fin nE → Fin nV
+  /-- Target vertex of each edge -/
+  edge_tgt : Fin nE → Fin nV
+  /-- No loops: every edge has distinct endpoints -/
+  edge_ne : ∀ e, edge_src e ≠ edge_tgt e
+  /-- Number of edges bounding each face -/
+  face_len : Fin nF → ℕ
+  /-- Every face boundary is nonempty -/
+  face_len_pos : ∀ f, 0 < face_len f
+  /-- The sequence of edges traversed by face f's boundary -/
+  face_edge : (f : Fin nF) → Fin (face_len f) → Fin nE
+  /-- Traversal direction for each boundary step: `true` = src → tgt -/
+  face_dir : (f : Fin nF) → Fin (face_len f) → Bool
+  /-- Trail condition: no edge is traversed twice in a single face boundary -/
+  face_inj : ∀ f, Function.Injective (face_edge f)
+  /-- **Closed walk**: the end vertex of step `i` equals the start vertex of the
+      cyclically next step. -/
+  face_closed : ∀ (f : Fin nF) (i : Fin (face_len f)),
+    let j : Fin (face_len f) :=
+      ⟨(i.val + 1) % face_len f, Nat.mod_lt _ (face_len_pos f)⟩
+    (if face_dir f i then edge_tgt (face_edge f i) else edge_src (face_edge f i)) =
+    (if face_dir f j then edge_src (face_edge f j) else edge_tgt (face_edge f j))
+
+namespace CellularSurface
+
+variable (S : CellularSurface)
+
+/-- Cyclic successor on face boundary indices. -/
+def nextIdx (f : Fin S.nF) (i : Fin (S.face_len f)) : Fin (S.face_len f) :=
+  ⟨(i.val + 1) % S.face_len f, Nat.mod_lt _ (S.face_len_pos f)⟩
+
+/-- The starting vertex when traversing step `i` of face `f`'s boundary. -/
+def stepStart (f : Fin S.nF) (i : Fin (S.face_len f)) : Fin S.nV :=
+  if S.face_dir f i then S.edge_src (S.face_edge f i)
+  else S.edge_tgt (S.face_edge f i)
+
+/-- The ending vertex when traversing step `i` of face `f`'s boundary. -/
+def stepEnd (f : Fin S.nF) (i : Fin (S.face_len f)) : Fin S.nV :=
+  if S.face_dir f i then S.edge_tgt (S.face_edge f i)
+  else S.edge_src (S.face_edge f i)
+
+theorem stepEnd_eq_stepStart_next (f : Fin S.nF) (i : Fin (S.face_len f)) :
+    S.stepEnd f i = S.stepStart f (S.nextIdx f i) :=
+  S.face_closed f i
+
+/-! ### Boundary operators over F₂ -/
+
+/-- The boundary operator ∂₁: vertex–edge incidence matrix over F₂. -/
+def d1 : Matrix (Fin S.nV) (Fin S.nE) (ZMod 2) :=
+  fun v e => (if S.edge_src e = v then 1 else 0) + (if S.edge_tgt e = v then 1 else 0)
+
+/-- The boundary operator ∂₂: edge–face boundary matrix over F₂. -/
+def d2 : Matrix (Fin S.nE) (Fin S.nF) (ZMod 2) :=
+  fun e f => ∑ i : Fin (S.face_len f), if S.face_edge f i = e then 1 else 0
+
+/-! ### ∂₁ ∘ ∂₂ = 0 -/
+
+theorem nextIdx_injective (f : Fin S.nF) : Function.Injective (S.nextIdx f) := by
+  intro a b h
+  simp only [nextIdx, Fin.mk.injEq] at h
+  have ha := a.isLt; have hb := b.isLt
+  ext
+  by_cases ha' : a.val + 1 < S.face_len f <;> by_cases hb' : b.val + 1 < S.face_len f
+  · rw [Nat.mod_eq_of_lt ha', Nat.mod_eq_of_lt hb'] at h; omega
+  · rw [Nat.mod_eq_of_lt ha', show b.val + 1 = S.face_len f from by omega, Nat.mod_self] at h
+    omega
+  · rw [show a.val + 1 = S.face_len f from by omega, Nat.mod_self, Nat.mod_eq_of_lt hb'] at h
+    omega
+  · omega
+
+theorem nextIdx_bijective (f : Fin S.nF) : Function.Bijective (S.nextIdx f) :=
+  Finite.injective_iff_bijective.mp (S.nextIdx_injective f)
+
+noncomputable def nextPerm (f : Fin S.nF) : Equiv.Perm (Fin (S.face_len f)) :=
+  Equiv.ofBijective _ (S.nextIdx_bijective f)
+
+theorem d1_eq_start_add_end (v : Fin S.nV) (f : Fin S.nF) (i : Fin (S.face_len f)) :
+    S.d1 v (S.face_edge f i) =
+      (if S.stepStart f i = v then 1 else 0) +
+      (if S.stepEnd f i = v then 1 else 0) := by
+  unfold d1 stepStart stepEnd
+  rcases S.face_dir f i with _ | _ <;> simp [add_comm]
+
+/-- **∂₁ ∘ ∂₂ = 0**: the chain complex condition for cellular surfaces over F₂. -/
+theorem d1_mul_d2_eq_zero : S.d1 * S.d2 = 0 := by
+  ext v f
+  simp only [Matrix.mul_apply, d2, Matrix.zero_apply]
+  simp_rw [Finset.mul_sum]
+  rw [Finset.sum_comm]
+  have step2 : ∀ i : Fin (S.face_len f),
+      ∑ e : Fin S.nE, S.d1 v e * (if S.face_edge f i = e then 1 else 0) =
+      S.d1 v (S.face_edge f i) := by
+    intro i
+    conv_lhs =>
+      arg 2; ext e
+      rw [show S.d1 v e * (if S.face_edge f i = e then 1 else 0) =
+          (if e = S.face_edge f i then S.d1 v e else 0) from by
+        split_ifs with h1 h2 h2 <;> simp_all [eq_comm]]
+    rw [Finset.sum_ite_eq']; simp [Finset.mem_univ]
+  simp_rw [step2, S.d1_eq_start_add_end v f, Finset.sum_add_distrib]
+  have step5 : ∀ i, (if S.stepEnd f i = v then (1 : ZMod 2) else 0) =
+      (if S.stepStart f (S.nextIdx f i) = v then 1 else 0) := by
+    intro i; rw [← S.stepEnd_eq_stepStart_next]
+  simp_rw [step5]
+  rw [show ∑ i, (if S.stepStart f (S.nextIdx f i) = v then (1 : ZMod 2) else 0) =
+      ∑ i, (if S.stepStart f i = v then 1 else 0) from
+    Equiv.sum_comp (S.nextPerm f) (fun j => if S.stepStart f j = v then 1 else 0)]
+  have : ∀ (x : ZMod 2), x + x = 0 := by decide
+  exact this _
+
+/-! ### Rank theorems -/
+
+theorem d1_col_sum_eq_zero (e : Fin S.nE) :
+    ∑ v : Fin S.nV, S.d1 v e = 0 := by
+  simp only [d1, Finset.sum_add_distrib]
+  have hsum : ∀ (a : Fin S.nV),
+      ∑ v : Fin S.nV, (if a = v then (1 : ZMod 2) else 0) = 1 := fun a => by
+    rw [Finset.sum_eq_single_of_mem a (Finset.mem_univ _)
+      (fun b _ hne => if_neg (Ne.symm hne)), if_pos rfl]
+  simp only [hsum]; decide
+
+theorem one_mem_ker_d1T :
+    (1 : Fin S.nV → ZMod 2) ∈ LinearMap.ker S.d1ᵀ.mulVecLin := by
+  rw [LinearMap.mem_ker]; ext e
+  simp only [mulVecLin_apply, mulVec, dotProduct, transpose_apply, Pi.zero_apply,
+    Pi.one_apply, mul_one]
+  exact S.d1_col_sum_eq_zero e
+
+theorem one_ne_zero_fin (hV : 0 < S.nV) :
+    (1 : Fin S.nV → ZMod 2) ≠ 0 := by
+  intro h; exact absurd (congr_fun h ⟨0, hV⟩) (by simp)
+
+theorem d1_rank_le (hV : 0 < S.nV) : S.d1.rank ≤ S.nV - 1 := by
+  rw [← rank_transpose S.d1]
+  have hrn := LinearMap.finrank_range_add_finrank_ker S.d1ᵀ.mulVecLin
+  simp only [rank, Module.finrank_pi_fintype, Module.finrank_self, Finset.sum_const,
+    Finset.card_univ, Fintype.card_fin, smul_eq_mul, mul_one] at hrn ⊢
+  have hker_ne : LinearMap.ker S.d1ᵀ.mulVecLin ≠ ⊥ := by
+    rw [ne_eq, LinearMap.ker_eq_bot']; push Not
+    exact ⟨1, (LinearMap.mem_ker.mp S.one_mem_ker_d1T), S.one_ne_zero_fin hV⟩
+  have hker_pos : 1 ≤ Module.finrank (ZMod 2) (LinearMap.ker S.d1ᵀ.mulVecLin) :=
+    Submodule.one_le_finrank_iff.mpr hker_ne
+  omega
+
+/-- The underlying simple graph of a CellularSurface. -/
+def toSimpleGraph : SimpleGraph (Fin S.nV) where
+  Adj u v := ∃ e : Fin S.nE,
+    (S.edge_src e = u ∧ S.edge_tgt e = v) ∨ (S.edge_src e = v ∧ S.edge_tgt e = u)
+  symm u v := fun ⟨e, h⟩ => ⟨e, h.symm⟩
+  loopless := ⟨fun v ⟨e, h⟩ => by
+    rcases h with ⟨h1, h2⟩ | ⟨h1, h2⟩ <;> exact S.edge_ne e (h1.trans h2.symm)⟩
+
+theorem d1T_mulVec_entry (x : Fin S.nV → ZMod 2) (e : Fin S.nE) :
+    (S.d1ᵀ *ᵥ x) e = x (S.edge_src e) + x (S.edge_tgt e) := by
+  simp only [mulVec, dotProduct, transpose_apply, d1, add_mul, Finset.sum_add_distrib]
+  have hsum : ∀ (a : Fin S.nV),
+      ∑ v : Fin S.nV, (if a = v then (1 : ZMod 2) else 0) * x v = x a := fun a => by
+    rw [Finset.sum_eq_single_of_mem a (Finset.mem_univ _)
+      (fun b _ hne => by simp [Ne.symm hne])]; simp
+  simp only [hsum]
+
+theorem ker_d1T_edge_eq {x : Fin S.nV → ZMod 2}
+    (hx : x ∈ LinearMap.ker S.d1ᵀ.mulVecLin) (e : Fin S.nE) :
+    x (S.edge_src e) = x (S.edge_tgt e) := by
+  have h := congr_fun (LinearMap.mem_ker.mp hx) e
+  simp only [mulVecLin_apply, Pi.zero_apply] at h
+  rw [S.d1T_mulVec_entry x e] at h
+  have : ∀ (a b : ZMod 2), a + b = 0 → a = b := by decide
+  exact this _ _ h
+
+theorem walk_preserves_ker {x : Fin S.nV → ZMod 2}
+    (hx : x ∈ LinearMap.ker S.d1ᵀ.mulVecLin)
+    {u v : Fin S.nV} (w : S.toSimpleGraph.Walk u v) :
+    x u = x v := by
+  induction w with
+  | nil => rfl
+  | cons hadj _ ih =>
+    obtain ⟨e, h | h⟩ := hadj
+    · have := S.ker_d1T_edge_eq hx e; rw [h.1, h.2] at this; exact this.trans ih
+    · have := S.ker_d1T_edge_eq hx e; rw [h.1, h.2] at this; exact this.symm.trans ih
+
+theorem ker_d1T_le_span_one (hconn : S.toSimpleGraph.Connected) :
+    LinearMap.ker S.d1ᵀ.mulVecLin ≤ Submodule.span (ZMod 2) {1} := by
+  intro x hx
+  rw [Submodule.mem_span_singleton]
+  have hV : 0 < S.nV := by obtain ⟨⟨_, hlt⟩⟩ := hconn.nonempty; omega
+  have hconst : ∀ u v : Fin S.nV, x u = x v := fun u v =>
+    S.walk_preserves_ker hx (hconn.preconnected u v).some
+  exact ⟨x ⟨0, hV⟩, funext fun v => by
+    simp [Pi.smul_apply, Pi.one_apply, smul_eq_mul, mul_one, hconst ⟨0, hV⟩ v]⟩
+
+theorem ker_d1T_finrank_eq_one (hconn : S.toSimpleGraph.Connected) (hV : 0 < S.nV) :
+    Module.finrank (ZMod 2) (LinearMap.ker S.d1ᵀ.mulVecLin) = 1 := by
+  have heq : LinearMap.ker S.d1ᵀ.mulVecLin =
+      Submodule.span (ZMod 2) {(1 : Fin S.nV → ZMod 2)} :=
+    le_antisymm (S.ker_d1T_le_span_one hconn)
+      ((Submodule.span_singleton_le_iff_mem _ _).mpr S.one_mem_ker_d1T)
+  rw [heq]; exact finrank_span_singleton (S.one_ne_zero_fin hV)
+
+/-- **rank(∂₁) = V - 1** for connected graphs. -/
+theorem d1_rank_eq (hconn : S.toSimpleGraph.Connected) (hV : 1 < S.nV) :
+    (S.d1.rank : ℤ) = S.nV - 1 := by
+  have hle := S.d1_rank_le (by omega)
+  have hge : S.nV - 1 ≤ S.d1.rank := by
+    rw [← rank_transpose S.d1]
+    have hrn := LinearMap.finrank_range_add_finrank_ker S.d1ᵀ.mulVecLin
+    simp only [rank, Module.finrank_pi_fintype, Module.finrank_self, Finset.sum_const,
+      Finset.card_univ, Fintype.card_fin, smul_eq_mul, mul_one] at hrn ⊢
+    rw [S.ker_d1T_finrank_eq_one hconn (by omega)] at hrn; omega
+  omega
+
+/-! ### Dual graph and rank(∂₂) -/
+
+/-- The dual graph: faces as vertices, adjacent when sharing a boundary edge. -/
+def toDualSimpleGraph : SimpleGraph (Fin S.nF) where
+  Adj f1 f2 := f1 ≠ f2 ∧ ∃ e : Fin S.nE,
+    (∃ i, S.face_edge f1 i = e) ∧ (∃ j, S.face_edge f2 j = e)
+  symm _ _ := fun ⟨hne, e, h1, h2⟩ => ⟨hne.symm, e, h2, h1⟩
+  loopless := ⟨fun _ ⟨hne, _⟩ => hne rfl⟩
+
+theorem d2_entry (f : Fin S.nF) (e : Fin S.nE) :
+    S.d2 e f = if ∃ i, S.face_edge f i = e then 1 else 0 := by
+  simp only [d2]; split_ifs with h
+  · obtain ⟨i, hi⟩ := h
+    rw [Finset.sum_eq_single_of_mem i (Finset.mem_univ _) (fun k _ hki =>
+      if_neg (fun hk => hki (S.face_inj f (hk.trans hi.symm))))]; simp [hi]
+  · push Not at h; exact Finset.sum_eq_zero (fun i _ => if_neg (h i))
+
+theorem d2_rank_le (hF : 0 < S.nF) (htwo_vec : S.d2 *ᵥ 1 = 0) :
+    S.d2.rank ≤ S.nF - 1 := by
+  unfold rank
+  have hrn := LinearMap.finrank_range_add_finrank_ker S.d2.mulVecLin
+  simp only [Module.finrank_pi_fintype, Module.finrank_self, Finset.sum_const,
+    Finset.card_univ, Fintype.card_fin, smul_eq_mul, mul_one] at hrn ⊢
+  have hker_ne : LinearMap.ker S.d2.mulVecLin ≠ ⊥ := by
+    rw [ne_eq, LinearMap.ker_eq_bot']; push Not
+    exact ⟨1, by rwa [show S.d2.mulVecLin 1 = S.d2 *ᵥ 1 from rfl],
+      fun h => absurd (congr_fun h ⟨0, hF⟩) (by simp)⟩
+  have : 1 ≤ Module.finrank (ZMod 2) (LinearMap.ker S.d2.mulVecLin) :=
+    Submodule.one_le_finrank_iff.mpr hker_ne
+  omega
+
+theorem ker_d2_dual_adj_eq {y : Fin S.nF → ZMod 2}
+    (hy : y ∈ LinearMap.ker S.d2.mulVecLin)
+    (htwo : ∀ e, (Finset.univ.filter fun f : Fin S.nF => S.d2 e f ≠ 0).card = 2)
+    {f₁ f₂ : Fin S.nF} (hadj : S.toDualSimpleGraph.Adj f₁ f₂) :
+    y f₁ = y f₂ := by
+  obtain ⟨hne, e, ⟨i, hi⟩, ⟨j, hj⟩⟩ := hadj
+  have hd₁ : S.d2 e f₁ = 1 := by rw [S.d2_entry]; exact if_pos ⟨i, hi⟩
+  have hd₂ : S.d2 e f₂ = 1 := by rw [S.d2_entry]; exact if_pos ⟨j, hj⟩
+  obtain ⟨a, b, hab, hFe_eq⟩ := Finset.card_eq_two.mp (htwo e)
+  have hf₁_mem : f₁ ∈ ({a, b} : Finset _) := by
+    rw [← hFe_eq]; exact Finset.mem_filter.mpr ⟨Finset.mem_univ _, by simp [hd₁]⟩
+  have hf₂_mem : f₂ ∈ ({a, b} : Finset _) := by
+    rw [← hFe_eq]; exact Finset.mem_filter.mpr ⟨Finset.mem_univ _, by simp [hd₂]⟩
+  have hker_e : ∑ f, S.d2 e f * y f = 0 := by
+    have := congr_fun (LinearMap.mem_ker.mp hy) e
+    simpa [mulVecLin_apply, mulVec, dotProduct] using this
+  have hpair : y a + y b = 0 := by
+    have hsplit : ∑ f, S.d2 e f * y f =
+        ∑ f ∈ Finset.univ.filter (fun f => S.d2 e f ≠ 0), S.d2 e f * y f := by
+      symm; apply Finset.sum_subset (Finset.filter_subset _ _)
+      intro f _ hf; simp only [Finset.mem_filter, Finset.mem_univ, true_and, not_not] at hf
+      rw [hf, zero_mul]
+    rw [hsplit, hFe_eq, Finset.sum_pair hab] at hker_e
+    have hzmod2 : ∀ (x : ZMod 2), x ≠ 0 → x = 1 := by decide
+    have ha_ne := (Finset.mem_filter.mp (hFe_eq ▸ Finset.mem_insert_self a {b})).2
+    have hb_ne := (Finset.mem_filter.mp (hFe_eq ▸ Finset.mem_insert.mpr
+      (Or.inr (Finset.mem_singleton.mpr rfl)))).2
+    rwa [hzmod2 _ ha_ne, hzmod2 _ hb_ne, one_mul, one_mul] at hker_e
+  have hab_eq : y a = y b := by
+    have : ∀ (x z : ZMod 2), x + z = 0 → x = z := by decide
+    exact this _ _ hpair
+  simp only [Finset.mem_insert, Finset.mem_singleton] at hf₁_mem hf₂_mem
+  rcases hf₁_mem with rfl | rfl <;> rcases hf₂_mem with rfl | rfl
+  · exact absurd rfl hne
+  · exact hab_eq
+  · exact hab_eq.symm
+  · exact absurd rfl hne
+
+theorem d2_mulVec_one_of_two_sides
+    (htwo : ∀ e, (Finset.univ.filter fun f : Fin S.nF => S.d2 e f ≠ 0).card = 2) :
+    S.d2 *ᵥ 1 = 0 := by
+  ext e
+  simp only [mulVec, dotProduct, Pi.one_apply, mul_one, Pi.zero_apply]
+  rw [show ∑ f, S.d2 e f = ∑ f ∈ Finset.univ.filter (fun f => S.d2 e f ≠ 0), S.d2 e f from by
+    symm; apply Finset.sum_subset (Finset.filter_subset _ _)
+    intro f _ hf; simpa using hf]
+  obtain ⟨a, b, hab, hFe_eq⟩ := Finset.card_eq_two.mp (htwo e)
+  rw [hFe_eq, Finset.sum_pair hab]
+  have hzmod2 : ∀ (x : ZMod 2), x ≠ 0 → x = 1 := by decide
+  have ha := (Finset.mem_filter.mp (hFe_eq ▸ Finset.mem_insert_self a {b})).2
+  have hb := (Finset.mem_filter.mp (hFe_eq ▸ Finset.mem_insert.mpr
+    (Or.inr (Finset.mem_singleton.mpr rfl)))).2
+  rw [hzmod2 _ ha, hzmod2 _ hb]; decide
+
+/-- **rank(∂₂) = F - 1** for connected dual graphs with the two-sides condition. -/
+theorem d2_rank_eq (hconn_dual : S.toDualSimpleGraph.Connected) (hF : 1 < S.nF)
+    (htwo : ∀ e, (Finset.univ.filter fun f : Fin S.nF => S.d2 e f ≠ 0).card = 2) :
+    (S.d2.rank : ℤ) = S.nF - 1 := by
+  have hF_pos : 0 < S.nF := by omega
+  have hmem : (1 : Fin S.nF → ZMod 2) ∈ LinearMap.ker S.d2.mulVecLin := by
+    rw [LinearMap.mem_ker, mulVecLin_apply]; exact S.d2_mulVec_one_of_two_sides htwo
+  have heq : LinearMap.ker S.d2.mulVecLin =
+      Submodule.span (ZMod 2) {(1 : Fin S.nF → ZMod 2)} :=
+    le_antisymm
+      (by intro y hy; rw [Submodule.mem_span_singleton]
+          have hconst : ∀ a b : Fin S.nF, y a = y b := fun a b =>
+            by induction (hconn_dual.preconnected a b).some with
+               | nil => rfl
+               | cons hadj _ ih => exact (S.ker_d2_dual_adj_eq hy htwo hadj).trans ih
+          exact ⟨y ⟨0, hF_pos⟩, funext fun v => by
+            simp [Pi.smul_apply, Pi.one_apply, smul_eq_mul, mul_one, hconst ⟨0, hF_pos⟩ v]⟩)
+      ((Submodule.span_singleton_le_iff_mem _ _).mpr hmem)
+  have hle := S.d2_rank_le hF_pos (S.d2_mulVec_one_of_two_sides htwo)
+  have hge : S.nF - 1 ≤ S.d2.rank := by
+    have hker : Module.finrank (ZMod 2) (LinearMap.ker S.d2.mulVecLin) = 1 := by
+      rw [heq]; exact finrank_span_singleton (fun h => absurd (congr_fun h ⟨0, hF_pos⟩) (by simp))
+    have hrn := LinearMap.finrank_range_add_finrank_ker S.d2.mulVecLin
+    simp only [rank, Module.finrank_pi_fintype, Module.finrank_self, Finset.sum_const,
+      Finset.card_univ, Fintype.card_fin, smul_eq_mul, mul_one] at hrn ⊢
+    rw [hker] at hrn; omega
+  omega
+
+end CellularSurface
+
+/-! ## CSS quantum codes from surface tilings -/
+
+/-- A tiling of a closed orientable surface of genus `g`. -/
+structure SurfaceTiling where
+  /-- Number of vertices -/
+  V : ℕ
+  /-- Number of edges -/
+  E : ℕ
+  /-- Number of faces -/
+  F : ℕ
+  /-- Genus of the surface -/
+  g : ℕ
+  /-- The primal graph is non-degenerate -/
+  hV : 0 < V
+  /-- The dual graph is non-degenerate -/
+  hF : 0 < F
+  /-- Euler's formula -/
+  euler : (V : ℤ) - E + F = 2 - 2 * g
+
+/-- A CSS quantum code from a surface tiling. -/
+structure CSSFromTiling (T : SurfaceTiling) where
+  /-- X-check matrix (vertex-edge incidence) -/
+  H_X : Matrix (Fin T.V) (Fin T.E) (ZMod 2)
+  /-- Z-check matrix (face-edge incidence) -/
+  H_Z : Matrix (Fin T.F) (Fin T.E) (ZMod 2)
+  /-- CSS orthogonality -/
+  orthogonal : H_X * H_Zᵀ = 0
+
+namespace CSSFromTiling
+
+variable {T : SurfaceTiling}
+
+/-- The number of logical qubits: k = E - rank(H_X) - rank(H_Z). -/
+noncomputable def k (css : CSSFromTiling T) : ℤ :=
+  (T.E : ℤ) - css.H_X.rank - css.H_Z.rank
+
+end CSSFromTiling
+
+/-- **The CSS surface code theorem**: k = 2g. -/
+theorem css_k_eq_2g (T : SurfaceTiling) (css : CSSFromTiling T)
+    (hX : (css.H_X.rank : ℤ) = T.V - 1)
+    (hZ : (css.H_Z.rank : ℤ) = T.F - 1) :
+    css.k = 2 * T.g := by
+  unfold CSSFromTiling.k
+  linarith [T.euler]
+
+/-! ## Assembly: CellularSurface → k = 2g -/
+
+/-- Extract a `SurfaceTiling` from a `CellularSurface` with given genus. -/
+def CellularSurface.toSurfaceTiling (S : CellularSurface) (g : ℕ)
+    (hV : 0 < S.nV) (hF : 0 < S.nF)
+    (euler : (S.nV : ℤ) - S.nE + S.nF = 2 - 2 * g) : SurfaceTiling where
+  V := S.nV
+  E := S.nE
+  F := S.nF
+  g := g
+  hV := hV
+  hF := hF
+  euler := euler
+
+/-- **End-to-end theorem**: a CellularSurface with connected primal and dual graphs
+on a genus-g surface encodes exactly 2g logical qubits. -/
+theorem CellularSurface.css_k_eq_2g_from_surface (S : CellularSurface) (g : ℕ)
+    (hV : 1 < S.nV) (hF : 1 < S.nF)
+    (euler : (S.nV : ℤ) - S.nE + S.nF = 2 - 2 * g)
+    (hconn : S.toSimpleGraph.Connected)
+    (hconn_dual : S.toDualSimpleGraph.Connected)
+    (htwo : ∀ e, (Finset.univ.filter fun f : Fin S.nF => S.d2 e f ≠ 0).card = 2) :
+    let T := S.toSurfaceTiling g (by omega) (by omega) euler
+    let css : CSSFromTiling T :=
+      { H_X := S.d1
+        H_Z := S.d2ᵀ
+        orthogonal := by rw [Matrix.transpose_transpose]; exact S.d1_mul_d2_eq_zero }
+    css.k = 2 * g := by
+  intro T css
+  apply css_k_eq_2g
+  · exact S.d1_rank_eq hconn hV
+  · show (S.d2ᵀ.rank : ℤ) = S.nF - 1
+    rw [rank_transpose]
+    exact S.d2_rank_eq hconn_dual hF htwo

From c21b1524376e0b1b412e367205042cdcfa372650 Mon Sep 17 00:00:00 2001
From: Robin Langer <langer.robin@gmail.com>
Date: Thu, 21 May 2026 21:54:12 +1000
Subject: [PATCH 09/10] chore: add nextPerm docstring, fix lint warnings

- Add missing documentation string for `CellularSurface.nextPerm`
- Remove unused `Pi.one_apply` from two `simp` calls
- Replace `show` with `change` where it transforms the goal
---
 Mathlib/Combinatorics/CellularSurface.lean | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Combinatorics/CellularSurface.lean b/Mathlib/Combinatorics/CellularSurface.lean
index 3a47c15e8580e8..a894799bdd54c2 100644
--- a/Mathlib/Combinatorics/CellularSurface.lean
+++ b/Mathlib/Combinatorics/CellularSurface.lean
@@ -144,6 +144,7 @@ theorem nextIdx_injective (f : Fin S.nF) : Function.Injective (S.nextIdx f) := b
 theorem nextIdx_bijective (f : Fin S.nF) : Function.Bijective (S.nextIdx f) :=
   Finite.injective_iff_bijective.mp (S.nextIdx_injective f)
 
+/-- `nextIdx` as a permutation (equivalence) on face boundary indices. -/
 noncomputable def nextPerm (f : Fin S.nF) : Equiv.Perm (Fin (S.face_len f)) :=
   Equiv.ofBijective _ (S.nextIdx_bijective f)
 
@@ -260,7 +261,7 @@ theorem ker_d1T_le_span_one (hconn : S.toSimpleGraph.Connected) :
   have hconst : ∀ u v : Fin S.nV, x u = x v := fun u v =>
     S.walk_preserves_ker hx (hconn.preconnected u v).some
   exact ⟨x ⟨0, hV⟩, funext fun v => by
-    simp [Pi.smul_apply, Pi.one_apply, smul_eq_mul, mul_one, hconst ⟨0, hV⟩ v]⟩
+    simp [Pi.smul_apply, smul_eq_mul, mul_one, hconst ⟨0, hV⟩ v]⟩
 
 theorem ker_d1T_finrank_eq_one (hconn : S.toSimpleGraph.Connected) (hV : 0 < S.nV) :
     Module.finrank (ZMod 2) (LinearMap.ker S.d1ᵀ.mulVecLin) = 1 := by
@@ -383,7 +384,7 @@ theorem d2_rank_eq (hconn_dual : S.toDualSimpleGraph.Connected) (hF : 1 < S.nF)
                | nil => rfl
                | cons hadj _ ih => exact (S.ker_d2_dual_adj_eq hy htwo hadj).trans ih
           exact ⟨y ⟨0, hF_pos⟩, funext fun v => by
-            simp [Pi.smul_apply, Pi.one_apply, smul_eq_mul, mul_one, hconst ⟨0, hF_pos⟩ v]⟩)
+            simp [Pi.smul_apply, smul_eq_mul, mul_one, hconst ⟨0, hF_pos⟩ v]⟩)
       ((Submodule.span_singleton_le_iff_mem _ _).mpr hmem)
   have hle := S.d2_rank_le hF_pos (S.d2_mulVec_one_of_two_sides htwo)
   have hge : S.nF - 1 ≤ S.d2.rank := by
@@ -474,6 +475,6 @@ theorem CellularSurface.css_k_eq_2g_from_surface (S : CellularSurface) (g : ℕ)
   intro T css
   apply css_k_eq_2g
   · exact S.d1_rank_eq hconn hV
-  · show (S.d2ᵀ.rank : ℤ) = S.nF - 1
+  · change (S.d2ᵀ.rank : ℤ) = S.nF - 1
     rw [rank_transpose]
     exact S.d2_rank_eq hconn_dual hF htwo

From b794a3ad67f822a87c548e3bc1ed203af5371ddb Mon Sep 17 00:00:00 2001
From: Robin Langer <langer.robin@gmail.com>
Date: Thu, 21 May 2026 23:33:27 +1000
Subject: [PATCH 10/10] chore: fix Mathlib.lean import ordering for
 CellularSurface

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

diff --git a/Mathlib.lean b/Mathlib.lean
index 7215598808ea0e..d5e433b1aa99b0 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -3491,9 +3491,9 @@ public import Mathlib.Combinatorics.Additive.RuzsaCovering
 public import Mathlib.Combinatorics.Additive.SmallTripling
 public import Mathlib.Combinatorics.Additive.SubsetSum
 public import Mathlib.Combinatorics.Additive.VerySmallDoubling
+public import Mathlib.Combinatorics.CellularSurface
 public import Mathlib.Combinatorics.Colex
 public import Mathlib.Combinatorics.Compactness
-public import Mathlib.Combinatorics.CellularSurface
 public import Mathlib.Combinatorics.Configuration
 public import Mathlib.Combinatorics.Derangements.Basic
 public import Mathlib.Combinatorics.Derangements.Exponential