The Atanasov--Ranganathan genus-five cubic atlas

This is the public-layer transcription of the sixteen loopless, bridgeless, topologically trivalent graphs displayed in Figure 8 of Atanasov--Ranganathan. It contains only incidence data and kernel-checked elementary properties; it does not assert the classification theorem or any divisor construction.

The vertices 0, ..., 7 follow the TikZ node order. Parallel TikZ edges are separate ordered slots. The source contains stray self-loop draw commands in the twelfth and sixteenth scopes; both scopes are already cubic with twelve non-loop edges, so those commands are omitted, as the figure caption requires.

@[reducible, inline]

abbrev AtanasovRanganathan.GenusFiveCoreAtlas.Core : Type

An ordered genus-five core with eight vertices and twelve edge slots.

Equations

• AtanasovRanganathan.GenusFiveCoreAtlas.Core = Utilities.Certificate.ExplicitPotential.Core 8 12

def AtanasovRanganathan.GenusFiveCoreAtlas.incidenceDegree (core : Core) (vertex : Fin 8) : ℕ

Number of half-edge incidences at a vertex of a loopless ordered core.

Equations

• AtanasovRanganathan.GenusFiveCoreAtlas.incidenceDegree core vertex = ∑ edge : Fin 12, ((if core.tail edge = vertex then 1 else 0) + if core.head edge = vertex then 1 else 0)

def AtanasovRanganathan.GenusFiveCoreAtlas.Trivalent (core : Core) : Prop

Every vertex has exactly three incident half-edges in the ordered core.

Equations

• AtanasovRanganathan.GenusFiveCoreAtlas.Trivalent core = ∀ (vertex : Fin 8), AtanasovRanganathan.GenusFiveCoreAtlas.incidenceDegree core vertex = 3

def AtanasovRanganathan.GenusFiveCoreAtlas.Loopless (core : Core) : Prop

Every edge slot has two distinct endpoints.

Equations

• AtanasovRanganathan.GenusFiveCoreAtlas.Loopless core = ∀ (edge : Fin 12), core.tail edge ≠ core.head edge

def AtanasovRanganathan.GenusFiveCoreAtlas.row01Core : Core

Figure scope 1 (a6,b6,c6,d6,x,y,e6,f6).

Equations

• AtanasovRanganathan.GenusFiveCoreAtlas.row01Core = { tail := ![0, 0, 2, 1, 2, 3, 5, 2, 4, 4, 6, 6], head := ![1, 1, 0, 3, 3, 5, 7, 4, 6, 5, 7, 7] }

def AtanasovRanganathan.GenusFiveCoreAtlas.row02Core : Core

Figure scope 2 (a9,b9,c9,b9a,c9a,d9,e9,f9).

Equations

• AtanasovRanganathan.GenusFiveCoreAtlas.row02Core = { tail := ![0, 1, 2, 5, 5, 6, 7, 7, 1, 2, 3, 3], head := ![1, 2, 5, 6, 6, 7, 0, 0, 3, 4, 4, 4] }

def AtanasovRanganathan.GenusFiveCoreAtlas.row03Core : Core

Figure scope 3 (41,42,43,45,A3,A5,B3,B5).

Equations

• AtanasovRanganathan.GenusFiveCoreAtlas.row03Core = { tail := ![0, 2, 0, 3, 0, 2, 6, 3, 7, 4, 4, 6], head := ![2, 1, 3, 1, 1, 6, 4, 7, 5, 5, 5, 7] }

def AtanasovRanganathan.GenusFiveCoreAtlas.row04Core : Core

Figure scope 4 (A1,A2,A8,A7,A3,A4,A5,A6).

Equations

• AtanasovRanganathan.GenusFiveCoreAtlas.row04Core = { tail := ![0, 0, 1, 4, 4, 5, 6, 6, 7, 3, 3, 2], head := ![1, 1, 4, 5, 5, 6, 7, 7, 3, 2, 2, 0] }

def AtanasovRanganathan.GenusFiveCoreAtlas.row05Core : Core

Figure scope 5 (a6,b6,c6,d6,x,y,e6,f6).

Equations

