Skip to content

Commit 7e13510

Browse files
RaggedRclaude
andcommitted
style: fix linter errors in Archive surface files
- Move documentation from copyright block to /-! ... -/ module docstring - Module docstring placed immediately after imports - Replace indented dash lists with * lists (no double spaces) - Wrap data array lines to stay under 100 characters - Wrap ++ concatenation lines in Clayworth Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent 74cc58b commit 7e13510

4 files changed

Lines changed: 3704 additions & 1862 deletions

File tree

Archive/BolzaSurface.lean

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -2,24 +2,24 @@
22
Copyright (c) 2026 Robin Langer. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Robin Langer
5+
-/
6+
import Mathlib.Combinatorics.CellularSurface
57

8+
/-!
69
# The Bolza Surface: Möbius-Kantor Graph (F016A) on Genus 2
710
811
The Möbius-Kantor graph (Foster census F016A) = generalized Petersen graph
912
GP(8,3). It is a cubic arc-transitive graph on 16 vertices.
1013
11-
- **Sabidussi**: Sab(GL(2,3), C₃), |GL(2,3)| = 48
12-
- **Voltage graph**: `voltageGraphK2 8 0 1 3` on K₂ with Z₈
13-
- **Tiling**: {8,3} — 6 octagonal faces on the Bolza surface (genus 2)
14-
- **CSS code**: [[24, 4, ≥ 6]]
15-
16-
- [Visualization](https://raw.githubusercontent.com/RaggedR/symmetric-graphs/main/lean/named_graphs/mobius-kantor-F016A.jpg) — the Möbius-Kantor graph (F016A)
14+
* **Sabidussi**: Sab(GL(2,3), C₃), |GL(2,3)| = 48
15+
* **Voltage graph**: `voltageGraphK2 8 0 1 3` on K₂ with Z₈
16+
* **Tiling**: {8,3} — 6 octagonal faces on the Bolza surface (genus 2)
17+
* **CSS code**: [[24, 4, ≥ 6]]
18+
* [Visualization](https://raw.githubusercontent.com/RaggedR/symmetric-graphs/main/lean/named_graphs/mobius-kantor-F016A.jpg)
1719
1820
All axioms verified by the Lean kernel (`decide`). No sorry.
1921
-/
2022

21-
import Mathlib.Combinatorics.CellularSurface
22-
2323
open CellularSurface
2424

2525
/-- The Möbius-Kantor graph GP(8,3) embedded on the Bolza surface (genus 2).
@@ -40,7 +40,7 @@ def bolzaSurface : CellularSurface where
4040
![16, 8, 19, 3, 20, 12, 23, 7], -- 0→8→11→3→4→12→15→7→0
4141
![1, 18, 10, 21, 5, 22, 14, 17], -- 1→2→10→13→5→6→14→9→1
4242
![2, 19, 11, 22, 6, 23, 15, 18], -- 2→3→11→14→6→7→15→10→2
43-
![13, 10, 15, 12, 9, 14, 11, 8] -- 8→13→10→15→12→9→14→11→8 (inner star reversed)
43+
![13, 10, 15, 12, 9, 14, 11, 8] -- inner star reversed
4444
]
4545
face_dir := ![
4646
![true, true, true, false, true, true, true, false],

0 commit comments

Comments
 (0)