Skip to content

Commit 4a55f04

Browse files
RaggedRclaude
andcommitted
doc: add visualization links for Bolza and Heawood surfaces
Link to underlying graph drawings (Möbius-Kantor F016A and Heawood F014A) hosted in the symmetric-graphs repo. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent f35385e commit 4a55f04

2 files changed

Lines changed: 4 additions & 0 deletions

File tree

Archive/BolzaSurface.lean

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,8 @@ GP(8,3). It is a cubic arc-transitive graph on 16 vertices.
1313
- **Tiling**: {8,3} — 6 octagonal faces on the Bolza surface (genus 2)
1414
- **CSS code**: [[24, 4, ≥ 6]]
1515
16+
- [Visualization](https://raw.githubusercontent.com/RaggedR/symmetric-graphs/main/lean/named_graphs/mobius-kantor-F016A.jpg) — the Möbius-Kantor graph (F016A)
17+
1618
All axioms verified by the Lean kernel (`decide`). No sorry.
1719
-/
1820

Archive/HeawoodSurface.lean

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,8 @@ the Fano plane PG(2,2). It is a cubic arc-transitive graph on 14 vertices.
1212
- **Tiling**: {6,3} — 7 hexagonal faces on the torus (genus 1)
1313
- **CSS code**: [[21, 2, ≥ 3]]
1414
15+
- [Visualization](https://raw.githubusercontent.com/RaggedR/symmetric-graphs/main/lean/named_graphs/heawood-F014A.jpg) — the Heawood graph (F014A)
16+
1517
Vertices 0–6 are the 7 points of the Fano plane.
1618
Vertices 7–13 are the 7 lines.
1719
Edge i connects a point to the line containing it.

0 commit comments

Comments
 (0)