• AtanasovRanganathan.GenusFiveCoreAtlas.row05Core = { tail := ![0, 0, 2, 1, 2, 3, 5, 2, 4, 4, 6, 6], head := ![1, 1, 0, 3, 5, 5, 7, 4, 6, 3, 7, 7] }

def AtanasovRanganathan.GenusFiveCoreAtlas.row06Core : Core

Figure scope 6 (a6,b6,c6,d6,e6,f6,q6,p6).

Equations

• AtanasovRanganathan.GenusFiveCoreAtlas.row06Core = { tail := ![0, 0, 2, 1, 2, 7, 7, 6, 3, 2, 4, 4], head := ![1, 1, 0, 3, 7, 6, 6, 3, 5, 4, 5, 5] }

def AtanasovRanganathan.GenusFiveCoreAtlas.row07Core : Core

Figure scope 7 (41,42,43,45,B1,B2,B3,B4).

Equations

• AtanasovRanganathan.GenusFiveCoreAtlas.row07Core = { tail := ![0, 2, 0, 3, 2, 0, 1, 6, 4, 4, 5, 5], head := ![2, 1, 3, 1, 3, 4, 5, 7, 6, 6, 7, 7] }

def AtanasovRanganathan.GenusFiveCoreAtlas.row08Core : Core

Figure scope 8 (a6,b6,c6,j6,d6,h6,e6,f6).

Equations

• AtanasovRanganathan.GenusFiveCoreAtlas.row08Core = { tail := ![0, 0, 6, 3, 1, 2, 4, 5, 5, 2, 6, 6], head := ![1, 1, 3, 0, 4, 4, 5, 7, 2, 3, 7, 7] }

def AtanasovRanganathan.GenusFiveCoreAtlas.row09Core : Core

Figure scope 9 (31,32,33,34,35,36,311,312).

Equations

• AtanasovRanganathan.GenusFiveCoreAtlas.row09Core = { tail := ![0, 2, 1, 2, 1, 3, 4, 5, 0, 3, 6, 6], head := ![2, 1, 0, 5, 4, 4, 5, 3, 6, 7, 7, 7] }

def AtanasovRanganathan.GenusFiveCoreAtlas.row10Core : Core

Figure scope 10 (31,32,33,34,35,36,37,38).

Equations

• AtanasovRanganathan.GenusFiveCoreAtlas.row10Core = { tail := ![0, 2, 1, 2, 1, 3, 4, 6, 6, 5, 0, 5], head := ![2, 1, 0, 5, 4, 4, 6, 7, 7, 3, 3, 7] }

def AtanasovRanganathan.GenusFiveCoreAtlas.row11Core : Core

Figure scope 11 (outer square and inner square).

Equations

• AtanasovRanganathan.GenusFiveCoreAtlas.row11Core = { tail := ![0, 1, 3, 2, 4, 5, 7, 6, 4, 5, 7, 6], head := ![1, 3, 2, 0, 5, 7, 6, 4, 0, 1, 3, 2] }

def AtanasovRanganathan.GenusFiveCoreAtlas.row12Core : Core

Figure scope 12, omitting the anomalous extra self-loop command.

Equations

• AtanasovRanganathan.GenusFiveCoreAtlas.row12Core = { tail := ![0, 4, 2, 3, 0, 1, 5, 6, 7, 5, 6, 7], head := ![4, 2, 3, 1, 3, 4, 6, 7, 5, 0, 1, 2] }

def AtanasovRanganathan.GenusFiveCoreAtlas.row13Core : Core

Figure scope 13 (two K₄-minus-edge blocks).

Equations

• AtanasovRanganathan.GenusFiveCoreAtlas.row13Core = { tail := ![0, 2, 0, 3, 2, 4, 6, 4, 7, 6, 0, 1], head := ![2, 1, 3, 1, 3, 6, 5, 7, 5, 7, 4, 5] }

def AtanasovRanganathan.GenusFiveCoreAtlas.row14Core : Core

Figure scope 14 (a,b,c,d,e,f,g,h).

Equations

• AtanasovRanganathan.GenusFiveCoreAtlas.row14Core = { tail := ![0, 7, 7, 7, 0, 2, 3, 1, 5, 4, 2, 3], head := ![6, 1, 6, 6, 2, 3, 1, 5, 4, 0, 5, 4] }

