The six loopless cubic genus-four core types

This module is the public, self-contained atlas of connected loopless cubic cores on six vertices. It contains only the six displayed cores and their kernel-checked validity. Exhaustiveness is proved separately by LowGenus.GenusFourCanonicalClassifier.

structure AtanasovRanganathan.GenusFourCubicAtlas.Row : Type

One concrete loopless 6-vertex, 9-slot cubic core.

• core : Utilities.Certificate.ExplicitPotential.Core 6 9

  The six-vertex, nine-slot core whose looplessness, connectedness, and cubic degrees are certified by this atlas row.

• loopless (edge : Fin 9) : self.core.tail edge ≠ self.core.head edge
• connected : self.core.Connected
• cubic : self.core.Cubic

The names retain the row numbers of the complete genus-four pseudocore catalog from which these six terminal loopless cubic rows were extracted.

def AtanasovRanganathan.GenusFourCubicAtlas.row095Core : Utilities.Certificate.ExplicitPotential.Core 6 9

The six-vertex cubic core for genus-four atlas row 095, with oriented slots 0→4, 0→5, 0→5, 1→3, 1→4, 1→5, 2→3, 2→3, 2→4 in index order.

Equations

• AtanasovRanganathan.GenusFourCubicAtlas.row095Core = { tail := ![0, 0, 0, 1, 1, 1, 2, 2, 2], head := ![4, 5, 5, 3, 4, 5, 3, 3, 4] }

def AtanasovRanganathan.GenusFourCubicAtlas.row096Core : Utilities.Certificate.ExplicitPotential.Core 6 9

The six-vertex cubic core for genus-four atlas row 096, with oriented slots 0→4, 0→5, 0→5, 1→3, 1→4, 1→4, 2→3, 2→3, 2→5 in index order.

Equations

• AtanasovRanganathan.GenusFourCubicAtlas.row096Core = { tail := ![0, 0, 0, 1, 1, 1, 2, 2, 2], head := ![4, 5, 5, 3, 4, 4, 3, 3, 5] }

def AtanasovRanganathan.GenusFourCubicAtlas.row097Core : Utilities.Certificate.ExplicitPotential.Core 6 9

The six-vertex cubic core for genus-four atlas row 097, with oriented slots 0→4, 0→5, 0→5, 1→2, 1→3, 1→5, 2→3, 2→4, 3→4 in index order.

Equations

• AtanasovRanganathan.GenusFourCubicAtlas.row097Core = { tail := ![0, 0, 0, 1, 1, 1, 2, 2, 3], head := ![4, 5, 5, 2, 3, 5, 3, 4, 4] }

def AtanasovRanganathan.GenusFourCubicAtlas.row098Core : Utilities.Certificate.ExplicitPotential.Core 6 9

The six-vertex cubic core for genus-four atlas row 098, with oriented slots 0→4, 0→5, 0→5, 1→2, 1→3, 1→4, 2→3, 2→3, 4→5 in index order.

Equations

• AtanasovRanganathan.GenusFourCubicAtlas.row098Core = { tail := ![0, 0, 0, 1, 1, 1, 2, 2, 4], head := ![4, 5, 5, 2, 3, 4, 3, 3, 5] }

def AtanasovRanganathan.GenusFourCubicAtlas.row099Core : Utilities.Certificate.ExplicitPotential.Core 6 9

The six-vertex cubic core for genus-four atlas row 099, with oriented slots 0→3, 0→4, 0→5, 1→3, 1→4, 1→5, 2→3, 2→4, 2→5 in index order.

Equations

• AtanasovRanganathan.GenusFourCubicAtlas.row099Core = { tail := ![0, 0, 0, 1, 1, 1, 2, 2, 2], head := ![3, 4, 5, 3, 4, 5, 3, 4, 5] }

def AtanasovRanganathan.GenusFourCubicAtlas.row100Core : Utilities.Certificate.ExplicitPotential.Core 6 9

The six-vertex cubic core for genus-four atlas row 100, with oriented slots 0→3, 0→4, 0→5, 1→2, 1→4, 1→5, 2→3, 2→5, 3→4 in index order.

Equations

• AtanasovRanganathan.GenusFourCubicAtlas.row100Core = { tail := ![0, 0, 0, 1, 1, 1, 2, 2, 3], head := ![3, 4, 5, 2, 4, 5, 3, 5, 4] }

def AtanasovRanganathan.GenusFourCubicAtlas.row095 : Row

Genus-four atlas row 095, packaging its concrete core with proofs that it is loopless, connected, and cubic.

Equations

• One or more equations did not get rendered due to their size.

def AtanasovRanganathan.GenusFourCubicAtlas.row096 : Row

Genus-four atlas row 096, packaging its concrete core with proofs that it is loopless, connected, and cubic.

Equations

• One or more equations did not get rendered due to their size.

def AtanasovRanganathan.GenusFourCubicAtlas.row097 : Row

Genus-four atlas row 097, packaging its concrete core with proofs that it is loopless, connected, and cubic.

Equations

• One or more equations did not get rendered due to their size.

def AtanasovRanganathan.GenusFourCubicAtlas.row098 : Row

Genus-four atlas row 098, packaging its concrete core with proofs that it is loopless, connected, and cubic.

Equations

• One or more equations did not get rendered due to their size.

def AtanasovRanganathan.GenusFourCubicAtlas.row099 : Row

Genus-four atlas row 099, packaging its concrete core with proofs that it is loopless, connected, and cubic.

Equations

• One or more equations did not get rendered due to their size.

def AtanasovRanganathan.GenusFourCubicAtlas.row100 : Row

Genus-four atlas row 100, packaging its concrete core with proofs that it is loopless, connected, and cubic.

Equations

• One or more equations did not get rendered due to their size.

def AtanasovRanganathan.GenusFourCubicAtlas.atlas : List Row

The exact atlas order used by the emitted canonical-classifier payload.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AtanasovRanganathan.GenusFourCubicAtlas.atlas_length : atlas.length = 6