diff --git a/Archive.lean b/Archive.lean
index 8ca03e8bc806d9..c6507babcd9424 100644
--- a/Archive.lean
+++ b/Archive.lean
@@ -61,6 +61,8 @@ import Archive.Imo.Imo2024Q5
 import Archive.Imo.Imo2024Q6
 import Archive.Imo.Imo2025Q3
 import Archive.Kuratowski
+import Archive.LangerGraph
+import Archive.DualLangerGraph
 import Archive.MinimalSheffer
 import Archive.MiuLanguage.Basic
 import Archive.MiuLanguage.DecisionNec
diff --git a/Archive/DualLangerGraph.lean b/Archive/DualLangerGraph.lean
new file mode 100644
index 00000000000000..f5ad53ee75e517
--- /dev/null
+++ b/Archive/DualLangerGraph.lean
@@ -0,0 +1,438 @@
+/-
+Copyright (c) 2026 Robin Langer. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Robin Langer
+
+# The dual Langer graph: line-collinearity of GH(2,2)
+
+The split Cayley hexagon GH(2,2) has 63 points and 63 lines, with incidence
+graph the Tutte 12-cage (126 vertices, cubic, girth 12). The **Langer graph**
+is the point-collinearity graph: p ~ q iff they share a line (distance-2 in
+the Tutte 12-cage restricted to points).
+
+The **dual Langer graph** is the line-collinearity graph: l₁ ~ l₂ iff they
+share a point (distance-2 restricted to lines). It has the same intersection
+array {6, 4, 4; 1, 1, 3} as the Langer graph but is **not isomorphic** to it.
+
+## Why GH(2,2) is not self-dual
+
+A generalized hexagon GH(q, q) is self-dual if and only if q is a power of 3
+(Cohen–Tits). Since q = 2 is not a power of 3, the split Cayley hexagon H(2)
+and its dual H(2)^D are non-isomorphic as geometries, though they share the
+same incidence graph. Their collinearity graphs (the Langer and dual Langer
+graphs) have identical intersection arrays but are non-isomorphic.
+
+## The distinguishing invariant
+
+For any vertex v, the subgraph induced on vertices at graph distance 3 is:
+  - **Connected** in the Langer graph (1 component of 32 vertices)
+  - **Disconnected** in the dual Langer graph (2 components of 16 vertices)
+
+This is a graph invariant: any isomorphism φ : G ≃g H preserves graph
+distances and hence connectivity of distance shells. The d₃-connectivity
+therefore provides a computable certificate of non-isomorphism.
+
+## Group-theoretic interpretation
+
+G₂(2) has two non-conjugate maximal subgroups of order 192:
+  - Point stabiliser: (SL(2,3) : C₄) : C₂ → Langer graph on G₂(2)/H₁₉₂
+  - Line stabiliser: (((C₄ × C₄) : C₃) : C₂) : C₂ → dual Langer on G₂(2)/H'₁₉₂
+
+Same group, non-conjugate stabilisers, non-isomorphic coset graphs.
+
+## References
+
+- Cohen, Tits, *On generalized hexagons and a near octagon whose lines have three points*
+- Langer, *Symmetric Graphs and their Quotients*, arXiv:1306.4798
+- Brouwer–Cohen–Neumaier, *Distance-Regular Graphs* (1989), §6.5
+-/
+
+import Archive.LangerGraph
+import Mathlib.Combinatorics.SimpleGraph.Maps
+
+/-! ## The dual Langer graph -/
+
+/-- Distance-2 adjacency on **lines**: two lines l₁, l₂ of GH(2,2) are
+    adjacent iff they share a point. In the Tutte 12-cage, line vertices have
+    indices 63–125, and a shared point means a common point-neighbor. -/
+def dualLangerAdjBool (l₁ l₂ : Fin 63) : Bool :=
+  l₁ != l₂ &&
+  let lv₁ : Fin 126 := ⟨l₁.val + 63, by omega⟩
+  let lv₂ : Fin 126 := ⟨l₂.val + 63, by omega⟩
+  (List.finRange 63).any fun p =>
+    let pv : Fin 126 := ⟨p.val, by omega⟩
+    tutte12AdjBool pv lv₁ && tutte12AdjBool pv lv₂
+
+set_option maxHeartbeats 400000 in
+/-- The **dual Langer graph**: line-collinearity of GH(2,2).
+
+    Two lines are adjacent iff they are concurrent (share a point).
+    This is the distance-2 graph of the Tutte 12-cage restricted to
+    line vertices, dual to the Langer graph (point-collinearity). -/
+def dualLangerSimpleGraph : SimpleGraph (Fin 63) where
+  Adj l₁ l₂ := dualLangerAdjBool l₁ l₂
+  symm l₁ l₂ := by simp only [dualLangerAdjBool]; revert l₁ l₂; native_decide
+  loopless := ⟨fun l => by simp only [dualLangerAdjBool]; revert l; native_decide⟩
+
+instance dualLangerDecAdj : DecidableRel dualLangerSimpleGraph.Adj :=
+  fun l₁ l₂ => inferInstanceAs (Decidable (dualLangerAdjBool l₁ l₂))
+
+/-! ## Basic properties — same parameters as Langer -/
+
+/-- The dual Langer graph is 6-regular: each line meets 6 other lines. -/
+theorem dualLanger_regular :
+    ∀ v : Fin 63, (Finset.univ.filter fun w => dualLangerSimpleGraph.Adj v w).card = 6 := by
+  native_decide
+
+/-- The dual Langer graph has 189 undirected edges. -/
+theorem dualLanger_edges :
+    (Finset.univ.filter fun p : Fin 63 × Fin 63 =>
+      p.1 < p.2 ∧ dualLangerSimpleGraph.Adj p.1 p.2).card = 189 := by
+  native_decide
+
+/-- λ = 1: each pair of concurrent lines shares exactly 1 common neighbor. -/
+theorem dualLanger_lambda :
+    ∀ l₁ l₂ : Fin 63, dualLangerSimpleGraph.Adj l₁ l₂ →
+      (Finset.univ.filter fun w =>
+        dualLangerSimpleGraph.Adj l₁ w ∧ dualLangerSimpleGraph.Adj l₂ w).card = 1 := by
+  native_decide
+
+/-! ## The duality: both graphs are halved Tutte 12-cage
+
+The Langer graph is the distance-2 graph on points (Tutte12Cage.lean).
+The dual Langer graph is the distance-2 graph on lines. -/
+
+/-- The dual Langer graph equals the distance-2 graph of the Tutte 12-cage
+    restricted to line vertices (indices 63–125), mirroring the Langer graph's
+    relationship to point vertices (indices 0–62). -/
+theorem dualLanger_eq_tutte12_distance2_lines :
+    ∀ l₁ l₂ : Fin 63,
+      dualLangerSimpleGraph.Adj l₁ l₂ ↔ dualLangerAdjBool l₁ l₂ := by
+  intro l₁ l₂; rfl
+
+/-! ## The distinguishing invariant: d₃-subgraph connectivity
+
+For a graph G on Fin n, the **d₃-subgraph** at vertex v is the subgraph
+induced on vertices at graph distance exactly 3 from v. We compute this
+via BFS and check connectivity. -/
+
+section BFS
+
+/-- BFS neighborhood expansion: the set of vertices reachable in exactly
+    one step from a set S, excluding vertices in `visited`. -/
+def bfsExpand (G : SimpleGraph (Fin n)) [DecidableRel G.Adj]
+    (S visited : Finset (Fin n)) : Finset (Fin n) :=
+  S.biUnion (fun v => Finset.univ.filter (G.Adj v)) \ visited
+
+/-- BFS layer computation: returns (layer_k, all_visited_through_k). -/
+def bfsLayers (G : SimpleGraph (Fin n)) [DecidableRel G.Adj]
+    (v : Fin n) : (depth : Nat) → Finset (Fin n) × Finset (Fin n)
+  | 0 => ({v}, {v})
+  | k + 1 =>
+    let (prevLayer, prevVisited) := bfsLayers G v k
+    let nextLayer := bfsExpand G prevLayer prevVisited
+    (nextLayer, prevVisited ∪ nextLayer)
+
+/-- The set of vertices at graph distance exactly `d` from `v`, computed by BFS. -/
+def distanceLayer (G : SimpleGraph (Fin n)) [DecidableRel G.Adj]
+    (v : Fin n) (d : Nat) : Finset (Fin n) :=
+  (bfsLayers G v d).1
+
+/-- Connectivity check via BFS on a subgraph induced by a vertex set.
+    Returns `true` iff the induced subgraph is connected (or empty). -/
+def isInducedConnectedBool (G : SimpleGraph (Fin n)) [DecidableRel G.Adj]
+    (S : Finset (Fin n)) : Bool :=
+  if h : S = ∅ then true
+  else
+    -- BFS from the first vertex of S, restricted to S
+    let start := S.min' (Finset.nonempty_of_ne_empty h)
+    let rec bfsReach (frontier visited : Finset (Fin n)) (fuel : Nat) : Finset (Fin n) :=
+      match fuel with
+      | 0 => visited
+      | fuel + 1 =>
+        let next := frontier.biUnion (fun v =>
+          S.filter (fun w => v ≠ w && G.Adj v w)) \ visited
+        if next = ∅ then visited
+        else bfsReach next (visited ∪ next) fuel
+    let reached := bfsReach {start} {start} S.card
+    reached.card == S.card
+
+/-- Is the d₃-subgraph at vertex v connected? -/
+def isD3ConnectedBool (G : SimpleGraph (Fin n)) [DecidableRel G.Adj]
+    (v : Fin n) : Bool :=
+  isInducedConnectedBool G (distanceLayer G v 3)
+
+/-- Number of connected components in the d₃-subgraph, computed by
+    iterating BFS until all vertices are assigned a component. -/
+def numD3Components (G : SimpleGraph (Fin n)) [DecidableRel G.Adj]
+    (v : Fin n) : Nat :=
+  let S := distanceLayer G v 3
+  let rec countComps (remaining : Finset (Fin n)) (fuel : Nat) : Nat :=
+    match fuel with
+    | 0 => 0
+    | fuel + 1 =>
+      if h : remaining = ∅ then 0
+      else
+        let start := remaining.min' (Finset.nonempty_of_ne_empty h)
+        let rec bfsComp (frontier visited : Finset (Fin n)) (f2 : Nat) : Finset (Fin n) :=
+          match f2 with
+          | 0 => visited
+          | f2 + 1 =>
+            let next := frontier.biUnion (fun w =>
+              remaining.filter (fun u => w ≠ u && G.Adj w u)) \ visited
+            if next = ∅ then visited
+            else bfsComp next (visited ∪ next) f2
+        let comp := bfsComp {start} {start} remaining.card
+        1 + countComps (remaining \ comp) fuel
+  countComps S S.card
+
+/-- BFS reach within a vertex set S: starting from `frontier`, expand
+    to neighbors in S not yet visited, for `fuel` steps.
+    Unlike `isInducedConnectedBool`, this is a top-level named function
+    suitable for proving isomorphism invariance by induction. -/
+def inducedBfsReach (G : SimpleGraph (Fin n)) [DecidableRel G.Adj]
+    (S frontier visited : Finset (Fin n)) : Nat → Finset (Fin n)
+  | 0 => visited
+  | fuel + 1 =>
+    let next := frontier.biUnion (fun v =>
+      S.filter (fun w => v ≠ w ∧ G.Adj v w)) \ visited
+    if next = ∅ then visited
+    else inducedBfsReach G S next (visited ∪ next) fuel
+
+/-- All-pairs reachability within a vertex set S: every pair u, v ∈ S
+    can reach each other via BFS restricted to S.
+    This is a **starting-vertex-independent** connectivity predicate,
+    unlike `isInducedConnectedBool` which starts from `S.min'`. -/
+def AllPairsReachable (G : SimpleGraph (Fin n)) [DecidableRel G.Adj]
+    (S : Finset (Fin n)) : Prop :=
+  ∀ u ∈ S, ∀ v ∈ S, v ∈ inducedBfsReach G S {u} {u} S.card
+
+instance decAllPairsReachable (G : SimpleGraph (Fin n)) [DecidableRel G.Adj]
+    (S : Finset (Fin n)) : Decidable (AllPairsReachable G S) :=
+  Finset.decidableBAll _ _
+
+end BFS
+
+/-! ## Computational verification of d₃-connectivity
+
+We verify at vertex 0 (fast) and also at all 63 vertices (the universal
+quantifier is needed for the non-isomorphism proof). -/
+
+/-- The Langer graph has 32 vertices at distance 3 from vertex 0. -/
+theorem langer_d3_size :
+    (distanceLayer langerSimpleGraph 0 3).card = 32 := by
+  native_decide
+
+/-- The dual Langer graph has 32 vertices at distance 3 from vertex 0. -/
+theorem dualLanger_d3_size :
+    (distanceLayer dualLangerSimpleGraph 0 3).card = 32 := by
+  native_decide
+
+/-- The d₃-subgraph of the Langer graph is **connected** at every vertex. -/
+theorem langer_d3_connected :
+    ∀ v : Fin 63, isD3ConnectedBool langerSimpleGraph v = true := by
+  native_decide
+
+/-- The d₃-subgraph of the dual Langer graph is **disconnected** at every vertex.
+    This is the key computational certificate for non-isomorphism. -/
+theorem dualLanger_d3_not_connected :
+    ∀ v : Fin 63, isD3ConnectedBool dualLangerSimpleGraph v = false := by
+  native_decide
+
+/-- The Langer d₃-subgraph has exactly 1 connected component at every vertex. -/
+theorem langer_d3_num_components :
+    ∀ v : Fin 63, numD3Components langerSimpleGraph v = 1 := by
+  native_decide
+
+/-- The dual Langer d₃-subgraph has exactly 2 connected components at every vertex. -/
+theorem dualLanger_d3_num_components :
+    ∀ v : Fin 63, numD3Components dualLangerSimpleGraph v = 2 := by
+  native_decide
+
+/-! ## All-pairs reachability: starting-vertex-independent connectivity
+
+The `isAllPairsReachable` predicate checks every pair, so it doesn't
+depend on `S.min'`. This makes it suitable for proving isomorphism
+invariance without needing a BFS-start-independence lemma. -/
+
+set_option maxHeartbeats 800000 in
+/-- The Langer d₃-subgraph is all-pairs reachable at every vertex.
+    Every pair of d₃-vertices can reach each other via BFS within d₃. -/
+theorem langer_d3_allPairs :
+    ∀ v : Fin 63, AllPairsReachable langerSimpleGraph
+      (distanceLayer langerSimpleGraph v 3) := by
+  native_decide
+
+set_option maxHeartbeats 800000 in
+/-- The dual Langer d₃-subgraph is NOT all-pairs reachable at any vertex.
+    Some pair of d₃-vertices cannot reach each other via BFS within d₃. -/
+theorem dualLanger_d3_not_allPairs :
+    ∀ v : Fin 63, ¬ AllPairsReachable dualLangerSimpleGraph
+      (distanceLayer dualLangerSimpleGraph v 3) := by
+  native_decide
+
+/-! ## Non-isomorphism
+
+The d₃-subgraph connectivity is a graph invariant: an isomorphism φ : G ≃g H
+maps BFS layers to BFS layers (since it preserves adjacency), hence maps
+d₃-vertices to d₃-vertices, and preserves connectivity of the induced
+d₃-subgraph. Since the Langer graph has connected d₃-subgraphs at every
+vertex and the dual Langer has disconnected ones, no isomorphism can exist.
+
+We prove the invariance by induction on BFS depth: φ commutes with
+`bfsExpand` because it bijects neighbors and commutes with set difference
+(being injective). -/
+
+section NonIsomorphism
+
+variable {n : Nat} {G H : SimpleGraph (Fin n)}
+  [DecidableRel G.Adj] [DecidableRel H.Adj]
+
+/-- A graph isomorphism commutes with neighbor-set biUnion. -/
+private theorem iso_biUnion_neighbors (φ : G ≃g H) (S : Finset (Fin n)) :
+    (S.biUnion (fun v => Finset.univ.filter (G.Adj v))).image φ =
+    (S.image φ).biUnion (fun v => Finset.univ.filter (H.Adj v)) := by
+  ext w
+  simp only [Finset.mem_image, Finset.mem_biUnion, Finset.mem_filter, Finset.mem_univ, true_and]
+  constructor
+  · rintro ⟨u, ⟨v, hv, hvadj⟩, rfl⟩
+    exact ⟨φ v, ⟨v, hv, rfl⟩, φ.map_adj_iff.mpr hvadj⟩
+  · rintro ⟨_, ⟨v, hv, rfl⟩, hadj⟩
+    exact ⟨φ.symm w, ⟨v, hv, by rwa [← φ.map_adj_iff, φ.apply_symm_apply]⟩,
+           φ.apply_symm_apply w⟩
+
+/-- A graph isomorphism commutes with `bfsExpand`. -/
+private theorem iso_bfsExpand (φ : G ≃g H) (S visited : Finset (Fin n)) :
+    (bfsExpand G S visited).image φ = bfsExpand H (S.image φ) (visited.image φ) := by
+  unfold bfsExpand
+  rw [Finset.image_sdiff _ _ φ.injective]
+  congr 1
+  exact iso_biUnion_neighbors φ S
+
+/-- A graph isomorphism commutes with `bfsLayers`. -/
+private theorem iso_bfsLayers (φ : G ≃g H) (v : Fin n) (d : Nat) :
+    ((bfsLayers G v d).1).image φ = (bfsLayers H (φ v) d).1 ∧
+    ((bfsLayers G v d).2).image φ = (bfsLayers H (φ v) d).2 := by
+  induction d with
+  | zero => simp [bfsLayers, Finset.image_singleton]
+  | succ d ih =>
+    simp only [bfsLayers]
+    have hexp := iso_bfsExpand φ (bfsLayers G v d).1 (bfsLayers G v d).2
+    rw [ih.1, ih.2] at hexp
+    exact ⟨hexp, by rw [Finset.image_union, hexp, ih.2]⟩
+
+/-- A graph isomorphism commutes with `distanceLayer`. -/
+theorem iso_distanceLayer (φ : G ≃g H) (v : Fin n) (d : Nat) :
+    (distanceLayer G v d).image φ = distanceLayer H (φ v) d :=
+  (iso_bfsLayers φ v d).1
+
+/-- A graph isomorphism commutes with restricted neighbor biUnion within S. -/
+private theorem iso_induced_neighbors (φ : G ≃g H)
+    (S frontier : Finset (Fin n)) :
+    (frontier.biUnion (fun v => S.filter (fun w => v ≠ w ∧ G.Adj v w))).image φ =
+    (frontier.image φ).biUnion (fun v =>
+      (S.image φ).filter (fun w => v ≠ w ∧ H.Adj v w)) := by
+  ext w
+  simp only [Finset.mem_image, Finset.mem_biUnion, Finset.mem_filter]
+  constructor
+  · rintro ⟨u, ⟨v, hv, hu_S, hne, hadj⟩, rfl⟩
+    exact ⟨φ v, ⟨v, hv, rfl⟩, Finset.mem_image_of_mem φ hu_S,
+           φ.injective.ne hne, φ.map_adj_iff.mpr hadj⟩
+  · rintro ⟨_, ⟨v, hv, rfl⟩, hw_S', hne, hadj⟩
+    rw [Finset.mem_image] at hw_S'
+    obtain ⟨u, hu_S, rfl⟩ := hw_S'
+    exact ⟨u, ⟨v, hv, hu_S, fun h => hne (congrArg φ h),
+           φ.map_adj_iff.mp hadj⟩, rfl⟩
+
+/-- A graph isomorphism commutes with `inducedBfsReach`.
+
+    This is the key structural lemma: φ maps the BFS-within-S reach set
+    bijectively to the corresponding reach set in the image graph.
+    Proved by induction on fuel, using `iso_induced_neighbors` at each step. -/
+private theorem iso_inducedBfsReach (φ : G ≃g H) (S frontier visited : Finset (Fin n))
+    (fuel : Nat) :
+    (inducedBfsReach G S frontier visited fuel).image φ =
+    inducedBfsReach H (S.image φ) (frontier.image φ) (visited.image φ) fuel := by
+  induction fuel generalizing frontier visited with
+  | zero => simp [inducedBfsReach]
+  | succ fuel ih =>
+    simp only [inducedBfsReach]
+    -- Abbreviate the next frontiers
+    set nextG := frontier.biUnion (fun v =>
+      S.filter (fun w => v ≠ w ∧ G.Adj v w)) \ visited with hNextG_def
+    set nextH := (frontier.image φ).biUnion (fun v =>
+      (S.image φ).filter (fun w => v ≠ w ∧ H.Adj v w)) \ (visited.image φ) with hNextH_def
+    -- Key: φ maps nextG to nextH
+    have hcomm : nextG.image φ = nextH := by
+      simp only [hNextG_def, hNextH_def]
+      rw [Finset.image_sdiff _ _ φ.injective]
+      congr 1
+      exact iso_induced_neighbors φ S frontier
+    -- Both sides branch on emptiness, which agrees under φ
+    by_cases h : nextG = ∅
+    · -- Next frontier is empty: both sides return visited
+      have hH : nextH = ∅ := by
+        rw [← hcomm, Finset.image_eq_empty]; exact h
+      simp [h, hH]
+    · -- Next frontier is non-empty: recurse with updated sets
+      have hH : nextH ≠ ∅ := by
+        intro habs; rw [← hcomm, Finset.image_eq_empty] at habs; exact h habs
+      simp only [h, ↓reduceIte, hH]
+      rw [← hcomm, Finset.image_union]
+      exact ih nextG (visited ∪ nextG)
+
+/-- A graph isomorphism preserves `AllPairsReachable`.
+
+    The key property: `AllPairsReachable` quantifies over ALL pairs in S,
+    so it doesn't depend on `S.min'`. Under the bijection φ|_S : S → S.image φ,
+    each pair (u, v) maps to (φ u, φ v), and reachability is preserved by
+    `iso_inducedBfsReach`. -/
+private theorem iso_AllPairsReachable (φ : G ≃g H) (S : Finset (Fin n)) :
+    AllPairsReachable G S ↔ AllPairsReachable H (S.image φ) := by
+  have hcard : (S.image φ).card = S.card :=
+    Finset.card_image_of_injective S φ.injective
+  -- Helper: iso_inducedBfsReach with singletons simplified
+  have key : ∀ u, (inducedBfsReach G S {u} {u} S.card).image φ =
+      inducedBfsReach H (S.image φ) {φ u} {φ u} S.card := by
+    intro u
+    have := iso_inducedBfsReach φ S {u} {u} S.card
+    rwa [Finset.image_singleton, Finset.image_singleton] at this
+  constructor
+  · -- Forward: if all pairs reachable in G|S, then in H|S'
+    intro h u' hu' v' hv'
+    rw [Finset.mem_image] at hu' hv'
+    obtain ⟨u, hu, rfl⟩ := hu'
+    obtain ⟨v, hv, rfl⟩ := hv'
+    rw [hcard, ← key]
+    exact Finset.mem_image_of_mem φ (h u hu v hv)
+  · -- Backward: if all pairs reachable in H|S', then in G|S
+    intro h u hu v hv
+    have hmem := h (φ u) (Finset.mem_image_of_mem φ hu) (φ v) (Finset.mem_image_of_mem φ hv)
+    rw [hcard, ← key, Finset.mem_image] at hmem
+    obtain ⟨w, hw, hφw⟩ := hmem
+    rwa [φ.injective hφw] at hw
+
+/-- The Langer and dual Langer graphs are **not isomorphic**.
+
+    **Proof**: The `AllPairsReachable` predicate is a graph invariant:
+    it checks ALL pairs via BFS within the d₃-set, making it independent
+    of BFS starting vertex. We prove φ commutes with BFS reach sets
+    (`iso_inducedBfsReach`), hence preserves all-pairs reachability.
+
+    Computational verification shows this predicate holds for the Langer
+    graph and fails for the dual Langer graph at every vertex.
+    Under any hypothetical isomorphism φ, the d₃-set at 0 maps to the
+    d₃-set at φ(0), but their all-pairs reachability disagrees. -/
+theorem langer_not_iso_dualLanger :
+    IsEmpty (langerSimpleGraph ≃g dualLangerSimpleGraph) := by
+  rw [isEmpty_iff]
+  intro φ
+  have h1 := langer_d3_allPairs 0
+  have h2 := dualLanger_d3_not_allPairs (φ 0)
+  have h3 : AllPairsReachable dualLangerSimpleGraph
+      (distanceLayer dualLangerSimpleGraph (φ 0) 3) := by
+    rw [← iso_distanceLayer φ 0 3]
+    exact (iso_AllPairsReachable φ _).mp h1
+  exact h2 h3
+
+end NonIsomorphism
diff --git a/Archive/LangerGraph.lean b/Archive/LangerGraph.lean
new file mode 100644
index 00000000000000..0dc97b8444dbe3
--- /dev/null
+++ b/Archive/LangerGraph.lean
@@ -0,0 +1,775 @@
+/-
+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.Data.ZMod.Basic
+import Mathlib.Data.Matrix.Basic
+import Mathlib.Data.Fin.VecNotation
+import Mathlib.Combinatorics.SimpleGraph.Basic
+import Mathlib.Combinatorics.SimpleGraph.Action
+import Mathlib.Combinatorics.SimpleGraph.Representation
+
+/-!
+# The Langer graph, the Tutte 12-cage, and the GH(2,2) ecosystem
+
+The **Langer graph** is the collinearity graph of the split Cayley hexagon GH(2,2),
+the unique generalized 6-gon over 𝔽₂. It has 63 vertices (the points of the parabolic
+quadric Q(6,2) in PG(6,2)), is 6-regular with 189 edges, and is the unique
+distance-regular graph with intersection array {6, 4, 4; 1, 1, 3}.
+
+The **Tutte 12-cage** is the incidence graph of GH(2,2): 126 vertices
+(63 points + 63 lines), 189 edges, girth 12. It is semisymmetric — edge-transitive
+but not vertex-transitive — because no polarity exists for GH(2,2) over 𝔽₂.
+
+The main result `langer_eq_tutte12_distance2` proves that the Langer graph (defined
+algebraically via the Zorn product on Q(6,2)) equals the distance-2 graph of the
+Tutte 12-cage restricted to points (defined combinatorially from the edge list).
+The proof uses G₂(2) transitivity: both graphs are invariant under two generators
+of G₂(2), so they agree everywhere if they agree at vertex 0.
+
+## Main definitions
+
+* `langerSimpleGraph` — the Langer graph on `Fin 63`, via Zorn product
+* `tutte12CageGraph` — the Tutte 12-cage on `Fin 126`, via edge list
+* `Q62form` — the quadratic form Q(x) = x₀x₄ + x₁x₅ + x₂x₆ + x₃² on 𝔽₂⁷
+* `Q62_H` — the 7 × 63 parity-check matrix from Q(6,2)
+
+## Main results
+
+* `Q62_self_orthogonal` — H · Hᵀ = 0 over 𝔽₂
+* `langer_regular` — the Langer graph is 6-regular
+* `tutte12_bipartite` — the Tutte 12-cage is bipartite
+* `langer_eq_tutte12_distance2'` — algebraic Langer = geometric distance-2
+  (structural proof via G₂(2) transitivity)
+
+## Visualizations
+
+* [The Langer graph](https://raw.githubusercontent.com/RaggedR/symmetric-graphs/main/lean/named_graphs/langer-63v.jpg) — symmetry-aware drawing with 6-fold rotational layout
+* [The Tutte 12-cage](https://raw.githubusercontent.com/RaggedR/symmetric-graphs/main/lean/named_graphs/tutte-12cage.jpg) — incidence graph of GH(2,2)
+
+## References
+
+* Robin Langer, *Symmetric Graphs and their Quotients*, arXiv:1306.4798
+* Benson, *Minimal regular graphs of girth 8 and 12*, Canad. J. Math. 18 (1966)
+* Springer–Veldkamp, *Octonions, Jordan Algebras and Exceptional Groups*, §1.8
+-/
+
+set_option linter.style.nativeDecide false
+
+open Matrix
+
+/-! ## Part 1: The quadratic form Q(6,2) -/
+
+/-- The quadratic form Q(x) = x₀x₄ + x₁x₅ + x₂x₆ + x₃² on 𝔽₂⁷.
+Points of Q(6,2) are the nonzero vectors with Q(x) = 0. -/
+def Q62form (x : Fin 7 → ZMod 2) : ZMod 2 :=
+  x 0 * x 4 + x 1 * x 5 + x 2 * x 6 + x 3 * x 3
+
+/-- Convert a natural number (1..127) to its bit vector in 𝔽₂⁷. -/
+def toBitVec (n : Fin 128) : Fin 7 → ZMod 2 :=
+  fun i => if n.val / (2 ^ i.val) % 2 = 0 then 0 else 1
+
+/-- The list of indices (1..127) whose bit vectors lie on Q(6,2). -/
+def q62Indices : List (Fin 128) :=
+  (List.finRange 128).tail.filter fun n => Q62form (toBitVec n) = 0
+
+/-- Q(6,2) has exactly 63 points. -/
+theorem q62_card : q62Indices.length = 63 := by native_decide
+
+/-- Get the n-th point of Q(6,2) (as an index into Fin 128). -/
+def q62Point (j : Fin 63) : Fin 128 :=
+  q62Indices.get (j.cast (by native_decide))
+
+/-- The parity-check matrix: H[i][j] = (j-th Q(6,2) point)[i-th coordinate]. -/
+def Q62_H : Matrix (Fin 7) (Fin 63) (ZMod 2) :=
+  fun i j => toBitVec (q62Point j) i
+
+/-- **Self-orthogonality of Q(6,2)**: H · Hᵀ = 0 over 𝔽₂.
+The CSS condition: the code C = ker(H) contains its dual C⊥ = rowspan(H). -/
+theorem Q62_self_orthogonal : Q62_H * Q62_Hᵀ = (0 : Matrix (Fin 7) (Fin 7) (ZMod 2)) := by
+  native_decide
+
+/-! ## Part 2: The Langer graph via Zorn product -/
+
+/-- Adjacency test for the Langer graph via the Zorn product criterion.
+Returns `true` iff `i ≠ j` and all eight entries of M_x · M_y vanish,
+where M_x is the Zorn vector matrix of the split octonion algebra over 𝔽₂. -/
+def langerAdjBool (i j : Fin 63) : Bool :=
+  if i == j then false else
+  let x := toBitVec (q62Point i)
+  let y := toBitVec (q62Point j)
+  let α := x 3; let γ := y 3
+  (α * γ + x 0 * y 4 + x 1 * y 5 + x 2 * y 6 == 0) &&
+  (α * γ + x 4 * y 0 + x 5 * y 1 + x 6 * y 2 == 0) &&
+  (γ * x 0 + α * y 0 + x 5 * y 6 + x 6 * y 5 == 0) &&
+  (γ * x 1 + α * y 1 + x 6 * y 4 + x 4 * y 6 == 0) &&
+  (γ * x 2 + α * y 2 + x 4 * y 5 + x 5 * y 4 == 0) &&
+  (γ * x 4 + α * y 4 + x 1 * y 2 + x 2 * y 1 == 0) &&
+  (γ * x 5 + α * y 5 + x 2 * y 0 + x 0 * y 2 == 0) &&
+  (γ * x 6 + α * y 6 + x 0 * y 1 + x 1 * y 0 == 0)
+
+/-- The **Langer graph**: collinearity graph of the split Cayley hexagon GH(2,2)
+on the 63 points of Q(6,2). 6-regular, 189 edges, distance-regular with
+intersection array {6, 4, 4; 1, 1, 3}. Aut ≅ G₂(2) of order 12096. -/
+def langerSimpleGraph : SimpleGraph (Fin 63) where
+  Adj i j := langerAdjBool i j
+  symm i j := by simp only [langerAdjBool]; revert i j; native_decide
+  loopless := ⟨fun i => by simp only [langerAdjBool]; revert i; native_decide⟩
+
+instance langerDecAdj : DecidableRel langerSimpleGraph.Adj :=
+  fun i j => inferInstanceAs (Decidable (langerAdjBool i j))
+
+/-- The Langer graph is 6-regular. -/
+theorem langer_regular :
+    ∀ v : Fin 63, (Finset.univ.filter fun w => langerSimpleGraph.Adj v w).card = 6 := by
+  native_decide
+
+/-- The Langer graph has 189 undirected edges. -/
+theorem langer_edges :
+    (Finset.univ.filter fun p : Fin 63 × Fin 63 =>
+      p.1 < p.2 ∧ langerSimpleGraph.Adj p.1 p.2).card = 189 := by
+  native_decide
+
+/-! ## Part 3: The Tutte 12-cage -/
+
+/-- Edge list for the Tutte 12-cage (189 edges, 0-indexed).
+Vertices 0–62 are points of GH(2,2), vertices 63–125 are lines.
+Every edge connects a point to a line (bipartite). -/
+private def tutte12Edges : Array (Fin 126 × Fin 126) := #[
+  (0,63), (0,64), (0,65), (1,66), (1,67), (1,68),
+  (2,69), (2,70), (2,71), (3,72), (3,73), (3,74),
+  (4,75), (4,76), (4,77), (5,78), (5,79), (5,80),
+  (6,81), (6,82), (6,83), (7,66), (7,72), (7,78),
+  (8,66), (8,84), (8,85), (9,72), (9,86), (9,87),
+  (10,78), (10,88), (10,89), (11,90), (11,91), (11,92),
+  (12,93), (12,94), (12,95), (13,96), (13,97), (13,98),
+  (14,99), (14,100), (14,101), (15,63), (15,73), (15,75),
+  (16,63), (16,102), (16,103), (17,73), (17,90), (17,96),
+  (18,75), (18,104), (18,105), (19,86), (19,106), (19,107),
+  (20,99), (20,108), (20,109), (21,87), (21,110), (21,111),
+  (22,93), (22,112), (22,113), (23,69), (23,74), (23,81),
+  (24,69), (24,114), (24,115), (25,74), (25,93), (25,99),
+  (26,81), (26,116), (26,117), (27,96), (27,118), (27,119),
+  (28,87), (28,120), (28,121), (29,90), (29,122), (29,123),
+  (30,86), (30,124), (30,125), (31,64), (31,67), (31,70),
+  (32,64), (32,106), (32,108), (33,67), (33,91), (33,94),
+  (34,70), (34,118), (34,120), (35,84), (35,102), (35,114),
+  (36,100), (36,103), (36,124), (37,85), (37,112), (37,122),
+  (38,97), (38,110), (38,115), (39,68), (39,76), (39,82),
+  (40,68), (40,97), (40,100), (41,76), (41,107), (41,113),
+  (42,82), (42,121), (42,123), (43,94), (43,104), (43,125),
+  (44,91), (44,111), (44,116), (45,85), (45,105), (45,117),
+  (46,84), (46,109), (46,119), (47,65), (47,79), (47,83),
+  (48,65), (48,110), (48,112), (49,79), (49,92), (49,101),
+  (50,83), (50,119), (50,125), (51,88), (51,108), (51,123),
+  (52,98), (52,106), (52,117), (53,89), (53,103), (53,116),
+  (54,95), (54,102), (54,121), (55,71), (55,77), (55,80),
+  (56,71), (56,122), (56,124), (57,77), (57,109), (57,111),
+  (58,80), (58,95), (58,98), (59,101), (59,105), (59,120),
+  (60,89), (60,113), (60,118), (61,88), (61,104), (61,115),
+  (62,92), (62,107), (62,114)]
+
+def tutte12AdjBool (u v : Fin 126) : Bool :=
+  tutte12Edges.any fun (a, b) => (u == a && v == b) || (u == b && v == a)
+
+/-- The **Tutte 12-cage**: incidence graph of GH(2,2) on 126 vertices.
+3-regular, 189 edges, girth 12. Semisymmetric (edge-transitive, not vertex-transitive). -/
+def tutte12CageGraph : SimpleGraph (Fin 126) where
+  Adj u v := tutte12AdjBool u v
+  symm u v := by simp only [tutte12AdjBool]; revert u v; native_decide
+  loopless := ⟨fun u => by simp only [tutte12AdjBool]; revert u; native_decide⟩
+
+instance tutte12DecAdj : DecidableRel tutte12CageGraph.Adj :=
+  fun u v => inferInstanceAs (Decidable (tutte12AdjBool u v))
+
+/-- The Tutte 12-cage is 3-regular. -/
+theorem tutte12_regular :
+    ∀ v : Fin 126, (Finset.univ.filter fun w => tutte12CageGraph.Adj v w).card = 3 := by
+  native_decide
+
+/-- The bipartition: point (< 63) or line (≥ 63). -/
+def tutte12Side (v : Fin 126) : Fin 2 :=
+  if v.val < 63 then 0 else 1
+
+/-- The Tutte 12-cage is bipartite: every edge connects a point to a line. -/
+theorem tutte12_bipartite :
+    ∀ u v : Fin 126, tutte12CageGraph.Adj u v → tutte12Side u ≠ tutte12Side v := by
+  native_decide
+
+/-! ## Part 4: Distance-2 adjacency on points -/
+
+/-- Distance-2 adjacency on points: p ~ q iff they share a line vertex
+in the Tutte 12-cage. -/
+def tutte12Distance2Bool (p q : Fin 63) : Bool :=
+  p != q &&
+  let pv : Fin 126 := ⟨p.val, by omega⟩
+  let qv : Fin 126 := ⟨q.val, by omega⟩
+  (List.finRange 63).any fun l =>
+    let lv : Fin 126 := ⟨l.val + 63, by omega⟩
+    tutte12AdjBool pv lv && tutte12AdjBool qv lv
+
+/-! ## Part 5: G₂(2) generators and invariance -/
+
+private def g2gen1Fwd : Array (Fin 63) := #[
+  ⟨1, by omega⟩, ⟨3, by omega⟩, ⟨5, by omega⟩, ⟨2, by omega⟩, ⟨0, by omega⟩,
+  ⟨6, by omega⟩, ⟨4, by omega⟩, ⟨23, by omega⟩, ⟨25, by omega⟩, ⟨24, by omega⟩,
+  ⟨26, by omega⟩, ⟨28, by omega⟩, ⟨30, by omega⟩, ⟨27, by omega⟩, ⟨29, by omega⟩,
+  ⟨31, by omega⟩, ⟨33, by omega⟩, ⟨34, by omega⟩, ⟨32, by omega⟩, ⟨35, by omega⟩,
+  ⟨37, by omega⟩, ⟨38, by omega⟩, ⟨36, by omega⟩, ⟨55, by omega⟩, ⟨58, by omega⟩,
+  ⟨56, by omega⟩, ⟨57, by omega⟩, ⟨60, by omega⟩, ⟨61, by omega⟩, ⟨59, by omega⟩,
+  ⟨62, by omega⟩, ⟨7, by omega⟩, ⟨8, by omega⟩, ⟨9, by omega⟩, ⟨10, by omega⟩,
+  ⟨12, by omega⟩, ⟨11, by omega⟩, ⟨14, by omega⟩, ⟨13, by omega⟩, ⟨15, by omega⟩,
+  ⟨17, by omega⟩, ⟨16, by omega⟩, ⟨18, by omega⟩, ⟨19, by omega⟩, ⟨21, by omega⟩,
+  ⟨20, by omega⟩, ⟨22, by omega⟩, ⟨39, by omega⟩, ⟨40, by omega⟩, ⟨42, by omega⟩,
+  ⟨41, by omega⟩, ⟨45, by omega⟩, ⟨46, by omega⟩, ⟨44, by omega⟩, ⟨43, by omega⟩,
+  ⟨47, by omega⟩, ⟨49, by omega⟩, ⟨48, by omega⟩, ⟨50, by omega⟩, ⟨51, by omega⟩,
+  ⟨53, by omega⟩, ⟨52, by omega⟩, ⟨54, by omega⟩]
+
+private def g2gen1Inv : Array (Fin 63) := #[
+  ⟨4, by omega⟩, ⟨0, by omega⟩, ⟨3, by omega⟩, ⟨1, by omega⟩, ⟨6, by omega⟩,
+  ⟨2, by omega⟩, ⟨5, by omega⟩, ⟨31, by omega⟩, ⟨32, by omega⟩, ⟨33, by omega⟩,
+  ⟨34, by omega⟩, ⟨36, by omega⟩, ⟨35, by omega⟩, ⟨38, by omega⟩, ⟨37, by omega⟩,
+  ⟨39, by omega⟩, ⟨41, by omega⟩, ⟨40, by omega⟩, ⟨42, by omega⟩, ⟨43, by omega⟩,
+  ⟨45, by omega⟩, ⟨44, by omega⟩, ⟨46, by omega⟩, ⟨7, by omega⟩, ⟨9, by omega⟩,
+  ⟨8, by omega⟩, ⟨10, by omega⟩, ⟨13, by omega⟩, ⟨11, by omega⟩, ⟨14, by omega⟩,
+  ⟨12, by omega⟩, ⟨15, by omega⟩, ⟨18, by omega⟩, ⟨16, by omega⟩, ⟨17, by omega⟩,
+  ⟨19, by omega⟩, ⟨22, by omega⟩, ⟨20, by omega⟩, ⟨21, by omega⟩, ⟨47, by omega⟩,
+  ⟨48, by omega⟩, ⟨50, by omega⟩, ⟨49, by omega⟩, ⟨54, by omega⟩, ⟨53, by omega⟩,
+  ⟨51, by omega⟩, ⟨52, by omega⟩, ⟨55, by omega⟩, ⟨57, by omega⟩, ⟨56, by omega⟩,
+  ⟨58, by omega⟩, ⟨59, by omega⟩, ⟨61, by omega⟩, ⟨60, by omega⟩, ⟨62, by omega⟩,
+  ⟨23, by omega⟩, ⟨25, by omega⟩, ⟨26, by omega⟩, ⟨24, by omega⟩, ⟨29, by omega⟩,
+  ⟨27, by omega⟩, ⟨28, by omega⟩, ⟨30, by omega⟩]
+
+private def g2gen2Fwd : Array (Fin 63) := #[
+  ⟨10, by omega⟩, ⟨20, by omega⟩, ⟨29, by omega⟩, ⟨49, by omega⟩, ⟨55, by omega⟩,
+  ⟨36, by omega⟩, ⟨44, by omega⟩, ⟨14, by omega⟩, ⟨25, by omega⟩, ⟨59, by omega⟩,
+  ⟨40, by omega⟩, ⟨0, by omega⟩, ⟨19, by omega⟩, ⟨50, by omega⟩, ⟨35, by omega⟩,
+  ⟨5, by omega⟩, ⟨7, by omega⟩, ⟨47, by omega⟩, ⟨58, by omega⟩, ⟨18, by omega⟩,
+  ⟨24, by omega⟩, ⟨34, by omega⟩, ⟨41, by omega⟩, ⟨11, by omega⟩, ⟨17, by omega⟩,
+  ⟨62, by omega⟩, ⟨33, by omega⟩, ⟨6, by omega⟩, ⟨28, by omega⟩, ⟨48, by omega⟩,
+  ⟨45, by omega⟩, ⟨51, by omega⟩, ⟨61, by omega⟩, ⟨32, by omega⟩, ⟨42, by omega⟩,
+  ⟨3, by omega⟩, ⟨8, by omega⟩, ⟨22, by omega⟩, ⟨27, by omega⟩, ⟨57, by omega⟩,
+  ⟨46, by omega⟩, ⟨4, by omega⟩, ⟨21, by omega⟩, ⟨52, by omega⟩, ⟨31, by omega⟩,
+  ⟨12, by omega⟩, ⟨23, by omega⟩, ⟨53, by omega⟩, ⟨60, by omega⟩, ⟨16, by omega⟩,
+  ⟨26, by omega⟩, ⟨38, by omega⟩, ⟨43, by omega⟩, ⟨1, by omega⟩, ⟨9, by omega⟩,
+  ⟨56, by omega⟩, ⟨37, by omega⟩, ⟨2, by omega⟩, ⟨30, by omega⟩, ⟨54, by omega⟩,
+  ⟨39, by omega⟩, ⟨13, by omega⟩, ⟨15, by omega⟩]
+
+private def g2gen2Inv : Array (Fin 63) := #[
+  ⟨11, by omega⟩, ⟨53, by omega⟩, ⟨57, by omega⟩, ⟨35, by omega⟩, ⟨41, by omega⟩,
+  ⟨15, by omega⟩, ⟨27, by omega⟩, ⟨16, by omega⟩, ⟨36, by omega⟩, ⟨54, by omega⟩,
+  ⟨0, by omega⟩, ⟨23, by omega⟩, ⟨45, by omega⟩, ⟨61, by omega⟩, ⟨7, by omega⟩,
+  ⟨62, by omega⟩, ⟨49, by omega⟩, ⟨24, by omega⟩, ⟨19, by omega⟩, ⟨12, by omega⟩,
+  ⟨1, by omega⟩, ⟨42, by omega⟩, ⟨37, by omega⟩, ⟨46, by omega⟩, ⟨20, by omega⟩,
+  ⟨8, by omega⟩, ⟨50, by omega⟩, ⟨38, by omega⟩, ⟨28, by omega⟩, ⟨2, by omega⟩,
+  ⟨58, by omega⟩, ⟨44, by omega⟩, ⟨33, by omega⟩, ⟨26, by omega⟩, ⟨21, by omega⟩,
+  ⟨14, by omega⟩, ⟨5, by omega⟩, ⟨56, by omega⟩, ⟨51, by omega⟩, ⟨60, by omega⟩,
+  ⟨10, by omega⟩, ⟨22, by omega⟩, ⟨34, by omega⟩, ⟨52, by omega⟩, ⟨6, by omega⟩,
+  ⟨30, by omega⟩, ⟨40, by omega⟩, ⟨17, by omega⟩, ⟨29, by omega⟩, ⟨3, by omega⟩,
+  ⟨13, by omega⟩, ⟨31, by omega⟩, ⟨43, by omega⟩, ⟨47, by omega⟩, ⟨59, by omega⟩,
+  ⟨4, by omega⟩, ⟨55, by omega⟩, ⟨39, by omega⟩, ⟨18, by omega⟩, ⟨9, by omega⟩,
+  ⟨48, by omega⟩, ⟨32, by omega⟩, ⟨25, by omega⟩]
+
+private theorem g2gen1Fwd_size : g2gen1Fwd.size = 63 := by native_decide
+private theorem g2gen1Inv_size : g2gen1Inv.size = 63 := by native_decide
+private theorem g2gen2Fwd_size : g2gen2Fwd.size = 63 := by native_decide
+private theorem g2gen2Inv_size : g2gen2Inv.size = 63 := by native_decide
+
+/-- First generator of G₂(2): order 7, from companion matrix of x³ + x + 1. -/
+def g2gen1 : Equiv.Perm (Fin 63) where
+  toFun i := g2gen1Fwd[i.val]'(by have := g2gen1Fwd_size; omega)
+  invFun i := g2gen1Inv[i.val]'(by have := g2gen1Inv_size; omega)
+  left_inv := by intro i; revert i; native_decide
+  right_inv := by intro i; revert i; native_decide
+
+/-- Second generator of G₂(2): order 6, maps vertex 0 → 10. -/
+def g2gen2 : Equiv.Perm (Fin 63) where
+  toFun i := g2gen2Fwd[i.val]'(by have := g2gen2Fwd_size; omega)
+  invFun i := g2gen2Inv[i.val]'(by have := g2gen2Inv_size; omega)
+  left_inv := by intro i; revert i; native_decide
+  right_inv := by intro i; revert i; native_decide
+
+/-- σ₁ preserves Langer adjacency. -/
+theorem g2gen1_langer_inv :
+    ∀ i j : Fin 63,
+      langerSimpleGraph.Adj i j ↔ langerSimpleGraph.Adj (g2gen1 i) (g2gen1 j) := by
+  native_decide
+
+/-- σ₂ preserves Langer adjacency. -/
+theorem g2gen2_langer_inv :
+    ∀ i j : Fin 63,
+      langerSimpleGraph.Adj i j ↔ langerSimpleGraph.Adj (g2gen2 i) (g2gen2 j) := by
+  native_decide
+
+/-- σ₁ preserves distance-2 adjacency. -/
+theorem g2gen1_dist2_inv :
+    ∀ p q : Fin 63,
+      tutte12Distance2Bool p q = tutte12Distance2Bool (g2gen1 p) (g2gen1 q) := by
+  native_decide
+
+/-- σ₂ preserves distance-2 adjacency. -/
+theorem g2gen2_dist2_inv :
+    ∀ p q : Fin 63,
+      tutte12Distance2Bool p q = tutte12Distance2Bool (g2gen2 p) (g2gen2 q) := by
+  native_decide
+
+/-! ## Part 6: Word induction (structural, no native_decide) -/
+
+/-- The four generator actions: σ₁, σ₁⁻¹, σ₂, σ₂⁻¹. -/
+def applyGen : Fin 4 → Equiv.Perm (Fin 63)
+  | 0 => g2gen1
+  | 1 => g2gen1.symm
+  | 2 => g2gen2
+  | 3 => g2gen2.symm
+
+/-- Apply a generator word (left-to-right). -/
+def applyWord : List (Fin 4) → Equiv.Perm (Fin 63)
+  | [] => Equiv.refl _
+  | g :: gs => (applyGen g).trans (applyWord gs)
+
+private theorem symm_preserves_langer (σ : Equiv.Perm (Fin 63))
+    (h : ∀ i j : Fin 63,
+      langerSimpleGraph.Adj i j ↔ langerSimpleGraph.Adj (σ i) (σ j))
+    (i j : Fin 63) :
+    langerSimpleGraph.Adj i j ↔ langerSimpleGraph.Adj (σ.symm i) (σ.symm j) := by
+  have := h (σ.symm i) (σ.symm j)
+  simp only [Equiv.apply_symm_apply] at this
+  exact this.symm
+
+private theorem applyGen_langer_inv (g : Fin 4) (i j : Fin 63) :
+    langerSimpleGraph.Adj i j ↔ langerSimpleGraph.Adj (applyGen g i) (applyGen g j) := by
+  fin_cases g <;> simp only [applyGen]
+  · exact g2gen1_langer_inv i j
+  · exact symm_preserves_langer g2gen1 (g2gen1_langer_inv) i j
+  · exact g2gen2_langer_inv i j
+  · exact symm_preserves_langer g2gen2 (g2gen2_langer_inv) i j
+
+/-- Any generator word preserves Langer adjacency (structural induction). -/
+theorem applyWord_langer_inv (w : List (Fin 4)) :
+    ∀ i j : Fin 63, langerSimpleGraph.Adj i j ↔
+      langerSimpleGraph.Adj (applyWord w i) (applyWord w j) := by
+  induction w with
+  | nil => intro i j; simp [applyWord]
+  | cons g gs ih =>
+    intro i j
+    simp only [applyWord, Equiv.trans_apply]
+    rw [applyGen_langer_inv g i j]
+    exact ih (applyGen g i) (applyGen g j)
+
+private theorem symm_preserves_dist2 (σ : Equiv.Perm (Fin 63))
+    (h : ∀ p q : Fin 63, tutte12Distance2Bool p q = tutte12Distance2Bool (σ p) (σ q))
+    (p q : Fin 63) :
+    tutte12Distance2Bool p q = tutte12Distance2Bool (σ.symm p) (σ.symm q) := by
+  have := h (σ.symm p) (σ.symm q)
+  simp only [Equiv.apply_symm_apply] at this
+  exact this.symm
+
+private theorem applyGen_dist2_inv (g : Fin 4) (p q : Fin 63) :
+    tutte12Distance2Bool p q = tutte12Distance2Bool (applyGen g p) (applyGen g q) := by
+  fin_cases g <;> simp only [applyGen]
+  · exact g2gen1_dist2_inv p q
+  · exact symm_preserves_dist2 g2gen1 (g2gen1_dist2_inv) p q
+  · exact g2gen2_dist2_inv p q
+  · exact symm_preserves_dist2 g2gen2 (g2gen2_dist2_inv) p q
+
+/-- Any generator word preserves distance-2 adjacency (structural induction). -/
+theorem applyWord_dist2_inv (w : List (Fin 4)) :
+    ∀ p q : Fin 63, tutte12Distance2Bool p q =
+      tutte12Distance2Bool (applyWord w p) (applyWord w q) := by
+  induction w with
+  | nil => intro p q; simp [applyWord]
+  | cons g gs ih =>
+    intro p q
+    simp only [applyWord, Equiv.trans_apply]
+    rw [applyGen_dist2_inv g p q]
+    exact ih (applyGen g p) (applyGen g q)
+
+/-! ## Part 7: Transitivity witnesses and main theorem -/
+
+private def witnessWordData : Array (List (Fin 4)) := #[
+  [],           [0],          [0,0,0],      [0,0],        [1],
+  [1,1,1],      [1,1],        [3,3,1],      [3,1,2],      [0,2,2,1],
+  [2],          [3],          [0,0,3,0],    [1,1,3,1],    [0,0,3,3],
+  [1,1,1,3],    [1,3,0],      [2,1,1],      [2,1,2,0],    [0,0,3,1],
+  [0,2],        [2,1,3],      [1,3,3],      [3,3],        [0,2,2],
+  [1,2,2,1],    [2,0],        [1,1,3],      [3,0],        [0,0,0,2],
+  [0,2,1,3],    [0,3,0,2],    [2,0,2,2],    [2,0,2],      [2,1],
+  [0,0,3],      [3,1],        [0,2,0],      [1,1,3,3],    [0,3,1,2],
+  [2,2],        [1,3],        [2,1,2],      [0,0,3,1,1],  [0,3,0],
+  [0,2,1],      [2,2,2],      [0,3,3],      [2,2,1],      [0,0,2],
+  [1,3,1],      [0,2,1,1],    [2,2,2,1],    [0,3],        [0,2,2,1,3],
+  [1,2],        [1,2,2],      [2,0,0],      [0,2,2,0],    [0,0,0,2,0],
+  [0,3,1],      [3,0,0],      [0,2,1,3,0]]
+
+private theorem witnessWordData_size : witnessWordData.size = 63 := by native_decide
+
+/-- BFS witness words: `witnessWord v` is a generator word mapping 0 → v. -/
+def witnessWord (v : Fin 63) : List (Fin 4) :=
+  witnessWordData[v.val]'(by have := witnessWordData_size; omega)
+
+/-- Each witness word correctly maps 0 to its target vertex. -/
+theorem witnessWord_correct :
+    ∀ v : Fin 63, applyWord (witnessWord v) 0 = v := by
+  native_decide
+
+/-- The Langer graph and distance-2 graph agree at vertex 0. -/
+theorem graphs_agree_at_zero :
+    ∀ v : Fin 63,
+      langerSimpleGraph.Adj 0 v ↔ (tutte12Distance2Bool 0 v = true) := by
+  native_decide
+
+private theorem transport_langer (w : List (Fin 4)) (q : Fin 63) :
+    langerSimpleGraph.Adj (applyWord w 0) q ↔
+      langerSimpleGraph.Adj 0 ((applyWord w).symm q) := by
+  conv_lhs => rw [← Equiv.apply_symm_apply (applyWord w) q]
+  exact ((applyWord_langer_inv w) 0 ((applyWord w).symm q)).symm
+
+private theorem transport_dist2 (w : List (Fin 4)) (q : Fin 63) :
+    tutte12Distance2Bool (applyWord w 0) q =
+      tutte12Distance2Bool 0 ((applyWord w).symm q) := by
+  conv_lhs => rw [← Equiv.apply_symm_apply (applyWord w) q]
+  exact ((applyWord_dist2_inv w) 0 ((applyWord w).symm q)).symm
+
+/-- **The Langer graph equals the distance-2 graph of the Tutte 12-cage
+restricted to points** — proved structurally via G₂(2) transitivity.
+
+The argument:
+1. Let σ = applyWord (witnessWord p), so σ(0) = p
+2. Adj p q ↔ Adj 0 (σ⁻¹ q)  [by transport_langer]
+3. dist2 p q = dist2 0 (σ⁻¹ q)  [by transport_dist2]
+4. Adj 0 (σ⁻¹ q) ↔ dist2 0 (σ⁻¹ q)  [by graphs_agree_at_zero] -/
+theorem langer_eq_tutte12_distance2' :
+    ∀ p q : Fin 63,
+      langerSimpleGraph.Adj p q ↔ (tutte12Distance2Bool p q = true) := by
+  intro p q
+  rw [← witnessWord_correct p]
+  rw [transport_langer, transport_dist2]
+  exact graphs_agree_at_zero _
+
+/-! ## The Langer graph is a Sabidussi coset graph
+
+G₂(2) = ⟨σ₁, σ₂⟩ acts vertex-transitively on the 63 points of GH(2,2),
+so by the Sabidussi representation theorem:
+  `langerSimpleGraph ≃g cosetGraph(Stab_G₂(0), connectionSet G₂ langer 0)` -/
+
+/-- The two G₂(2) generators as a `Fin 2`-indexed family. -/
+def langerGens : Fin 2 → Equiv.Perm (Fin 63)
+  | 0 => g2gen1
+  | 1 => g2gen2
+
+/-- G₂(2) as a subgroup of Sym(63), generated by σ₁ and σ₂. -/
+def langerG : Subgroup (Equiv.Perm (Fin 63)) :=
+  Subgroup.closure (Set.range langerGens)
+
+private theorem applyGen_mem (i : Fin 4) : applyGen i ∈ langerG := by
+  unfold langerG
+  match i with
+  | 0 => exact Subgroup.subset_closure ⟨0, rfl⟩
+  | 1 => exact Subgroup.inv_mem _ (Subgroup.subset_closure ⟨0, rfl⟩)
+  | 2 => exact Subgroup.subset_closure ⟨1, rfl⟩
+  | 3 => exact Subgroup.inv_mem _ (Subgroup.subset_closure ⟨1, rfl⟩)
+
+private theorem applyWord_mem (w : List (Fin 4)) : applyWord w ∈ langerG := by
+  induction w with
+  | nil => exact Subgroup.one_mem _
+  | cons i rest ih => exact langerG.mul_mem ih (applyGen_mem i)
+
+noncomputable instance langerMulAction : MulAction langerG (Fin 63) :=
+  MulAction.compHom (Fin 63) langerG.subtype
+
+noncomputable instance langerGraphAction :
+    GraphAction langerG (Fin 63) langerSimpleGraph where
+  adj_smul := by
+    intro ⟨σ, hσ⟩ u v hadj
+    change langerSimpleGraph.Adj (σ u) (σ v)
+    revert u v; change ∀ u v, langerSimpleGraph.Adj u v → langerSimpleGraph.Adj (σ u) (σ v)
+    refine Subgroup.closure_induction
+      (p := fun σ _ => ∀ u v, langerSimpleGraph.Adj u v → langerSimpleGraph.Adj (σ u) (σ v))
+      ?_ ?_ ?_ ?_ hσ
+    · intro x ⟨i, hi⟩; subst hi
+      match i with
+      | 0 => exact fun u v h => (g2gen1_langer_inv u v).mp h
+      | 1 => exact fun u v h => (g2gen2_langer_inv u v).mp h
+    · intro u v h; simpa
+    · intro x y _ _ hx hy u v hadj
+      simp only [Equiv.Perm.mul_apply]; exact hx _ _ (hy u v hadj)
+    · intro x _ hx u v hadj
+      let f : { p : Fin 63 × Fin 63 // langerSimpleGraph.Adj p.1 p.2 } →
+              { p : Fin 63 × Fin 63 // langerSimpleGraph.Adj p.1 p.2 } :=
+        fun ⟨⟨a, b⟩, hab⟩ => ⟨⟨x a, x b⟩, hx a b hab⟩
+      have hf_surj : Function.Surjective f := Finite.surjective_of_injective (by
+        intro ⟨⟨a₁, b₁⟩, _⟩ ⟨⟨a₂, b₂⟩, _⟩ h
+        simp only [f, Subtype.mk.injEq, Prod.mk.injEq] at h
+        exact Subtype.ext (Prod.ext (x.injective h.1) (x.injective h.2)))
+      obtain ⟨⟨⟨a, b⟩, hab⟩, heq⟩ := hf_surj ⟨⟨u, v⟩, hadj⟩
+      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
+
+noncomputable instance langerPretransitive :
+    MulAction.IsPretransitive langerG (Fin 63) where
+  exists_smul_eq := by
+    intro x y
+    let σ_x := applyWord (witnessWord x)
+    let σ_y := applyWord (witnessWord y)
+    have hmem : σ_x.symm.trans σ_y ∈ langerG :=
+      langerG.mul_mem (applyWord_mem _) (langerG.inv_mem (applyWord_mem _))
+    exact ⟨⟨σ_x.symm.trans σ_y, hmem⟩, by
+      change (σ_x.symm.trans σ_y) x = y
+      simp only [Equiv.trans_apply]
+      rw [show σ_x.symm x = 0 from by
+        rw [Equiv.symm_apply_eq]; exact (witnessWord_correct x).symm]
+      exact witnessWord_correct y⟩
+
+/-- **The Langer graph is a Sabidussi coset graph.**
+
+  `langerSimpleGraph ≃g Sab(G₂(2), H₁₉₂, D)`
+
+where H₁₉₂ = Stab(0) has order 192. -/
+noncomputable def langerSabidussiIso :
+    langerSimpleGraph ≃g SimpleGraph.cosetGraph
+      (MulAction.stabilizer langerG (0 : Fin 63))
+      (connectionSet langerG langerSimpleGraph 0)
+      (connectionSet.isConnectionSet 0) :=
+  sabidussiIso 0
+
+/-! ## Primitivity of the G₂(2) action
+
+The action of G₂(2) on the 63 points of GH(2,2) is **primitive**: the point
+stabiliser H₁₉₂ (order 192 = 12096/63) is a maximal subgroup of G₂(2).
+
+We verify this directly using Atkinson's algorithm (1975): for each v ≠ 0,
+compute the smallest block containing {0, v} by propagating equivalences
+through generators. A block B satisfies: ∀ g ∈ G, gB = B ∨ gB ∩ B = ∅.
+Equivalently: if i ~ j (same block) then g(i) ~ g(j). Starting from
+0 ~ v, we propagate via a queue of newly-merged pairs until stable. If
+the block is always all of Ω, no non-trivial block system exists.
+
+The queue-based approach processes only the O(n) actual merges rather
+than scanning all elements at each round, keeping the computation
+small. -/
+
+/-- All four generator permutations: σ₁, σ₁⁻¹, σ₂, σ₂⁻¹. -/
+private def g2AllGens : List (Equiv.Perm (Fin 63)) :=
+  [g2gen1, g2gen1.symm, g2gen2, g2gen2.symm]
+
+/-- Merge two equivalence classes: replace all occurrences of `hi`
+    with `lo`. -/
+private def mergeRep (f : Fin 63 → Fin 63) (lo hi : Fin 63) :
+    Fin 63 → Fin 63 :=
+  fun i => let fi := f i; if fi = hi then lo else fi
+
+/-- Atkinson's algorithm: compute the smallest block containing
+    {0, v}.
+
+    State: `(queue, partition)` where `queue` is a list of
+    newly-merged pairs and `partition : Fin 63 → Fin 63` maps each
+    element to its class representative.
+
+    At each step, pop a pair (x, y) from the queue. For each
+    generator g, check if g(x) and g(y) have the same
+    representative. If not, merge their classes and enqueue the
+    new pair. Terminate when the queue is empty.
+
+    `fuel` bounds the number of steps (at most 62 merges ×
+    4 generators = 248 enqueued pairs, so fuel = 300 is
+    generous). -/
+private def atkinson (gens : List (Equiv.Perm (Fin 63)))
+    (queue : List (Fin 63 × Fin 63))
+    (part : Fin 63 → Fin 63) :
+    Nat → Fin 63 → Fin 63
+  | 0 => part
+  | fuel + 1 =>
+    match queue with
+    | [] => part
+    | (x, y) :: rest =>
+      let Acc :=
+        List (Fin 63 × Fin 63) × (Fin 63 → Fin 63)
+      let (newPairs, part') :=
+        gens.foldl (fun (acc : Acc) g =>
+          let (pairs, p) := acc
+          let rgx := p (g x)
+          let rgy := p (g y)
+          if rgx = rgy then (pairs, p)
+          else
+            let lo := min rgx rgy
+            let hi := max rgx rgy
+            ((lo, hi) :: pairs, mergeRep p lo hi))
+          ([], part)
+      atkinson gens (rest ++ newPairs) part' fuel
+
+/-- Check that Atkinson's algorithm starting from {0, v} merges
+    all vertices into a single class (representative 0). -/
+private def blockIsFullBool (v : Fin 63) : Bool :=
+  let initPart : Fin 63 → Fin 63 := fun i =>
+    if i = v then 0 else i
+  let finalPart :=
+    atkinson g2AllGens [(0, v)] initPart 300
+  decide (∀ w : Fin 63, finalPart w = 0)
+
+/-- **Primitivity of the G₂(2) action on the 63 points of GH(2,2).**
+
+For every vertex v ≠ 0, Atkinson's algorithm starting from 0 ~ v
+merges all 63 vertices into a single equivalence class. This means
+no non-trivial block system exists, so the point stabiliser
+H₁₉₂ ≤ G₂(2) is a **maximal subgroup** — there is no subgroup K
+with H₁₉₂ < K < G₂(2).
+
+The Langer graph is primitive, and unlike Zhou-6 (the Z₂ quotient of
+the cubic Zhou graph F182A) it admits no cubic double cover
+(see `tutte12_points_independent` below). -/
+theorem langer_action_primitive :
+    ∀ v : Fin 63, v ≠ 0 →
+      blockIsFullBool v = true := by
+  native_decide
+
+/-! ## No cubic double cover of the Langer graph
+
+The Zhou graph (F182A, 182 vertices, cubic) is a Z₂ double cover of its
+quotient Zhou-6 (91 vertices, 6-regular) via the block system S₃ < D₁₂.
+One might ask: does the same hold for the Langer graph? That is, does
+there exist a 126-vertex cubic graph covering the Langer graph via a
+2:1 map?
+
+The natural candidate is the Tutte 12-cage (126 vertices, cubic, same
+G₂(2) symmetry). However, it **cannot** cover the Langer graph:
+
+1. The Tutte 12-cage is semisymmetric (not vertex-transitive), while
+   any covering of the vertex-transitive Langer graph must be
+   vertex-transitive.
+
+2. More fundamentally, the point stabiliser H₁₉₂ in G₂(2) has three
+   index-2 subgroups of order 96, but **none** yield a size-3
+   suborbit in the coset action on 126 points. The smallest suborbits
+   are size 6 and 12 — no cubic Sabidussi graph exists.
+
+Verification: the Tutte 12-cage point subgraph (induced on vertices
+0–62) has no edges, so no point-point edge can cover a Langer edge.
+-/
+
+/-- The Tutte 12-cage has no edges between points: the induced
+    subgraph on vertices 0–62 is edgeless. This obstructs any
+    covering map to the Langer graph, which has 189 edges between
+    its 63 vertices. -/
+theorem tutte12_points_independent :
+    ∀ p q : Fin 63,
+      ¬tutte12CageGraph.Adj
+        ⟨p.val, by omega⟩ ⟨q.val, by omega⟩ := by
+  native_decide
+
+/-! ## Zhou-6: PSL(2,13) acts primitively on 91 points
+
+The **Zhou-6 graph** (91 vertices, 6-regular) is Sab(PSL(2,13), D₁₂).
+The stabiliser D₁₂ is maximal in PSL(2,13), so the action is primitive.
+We verify this with the same Atkinson algorithm used for the Langer
+graph. -/
+
+private def zhou6Gen1Fwd : Array (Fin 91) := #[
+  1, 3, 5, 7, 8, 10, 12, 13, 15, 17, 18, 20, 6, 21, 23, 25, 27, 26,
+  30, 32, 34, 0, 37, 39, 41, 42, 44, 16, 47, 48, 49, 51, 53, 31, 24,
+  55, 56, 58, 60, 61, 62, 46, 65, 64, 57, 69, 11, 40, 66, 2, 71, 73,
+  75, 76, 77, 79, 38, 70, 81, 82, 59, 83, 54, 85, 45, 4, 35, 63, 43,
+  86, 9, 33, 22, 50, 87, 84, 88, 28, 14, 29, 19, 89, 36, 78, 52, 74,
+  68, 90, 80, 72, 67]
+private def zhou6Gen1Inv : Array (Fin 91) := #[
+  21, 0, 49, 1, 65, 2, 12, 3, 4, 70, 5, 46, 6, 7, 78, 8, 27, 9, 10,
+  80, 11, 13, 72, 14, 34, 15, 17, 16, 77, 79, 18, 33, 19, 71, 20, 66,
+  82, 22, 56, 23, 47, 24, 25, 68, 26, 64, 41, 28, 29, 30, 73, 31, 84,
+  32, 62, 35, 36, 44, 37, 60, 38, 39, 40, 67, 43, 42, 48, 90, 86, 45,
+  57, 50, 89, 51, 85, 52, 53, 54, 83, 55, 88, 58, 59, 61, 75, 63, 69,
+  74, 76, 81, 87]
+private def zhou6Gen2Fwd : Array (Fin 91) := #[
+  2, 4, 6, 5, 9, 11, 0, 14, 16, 1, 19, 3, 17, 22, 24, 26, 28, 29,
+  31, 33, 35, 36, 38, 40, 7, 43, 45, 46, 8, 12, 50, 52, 54, 10, 55,
+  53, 57, 59, 13, 51, 63, 64, 66, 67, 68, 15, 70, 56, 47, 41, 72, 74,
+  18, 20, 78, 80, 48, 21, 58, 69, 44, 73, 84, 23, 49, 79, 71, 25, 60,
+  37, 27, 42, 30, 81, 39, 85, 76, 65, 32, 77, 34, 61, 86, 62, 83, 89,
+  90, 87, 88, 75, 82]
+private def zhou6Gen2Inv : Array (Fin 91) := #[
+  6, 9, 0, 11, 1, 3, 2, 24, 28, 4, 33, 5, 29, 38, 7, 45, 8, 12, 52,
+  10, 53, 57, 13, 63, 14, 67, 15, 70, 16, 17, 72, 18, 78, 19, 80, 20,
+  21, 69, 22, 74, 23, 49, 71, 25, 60, 26, 27, 48, 56, 64, 30, 39, 31,
+  35, 32, 34, 47, 36, 58, 37, 68, 81, 83, 40, 41, 77, 42, 43, 44, 59,
+  46, 66, 50, 61, 51, 89, 76, 79, 54, 65, 55, 73, 90, 84, 62, 75, 82,
+  87, 88, 85, 86]
+
+private theorem zhou6Gen1Fwd_size : zhou6Gen1Fwd.size = 91 := by
+  native_decide
+private theorem zhou6Gen1Inv_size : zhou6Gen1Inv.size = 91 := by
+  native_decide
+private theorem zhou6Gen2Fwd_size : zhou6Gen2Fwd.size = 91 := by
+  native_decide
+private theorem zhou6Gen2Inv_size : zhou6Gen2Inv.size = 91 := by
+  native_decide
+
+/-- First generator of PSL(2,13) on 91 cosets of D₁₂. -/
+private def zhou6Gen1 : Equiv.Perm (Fin 91) where
+  toFun i := zhou6Gen1Fwd[i.val]'(by
+    have := zhou6Gen1Fwd_size; omega)
+  invFun i := zhou6Gen1Inv[i.val]'(by
+    have := zhou6Gen1Inv_size; omega)
+  left_inv := by intro i; revert i; native_decide
+  right_inv := by intro i; revert i; native_decide
+
+/-- Second generator of PSL(2,13) on 91 cosets of D₁₂. -/
+private def zhou6Gen2 : Equiv.Perm (Fin 91) where
+  toFun i := zhou6Gen2Fwd[i.val]'(by
+    have := zhou6Gen2Fwd_size; omega)
+  invFun i := zhou6Gen2Inv[i.val]'(by
+    have := zhou6Gen2Inv_size; omega)
+  left_inv := by intro i; revert i; native_decide
+  right_inv := by intro i; revert i; native_decide
+
+private def zhou6AllGens : List (Equiv.Perm (Fin 91)) :=
+  [zhou6Gen1, zhou6Gen1.symm, zhou6Gen2, zhou6Gen2.symm]
+
+private def mergeRep91 (f : Fin 91 → Fin 91) (lo hi : Fin 91) :
+    Fin 91 → Fin 91 :=
+  fun i => let fi := f i; if fi = hi then lo else fi
+
+private def atkinson91 (gens : List (Equiv.Perm (Fin 91)))
+    (queue : List (Fin 91 × Fin 91))
+    (part : Fin 91 → Fin 91) :
+    Nat → Fin 91 → Fin 91
+  | 0 => part
+  | fuel + 1 =>
+    match queue with
+    | [] => part
+    | (x, y) :: rest =>
+      let Acc :=
+        List (Fin 91 × Fin 91) × (Fin 91 → Fin 91)
+      let (newPairs, part') :=
+        gens.foldl (fun (acc : Acc) g =>
+          let (pairs, p) := acc
+          let rgx := p (g x)
+          let rgy := p (g y)
+          if rgx = rgy then (pairs, p)
+          else
+            let lo := min rgx rgy
+            let hi := max rgx rgy
+            ((lo, hi) :: pairs, mergeRep91 p lo hi))
+          ([], part)
+      atkinson91 gens (rest ++ newPairs) part' fuel
+
+private def zhou6BlockIsFullBool (v : Fin 91) : Bool :=
+  let initPart : Fin 91 → Fin 91 := fun i =>
+    if i = v then 0 else i
+  let finalPart :=
+    atkinson91 zhou6AllGens [(0, v)] initPart 400
+  decide (∀ w : Fin 91, finalPart w = 0)
+
+/-- **Primitivity of the PSL(2,13) action on 91 points.**
+
+For every vertex v ≠ 0, Atkinson's algorithm starting from 0 ~ v
+merges all 91 vertices into a single equivalence class. The point
+stabiliser D₁₂ ≤ PSL(2,13) is a maximal subgroup.
+
+The Zhou-6 graph Sab(PSL(2,13), D₁₂) is primitive and admits a
+cubic double cover: the Zhou graph F182A = Sab(PSL(2,13), S₃)
+covers it via S₃ ≤ D₁₂. -/
+theorem zhou6_action_primitive :
+    ∀ v : Fin 91, v ≠ 0 →
+      zhou6BlockIsFullBool v = true := by
+  native_decide
diff --git a/Mathlib.lean b/Mathlib.lean
index 51a2d9e682d0ca..100ccd502ff9dd 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
@@ -3591,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
@@ -3619,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
@@ -3626,9 +3629,11 @@ 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
+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/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]⟩
diff --git a/Mathlib/Combinatorics/SimpleGraph/CosetGraph.lean b/Mathlib/Combinatorics/SimpleGraph/CosetGraph.lean
new file mode 100644
index 00000000000000..caebcd8cfdedfe
--- /dev/null
+++ b/Mathlib/Combinatorics/SimpleGraph/CosetGraph.lean
@@ -0,0 +1,173 @@
+/-
+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
+
+/-! ## Coset projection
+
+When `H ≤ K`, the natural projection `G ⧸ H → G ⧸ K` sends `gH ↦ gK`.
+If `D` is a connection set for both `H` and `K`, this projection is a
+graph homomorphism: adjacency in `Sab(G, H, D)` implies adjacency in
+`Sab(G, K, D)`.
+
+This is the Sabidussi analogue of quotient by a block system: the orbits
+of `K` on `G ⧸ H` form a system of blocks of size `[K : H]`, and the
+quotient graph is `Sab(G, K, D)`. -/
+
+/-- The natural projection `G ⧸ H → G ⧸ K` when `H ≤ K`. -/
+def cosetProjection (H K : Subgroup G) (hle : H ≤ K) :
+    G ⧸ H → G ⧸ K :=
+  Quotient.map id fun _ _ hab => by
+    change (QuotientGroup.leftRel K).r _ _
+    have hab' : (QuotientGroup.leftRel H).r _ _ := hab
+    rw [QuotientGroup.leftRel_apply] at hab' ⊢
+    exact hle hab'
+
+@[simp]
+theorem cosetProjection_mk (H K : Subgroup G) (hle : H ≤ K)
+    (g : G) : cosetProjection H K hle ⟦g⟧ = ⟦g⟧ :=
+  rfl
+
+/-- **Coset projection is a graph homomorphism**: if `H ≤ K` and `D` is a
+    connection set for both, then adjacency in `Sab(G, H, D)` implies
+    adjacency in `Sab(G, K, D)`.
+
+    The proof is trivial: adjacency is `x⁻¹y ∈ D` in both graphs.
+    The subgroup only determines the coset equivalence, not the adjacency test. -/
+theorem SimpleGraph.cosetGraph.proj_adj
+    {H K : Subgroup G} (hle : H ≤ K) {D : Set G}
+    (hDH : IsConnectionSet H D) (hDK : IsConnectionSet K D)
+    (q₁ q₂ : G ⧸ H) :
+    (cosetGraph H D hDH).Adj q₁ q₂ →
+    (cosetGraph K D hDK).Adj (cosetProjection H K hle q₁)
+                              (cosetProjection H K hle q₂) :=
+  Quotient.inductionOn₂ q₁ q₂ fun _ _ h => h
+
+/-- The coset projection is surjective. -/
+theorem cosetProjection_surjective (H K : Subgroup G) (hle : H ≤ K) :
+    Function.Surjective (cosetProjection H K hle) :=
+  fun q => Quotient.inductionOn q fun g => ⟨⟦g⟧, rfl⟩
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/Representation.lean b/Mathlib/Combinatorics/SimpleGraph/Representation.lean
new file mode 100644
index 00000000000000..b1faf6b2f9bd21
--- /dev/null
+++ b/Mathlib/Combinatorics/SimpleGraph/Representation.lean
@@ -0,0 +1,163 @@
+/-
+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`: the set of group elements
+that move `v` to one of its neighbors. -/
+def connectionSet (G : Type*) [Group G] [MulAction G V]
+    (Γ : 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]
+
+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
+
+omit [GraphAction G V Γ] in
+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
diff --git a/Mathlib/Combinatorics/SimpleGraph/Symmetric.lean b/Mathlib/Combinatorics/SimpleGraph/Symmetric.lean
new file mode 100644
index 00000000000000..396baa0b54a598
--- /dev/null
+++ b/Mathlib/Combinatorics/SimpleGraph/Symmetric.lean
@@ -0,0 +1,196 @@
+/-
+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)
+
+/-- 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)
+
+/-- 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)