def AtanasovRanganathan.GenusFiveCoreAtlas.row15Core : Core

Figure scope 15, with cyclic vertex labels O1, ..., O8.

Equations

• AtanasovRanganathan.GenusFiveCoreAtlas.row15Core = { tail := ![0, 1, 2, 3, 4, 5, 6, 7, 0, 1, 2, 7], head := ![1, 2, 3, 4, 5, 6, 7, 0, 4, 5, 6, 3] }

def AtanasovRanganathan.GenusFiveCoreAtlas.row16Core : Core

Figure scope 16, omitting the anomalous extra self-loop command.

Equations

• AtanasovRanganathan.GenusFiveCoreAtlas.row16Core = { tail := ![0, 4, 2, 3, 0, 3, 5, 6, 7, 5, 6, 7], head := ![4, 2, 3, 1, 1, 4, 6, 7, 5, 0, 1, 2] }

theorem AtanasovRanganathan.GenusFiveCoreAtlas.row01_trivalent : Trivalent row01Core

theorem AtanasovRanganathan.GenusFiveCoreAtlas.row02_trivalent : Trivalent row02Core

theorem AtanasovRanganathan.GenusFiveCoreAtlas.row03_trivalent : Trivalent row03Core

theorem AtanasovRanganathan.GenusFiveCoreAtlas.row04_trivalent : Trivalent row04Core

theorem AtanasovRanganathan.GenusFiveCoreAtlas.row05_trivalent : Trivalent row05Core

theorem AtanasovRanganathan.GenusFiveCoreAtlas.row06_trivalent : Trivalent row06Core

theorem AtanasovRanganathan.GenusFiveCoreAtlas.row07_trivalent : Trivalent row07Core

theorem AtanasovRanganathan.GenusFiveCoreAtlas.row08_trivalent : Trivalent row08Core

theorem AtanasovRanganathan.GenusFiveCoreAtlas.row09_trivalent : Trivalent row09Core

theorem AtanasovRanganathan.GenusFiveCoreAtlas.row10_trivalent : Trivalent row10Core

theorem AtanasovRanganathan.GenusFiveCoreAtlas.row11_trivalent : Trivalent row11Core

theorem AtanasovRanganathan.GenusFiveCoreAtlas.row12_trivalent : Trivalent row12Core

theorem AtanasovRanganathan.GenusFiveCoreAtlas.row13_trivalent : Trivalent row13Core

theorem AtanasovRanganathan.GenusFiveCoreAtlas.row14_trivalent : Trivalent row14Core

theorem AtanasovRanganathan.GenusFiveCoreAtlas.row15_trivalent : Trivalent row15Core

theorem AtanasovRanganathan.GenusFiveCoreAtlas.row16_trivalent : Trivalent row16Core

theorem AtanasovRanganathan.GenusFiveCoreAtlas.row01_loopless : Loopless row01Core

theorem AtanasovRanganathan.GenusFiveCoreAtlas.row02_loopless : Loopless row02Core

theorem AtanasovRanganathan.GenusFiveCoreAtlas.row03_loopless : Loopless row03Core

theorem AtanasovRanganathan.GenusFiveCoreAtlas.row04_loopless : Loopless row04Core

theorem AtanasovRanganathan.GenusFiveCoreAtlas.row05_loopless : Loopless row05Core

theorem AtanasovRanganathan.GenusFiveCoreAtlas.row06_loopless : Loopless row06Core

theorem AtanasovRanganathan.GenusFiveCoreAtlas.row07_loopless : Loopless row07Core

theorem AtanasovRanganathan.GenusFiveCoreAtlas.row08_loopless : Loopless row08Core

theorem AtanasovRanganathan.GenusFiveCoreAtlas.row09_loopless : Loopless row09Core

theorem AtanasovRanganathan.GenusFiveCoreAtlas.row10_loopless : Loopless row10Core

theorem AtanasovRanganathan.GenusFiveCoreAtlas.row11_loopless : Loopless row11Core

theorem AtanasovRanganathan.GenusFiveCoreAtlas.row12_loopless : Loopless row12Core

theorem AtanasovRanganathan.GenusFiveCoreAtlas.row13_loopless : Loopless row13Core

