feat(Archive): Heawood and MK are Sabidussi coset graphs

Add heawoodSabidussiIso and mkSabidussiIso: both voltage graphs are
proved to be coset graphs via the Sabidussi representation theorem.

Generators defined by formulas (no lookup tables):
- Heawood: Z₇ translation + fibre swap with negation (D₁₄ action)
- MK: Z₈ translation + fibre swap with ×5 (D₁₆ action)

Adjacency preservation by native_decide, transitivity by explicit
witness elements (translation^k and translation^k * swap).

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: RaggedR

Archive/VoltageGraphs.lean

@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robin Langer
 -/
 import Mathlib.Combinatorics.SimpleGraph.QuotientGraph
+import Mathlib.Combinatorics.SimpleGraph.Action
+import Mathlib.Combinatorics.SimpleGraph.Representation
 import Mathlib.Data.ZMod.Basic
 
 /-!
@@ -123,3 +125,233 @@ theorem mobiusKantorVoltage_quotient_complete :
     (mobiusKantorVoltage.quotientGraph
       (Prod.fst : Fin 2 × ZMod 8 → Fin 2)).Adj i j := by
   native_decide
+
+/-! ## Sabidussi coset graph representations
+
+Every voltage graph on K₂ is vertex-transitive: the cyclic group acts by
+translation on the fibre coordinate, and a fibre-swapping automorphism
+makes the action transitive on all vertices. By the Sabidussi representation
+theorem, the graph is a coset graph. -/
+
+section HeawoodSabidussi
+
+/-- Z₇ translation: `(i, g) ↦ (i, g + 1)`. -/
+private def heawoodTranslation : Equiv.Perm (Fin 2 × ZMod 7) where
+  toFun p := (p.1, p.2 + 1)
+  invFun p := (p.1, p.2 - 1)
+  left_inv := by intro ⟨i, g⟩; simp [add_sub_cancel_right]
+  right_inv := by intro ⟨i, g⟩; simp [sub_add_cancel]
+
+/-- Fibre swap with negation: `(i, g) ↦ (1 - i, -g)`.
+    Preserves Heawood adjacency because `-v ∈ {0, 4, 6}` for `v ∈ {0, 4, 6}` in Z₇. -/
+private def heawoodSwap : Equiv.Perm (Fin 2 × ZMod 7) where
+  toFun p := (⟨1 - p.1.val, by omega⟩, -p.2)
+  invFun p := (⟨1 - p.1.val, by omega⟩, -p.2)
+  left_inv := by native_decide
+  right_inv := by native_decide
+
+/-- Translation preserves Heawood adjacency. -/
+private theorem heawoodTranslation_adj : ∀ u v : Fin 2 × ZMod 7,
+    heawoodVoltage.Adj u v → heawoodVoltage.Adj (heawoodTranslation u) (heawoodTranslation v) := by
+  native_decide
+
+/-- Swap preserves Heawood adjacency. -/
+private theorem heawoodSwap_adj : ∀ u v : Fin 2 × ZMod 7,
+    heawoodVoltage.Adj u v → heawoodVoltage.Adj (heawoodSwap u) (heawoodSwap v) := by
+  native_decide
+
+/-- The group generated by translation and swap. -/
+private def heawoodG : Subgroup (Equiv.Perm (Fin 2 × ZMod 7)) :=
+  Subgroup.closure ({heawoodTranslation, heawoodSwap} : Set _)
+
+private noncomputable instance : MulAction heawoodG (Fin 2 × ZMod 7) :=
+  MulAction.compHom _ heawoodG.subtype
+
+private noncomputable instance : GraphAction heawoodG (Fin 2 × ZMod 7) heawoodVoltage where
+  adj_smul := by
+    intro ⟨σ, hσ⟩ u v hadj
+    show heawoodVoltage.Adj (σ u) (σ v)
+    revert u v; change ∀ u v, heawoodVoltage.Adj u v → heawoodVoltage.Adj (σ u) (σ v)
+    refine Subgroup.closure_induction
+      (p := fun σ _ => ∀ u v, heawoodVoltage.Adj u v → heawoodVoltage.Adj (σ u) (σ v))
+      ?_ ?_ ?_ ?_ hσ
+    · intro x hx
+      rcases hx with rfl | rfl
+      · exact heawoodTranslation_adj
+      · exact heawoodSwap_adj
+    · 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 2 × ZMod 7) × (Fin 2 × ZMod 7) // heawoodVoltage.Adj p.1 p.2 } →
+              { p : (Fin 2 × ZMod 7) × (Fin 2 × ZMod 7) // heawoodVoltage.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
+
+private def heawoodT_mem : heawoodTranslation ∈ heawoodG :=
+  Subgroup.subset_closure (Set.mem_insert _ _)
+
+private def heawoodS_mem : heawoodSwap ∈ heawoodG :=
+  Subgroup.subset_closure (Set.mem_insert_of_mem _ rfl)
+
+/-- Witness element mapping (0,0) to v, as a product of generators. -/
+private def heawoodWitElem : Fin 2 × ZMod 7 → Equiv.Perm (Fin 2 × ZMod 7)
+  | (⟨0, _⟩, g) => heawoodTranslation ^ g.val
+  | (⟨1, _⟩, g) => heawoodTranslation ^ g.val * heawoodSwap
+
+private theorem heawoodWitElem_correct :
+    ∀ v : Fin 2 × ZMod 7,
+      heawoodWitElem v ((0 : Fin 2), (0 : ZMod 7)) = v := by native_decide
+
+private theorem heawoodWitElem_mem (v : Fin 2 × ZMod 7) : heawoodWitElem v ∈ heawoodG := by
+  rcases v with ⟨⟨i, hi⟩, g⟩
+  interval_cases i
+  · exact heawoodG.pow_mem heawoodT_mem _
+  · exact heawoodG.mul_mem (heawoodG.pow_mem heawoodT_mem _) heawoodS_mem
+
+private noncomputable instance : MulAction.IsPretransitive heawoodG (Fin 2 × ZMod 7) where
+  exists_smul_eq := by
+    intro x y
+    have hmem : (heawoodWitElem x).symm.trans (heawoodWitElem y) ∈ heawoodG :=
+      heawoodG.mul_mem (heawoodWitElem_mem y) (heawoodG.inv_mem (heawoodWitElem_mem x))
+    exact ⟨⟨_, hmem⟩, by
+      change ((heawoodWitElem x).symm.trans (heawoodWitElem y)) x = y
+      simp only [Equiv.trans_apply]
+      rw [show (heawoodWitElem x).symm x = ((0 : Fin 2), (0 : ZMod 7)) from by
+        rw [Equiv.symm_apply_eq]; exact (heawoodWitElem_correct x).symm]
+      exact heawoodWitElem_correct y⟩
+
+/-- **The Heawood graph is a Sabidussi coset graph.**
+
+The dihedral group D₁₄ = ⟨translation, swap⟩ acts vertex-transitively, giving:
+  `heawoodVoltage ≃g Sab(D₁₄, {1}, D)` (a Cayley graph). -/
+noncomputable def heawoodSabidussiIso :
+    heawoodVoltage ≃g SimpleGraph.cosetGraph
+      (MulAction.stabilizer heawoodG ((0 : Fin 2), (0 : ZMod 7)))
+      (connectionSet heawoodG heawoodVoltage ((0 : Fin 2), (0 : ZMod 7)))
+      (connectionSet.isConnectionSet _) :=
+  sabidussiIso _
+
+end HeawoodSabidussi
+
+section MKSabidussi
+
+/-- Z₈ translation: `(i, g) ↦ (i, g + 1)`. -/
+private def mkTranslation : Equiv.Perm (Fin 2 × ZMod 8) where
+  toFun p := (p.1, p.2 + 1)
+  invFun p := (p.1, p.2 - 1)
+  left_inv := by intro ⟨i, g⟩; simp [add_sub_cancel_right]
+  right_inv := by intro ⟨i, g⟩; simp [sub_add_cancel]
+
+/-- Fibre swap with multiplication by 5: `(i, g) ↦ (1 - i, 5g)`.
+    Preserves MK adjacency because `5 · {0, 1, 3} = {0, 5, 15} = {0, 5, 7}` and
+    the adjacency condition uses `-5v`: `-5 · {0, 1, 3} = {0, 3, 1} = {0, 1, 3}`. -/
+private def mkSwap : Equiv.Perm (Fin 2 × ZMod 8) where
+  toFun p := (⟨1 - p.1.val, by omega⟩, 5 * p.2)
+  invFun p := (⟨1 - p.1.val, by omega⟩, 5 * p.2)  -- 5² = 25 = 1 mod 8
+  left_inv := by native_decide
+  right_inv := by native_decide
+
+/-- Translation preserves MK adjacency. -/
+private theorem mkTranslation_adj : ∀ u v : Fin 2 × ZMod 8,
+    mobiusKantorVoltage.Adj u v →
+    mobiusKantorVoltage.Adj (mkTranslation u) (mkTranslation v) := by
+  native_decide
+
+/-- Swap preserves MK adjacency. -/
+private theorem mkSwap_adj : ∀ u v : Fin 2 × ZMod 8,
+    mobiusKantorVoltage.Adj u v →
+    mobiusKantorVoltage.Adj (mkSwap u) (mkSwap v) := by
+  native_decide
+
+private def mkG : Subgroup (Equiv.Perm (Fin 2 × ZMod 8)) :=
+  Subgroup.closure ({mkTranslation, mkSwap} : Set _)
+
+private noncomputable instance : MulAction mkG (Fin 2 × ZMod 8) :=
+  MulAction.compHom _ mkG.subtype
+
+private noncomputable instance : GraphAction mkG (Fin 2 × ZMod 8) mobiusKantorVoltage where
+  adj_smul := by
+    intro ⟨σ, hσ⟩ u v hadj
+    show mobiusKantorVoltage.Adj (σ u) (σ v)
+    revert u v
+    change ∀ u v, mobiusKantorVoltage.Adj u v → mobiusKantorVoltage.Adj (σ u) (σ v)
+    refine Subgroup.closure_induction
+      (p := fun σ _ => ∀ u v, mobiusKantorVoltage.Adj u v →
+        mobiusKantorVoltage.Adj (σ u) (σ v))
+      ?_ ?_ ?_ ?_ hσ
+    · intro x hx
+      rcases hx with rfl | rfl
+      · exact mkTranslation_adj
+      · exact mkSwap_adj
+    · 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 2 × ZMod 8) × (Fin 2 × ZMod 8) //
+                mobiusKantorVoltage.Adj p.1 p.2 } →
+              { p : (Fin 2 × ZMod 8) × (Fin 2 × ZMod 8) //
+                mobiusKantorVoltage.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
+
+private def mkT_mem : mkTranslation ∈ mkG :=
+  Subgroup.subset_closure (Set.mem_insert _ _)
+
+private def mkS_mem : mkSwap ∈ mkG :=
+  Subgroup.subset_closure (Set.mem_insert_of_mem _ rfl)
+
+private def mkWitElem : Fin 2 × ZMod 8 → Equiv.Perm (Fin 2 × ZMod 8)
+  | (⟨0, _⟩, g) => mkTranslation ^ g.val
+  | (⟨1, _⟩, g) => mkTranslation ^ g.val * mkSwap
+
+private theorem mkWitElem_correct :
+    ∀ v : Fin 2 × ZMod 8,
+      mkWitElem v ((0 : Fin 2), (0 : ZMod 8)) = v := by native_decide
+
+private theorem mkWitElem_mem (v : Fin 2 × ZMod 8) : mkWitElem v ∈ mkG := by
+  rcases v with ⟨⟨i, hi⟩, g⟩
+  interval_cases i
+  · exact mkG.pow_mem mkT_mem _
+  · exact mkG.mul_mem (mkG.pow_mem mkT_mem _) mkS_mem
+
+private noncomputable instance : MulAction.IsPretransitive mkG (Fin 2 × ZMod 8) where
+  exists_smul_eq := by
+    intro x y
+    have hmem : (mkWitElem x).symm.trans (mkWitElem y) ∈ mkG :=
+      mkG.mul_mem (mkWitElem_mem y) (mkG.inv_mem (mkWitElem_mem x))
+    exact ⟨⟨_, hmem⟩, by
+      change ((mkWitElem x).symm.trans (mkWitElem y)) x = y
+      simp only [Equiv.trans_apply]
+      rw [show (mkWitElem x).symm x = ((0 : Fin 2), (0 : ZMod 8)) from by
+        rw [Equiv.symm_apply_eq]; exact (mkWitElem_correct x).symm]
+      exact mkWitElem_correct y⟩
+
+/-- **The Möbius-Kantor graph is a Sabidussi coset graph.**
+
+The dihedral group D₁₆ = ⟨translation, swap⟩ acts vertex-transitively, giving:
+  `mobiusKantorVoltage ≃g Sab(D₁₆, {1}, D)` (a Cayley graph). -/
+noncomputable def mkSabidussiIso :
+    mobiusKantorVoltage ≃g SimpleGraph.cosetGraph
+      (MulAction.stabilizer mkG ((0 : Fin 2), (0 : ZMod 8)))
+      (connectionSet mkG mobiusKantorVoltage ((0 : Fin 2), (0 : ZMod 8)))
+      (connectionSet.isConnectionSet _) :=
+  sabidussiIso _
+
+end MKSabidussi