The twenty loopless cubic genus-five core types

The first sixteen entries are the Atanasov--Ranganathan rows already owned by LowGenus. The final four are the elementary bridge-core types. This module is passive finite data plus kernel-checked validity; exhaustiveness is proved separately by the public canonical classifier.

structure AtanasovRanganathan.GenusFiveCubicAtlas.Row : Type

One concrete loopless 8-vertex, 12-slot cubic core.

• core : Utilities.Certificate.ExplicitPotential.Core 8 12

  The eight-vertex, twelve-slot core underlying this connected loopless cubic atlas row.

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

The sixteen AR rows

def AtanasovRanganathan.GenusFiveCubicAtlas.row01 : Row

Atlas row 01, bundling row01Core with its looplessness, connectivity, and cubic-degree proofs.

Equations

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

def AtanasovRanganathan.GenusFiveCubicAtlas.row02 : Row

Atlas row 02, bundling row02Core with its looplessness, connectivity, and cubic-degree proofs.

Equations

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

def AtanasovRanganathan.GenusFiveCubicAtlas.row03 : Row

Atlas row 03, bundling row03Core with its looplessness, connectivity, and cubic-degree proofs.

Equations

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

def AtanasovRanganathan.GenusFiveCubicAtlas.row04 : Row

Atlas row 04, bundling row04Core with its looplessness, connectivity, and cubic-degree proofs.

Equations

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

def AtanasovRanganathan.GenusFiveCubicAtlas.row05 : Row

Atlas row 05, bundling row05Core with its looplessness, connectivity, and cubic-degree proofs.

Equations

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

def AtanasovRanganathan.GenusFiveCubicAtlas.row06 : Row

Atlas row 06, bundling row06Core with its looplessness, connectivity, and cubic-degree proofs.

Equations

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

def AtanasovRanganathan.GenusFiveCubicAtlas.row07 : Row

Atlas row 07, bundling row07Core with its looplessness, connectivity, and cubic-degree proofs.

Equations

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

def AtanasovRanganathan.GenusFiveCubicAtlas.row08 : Row

Atlas row 08, bundling row08Core with its looplessness, connectivity, and cubic-degree proofs.

Equations

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

def AtanasovRanganathan.GenusFiveCubicAtlas.row09 : Row

Atlas row 09, bundling row09Core with its looplessness, connectivity, and cubic-degree proofs.

Equations

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

def AtanasovRanganathan.GenusFiveCubicAtlas.row10 : Row

Atlas row 10, bundling row10Core with its looplessness, connectivity, and cubic-degree proofs.

Equations

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

def AtanasovRanganathan.GenusFiveCubicAtlas.row11 : Row

Atlas row 11, bundling row11Core with its looplessness, connectivity, and cubic-degree proofs.

Equations

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

def AtanasovRanganathan.GenusFiveCubicAtlas.row12 : Row

Atlas row 12, bundling row12Core with its looplessness, connectivity, and cubic-degree proofs.

Equations

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

def AtanasovRanganathan.GenusFiveCubicAtlas.row13 : Row

Atlas row 13, bundling row13Core with its looplessness, connectivity, and cubic-degree proofs.

Equations

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

def AtanasovRanganathan.GenusFiveCubicAtlas.row14 : Row

Atlas row 14, bundling row14Core with its looplessness, connectivity, and cubic-degree proofs.

Equations

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

def AtanasovRanganathan.GenusFiveCubicAtlas.row15 : Row

Atlas row 15, bundling row15Core with its looplessness, connectivity, and cubic-degree proofs.

Equations

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

def AtanasovRanganathan.GenusFiveCubicAtlas.row16 : Row

Atlas row 16, bundling row16Core with its looplessness, connectivity, and cubic-degree proofs.

Equations

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

def AtanasovRanganathan.GenusFiveCubicAtlas.arAtlas : List Row

The sixteen Atanasov–Ranganathan cubic rows, in their numbered order.

Equations

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

The four bridge rows

def AtanasovRanganathan.GenusFiveCubicAtlas.rootDoubleCore : Utilities.Certificate.ExplicitPotential.Core 8 12

The eight-vertex root-double bridge core, given by its twelve ordered endpoint pairs.

Equations

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

def AtanasovRanganathan.GenusFiveCubicAtlas.oneChordCore : Utilities.Certificate.ExplicitPotential.Core 8 12

The eight-vertex one-chord bridge core, given by its twelve ordered endpoint pairs.

Equations

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

def AtanasovRanganathan.GenusFiveCubicAtlas.squareCore : Utilities.Certificate.ExplicitPotential.Core 8 12

The eight-vertex square bridge core, given by its twelve ordered endpoint pairs.

Equations

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

def AtanasovRanganathan.GenusFiveCubicAtlas.doubleMatchingCore : Utilities.Certificate.ExplicitPotential.Core 8 12

The eight-vertex double-matching bridge core, given by its twelve ordered endpoint pairs.

Equations

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

def AtanasovRanganathan.GenusFiveCubicAtlas.rootDouble : Row

The root-double bridge core bundled with its looplessness, connectivity, and cubic-degree proofs.

Equations

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

def AtanasovRanganathan.GenusFiveCubicAtlas.oneChord : Row

The one-chord bridge core bundled with its looplessness, connectivity, and cubic-degree proofs.

Equations

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

def AtanasovRanganathan.GenusFiveCubicAtlas.square : Row

The square bridge core bundled with its looplessness, connectivity, and cubic-degree proofs.

Equations

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

def AtanasovRanganathan.GenusFiveCubicAtlas.doubleMatching : Row

The double-matching bridge core bundled with its looplessness, connectivity, and cubic-degree proofs.

Equations

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

def AtanasovRanganathan.GenusFiveCubicAtlas.bridgeAtlas : List Row

The four bridge cores, ordered as root-double, one-chord, square, and double-matching.

Equations

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

def AtanasovRanganathan.GenusFiveCubicAtlas.atlas : List Row

The exact atlas order used by the emitted classifier payload.

Equations

• AtanasovRanganathan.GenusFiveCubicAtlas.atlas = AtanasovRanganathan.GenusFiveCubicAtlas.arAtlas ++ AtanasovRanganathan.GenusFiveCubicAtlas.bridgeAtlas

@[simp]

theorem AtanasovRanganathan.GenusFiveCubicAtlas.atlas_length : atlas.length = 20