theorem AtanasovRanganathan.GenusFiveCoreAtlas.row14_loopless : Loopless row14Core

theorem AtanasovRanganathan.GenusFiveCoreAtlas.row15_loopless : Loopless row15Core

theorem AtanasovRanganathan.GenusFiveCoreAtlas.row16_loopless : Loopless row16Core

Connectivity

All sixteen rows, in one place. Six of them (01, 02, 04, 05, 08, 10) used to be proved locally in the row and chamber files instead — nine copies in all, because rows 08 and 10 repeated the fact once per chamber — and GenusFiveCubicAtlas re-proved the same six inline. They were kept out of here only because touching this file invalidates the forty-six modules that import it, including every generated cover; the generated covers now build

/-! # Genus Five Core Atlas -/ only in the independent generated checks.

The checker is connectedCheckFast (Utilities/Subdivision/ConnectedCheckFast.lean): a union--find fold rather than an enumeration of all 2⁸ vertex subsets. Measured on exactly these sixteen cores, the old connectedCheck cost 0.52 s each and this costs 0.013 s.

theorem AtanasovRanganathan.GenusFiveCoreAtlas.row01_connected : Utilities.Certificate.ExplicitPotential.Core.Connected row01Core

The first displayed row, AR's first family, is connected.

theorem AtanasovRanganathan.GenusFiveCoreAtlas.row02_connected : Utilities.Certificate.ExplicitPotential.Core.Connected row02Core

The second displayed row, AR's second family, is connected.

theorem AtanasovRanganathan.GenusFiveCoreAtlas.row03_connected : Utilities.Certificate.ExplicitPotential.Core.Connected row03Core

theorem AtanasovRanganathan.GenusFiveCoreAtlas.row04_connected : Utilities.Certificate.ExplicitPotential.Core.Connected row04Core

The necklace row, AR's fourth family, is connected.

theorem AtanasovRanganathan.GenusFiveCoreAtlas.row05_connected : Utilities.Certificate.ExplicitPotential.Core.Connected row05Core

The sixth-family row is connected.

theorem AtanasovRanganathan.GenusFiveCoreAtlas.row06_connected : Utilities.Certificate.ExplicitPotential.Core.Connected row06Core

theorem AtanasovRanganathan.GenusFiveCoreAtlas.row07_connected : Utilities.Certificate.ExplicitPotential.Core.Connected row07Core

The configuration-5 row is connected.

theorem AtanasovRanganathan.GenusFiveCoreAtlas.row08_connected : Utilities.Certificate.ExplicitPotential.Core.Connected row08Core

The seventh-family row is connected.

theorem AtanasovRanganathan.GenusFiveCoreAtlas.row09_connected : Utilities.Certificate.ExplicitPotential.Core.Connected row09Core

theorem AtanasovRanganathan.GenusFiveCoreAtlas.row10_connected : Utilities.Certificate.ExplicitPotential.Core.Connected row10Core

The ninth-family row is connected.

theorem AtanasovRanganathan.GenusFiveCoreAtlas.row11_connected : Utilities.Certificate.ExplicitPotential.Core.Connected row11Core

The cube row is connected. This small public fact lets its readable AR construction use the closed-subdivision rank-determining-set theorem without importing the private generated atlas.

theorem AtanasovRanganathan.GenusFiveCoreAtlas.row12_connected : Utilities.Certificate.ExplicitPotential.Core.Connected row12Core

The twelfth displayed row is connected.

theorem AtanasovRanganathan.GenusFiveCoreAtlas.row13_connected : Utilities.Certificate.ExplicitPotential.Core.Connected row13Core

The two-block row is connected.

theorem AtanasovRanganathan.GenusFiveCoreAtlas.row14_connected : Utilities.Certificate.ExplicitPotential.Core.Connected row14Core

theorem AtanasovRanganathan.GenusFiveCoreAtlas.row15_connected : Utilities.Certificate.ExplicitPotential.Core.Connected row15Core

The Möbius-ladder row is connected.

theorem AtanasovRanganathan.GenusFiveCoreAtlas.row16_connected : Utilities.Certificate.ExplicitPotential.Core.Connected row16Core

The final displayed row is connected.