Articulation data for the four genus-five cubic bridge rows

All four exceptional rows in the public cubic atlas have the same labelled genus-two lobe on vertices {0,1,2}, attached to the complementary genus-three side at vertex 0. The occurrence-level core cut checker and the factor-genus calculator verify this finite structural data directly.

def AtanasovRanganathan.GenusFiveBridgeRows.rootDoubleCut : Utilities.Certificate.CoreVertexCut.Data GenusFiveCubicAtlas.rootDoubleCore

The root-double bridge cut, with gluing vertex zero and left vertex set {0, 1, 2}.

Equations

• AtanasovRanganathan.GenusFiveBridgeRows.rootDoubleCut = { glue := 0, left := {0, 1, 2} }

def AtanasovRanganathan.GenusFiveBridgeRows.oneChordCut : Utilities.Certificate.CoreVertexCut.Data GenusFiveCubicAtlas.oneChordCore

The one-chord bridge cut, with gluing vertex zero and left vertex set {0, 1, 2}.

Equations

• AtanasovRanganathan.GenusFiveBridgeRows.oneChordCut = { glue := 0, left := {0, 1, 2} }

def AtanasovRanganathan.GenusFiveBridgeRows.squareCut : Utilities.Certificate.CoreVertexCut.Data GenusFiveCubicAtlas.squareCore

The square bridge cut, with gluing vertex zero and left vertex set {0, 1, 2}.

Equations

• AtanasovRanganathan.GenusFiveBridgeRows.squareCut = { glue := 0, left := {0, 1, 2} }

def AtanasovRanganathan.GenusFiveBridgeRows.doubleMatchingCut : Utilities.Certificate.CoreVertexCut.Data GenusFiveCubicAtlas.doubleMatchingCore

The double-matching bridge cut, with gluing vertex zero and left vertex set {0, 1, 2}.

Equations

• AtanasovRanganathan.GenusFiveBridgeRows.doubleMatchingCut = { glue := 0, left := {0, 1, 2} }

theorem AtanasovRanganathan.GenusFiveBridgeRows.rootDoubleCut_valid : rootDoubleCut.Valid

theorem AtanasovRanganathan.GenusFiveBridgeRows.oneChordCut_valid : oneChordCut.Valid

theorem AtanasovRanganathan.GenusFiveBridgeRows.squareCut_valid : squareCut.Valid

theorem AtanasovRanganathan.GenusFiveBridgeRows.doubleMatchingCut_valid : doubleMatchingCut.Valid

theorem AtanasovRanganathan.GenusFiveBridgeRows.rootDoubleCut_leftGenus : rootDoubleCut.leftGenus = 2

theorem AtanasovRanganathan.GenusFiveBridgeRows.oneChordCut_leftGenus : oneChordCut.leftGenus = 2

theorem AtanasovRanganathan.GenusFiveBridgeRows.squareCut_leftGenus : squareCut.leftGenus = 2

theorem AtanasovRanganathan.GenusFiveBridgeRows.doubleMatchingCut_leftGenus : doubleMatchingCut.leftGenus = 2

theorem AtanasovRanganathan.GenusFiveBridgeRows.rootDoubleCut_rightGenus : rootDoubleCut.rightGenus = 3

theorem AtanasovRanganathan.GenusFiveBridgeRows.oneChordCut_rightGenus : oneChordCut.rightGenus = 3

theorem AtanasovRanganathan.GenusFiveBridgeRows.squareCut_rightGenus : squareCut.rightGenus = 3

theorem AtanasovRanganathan.GenusFiveBridgeRows.doubleMatchingCut_rightGenus : doubleMatchingCut.rightGenus = 3

theorem AtanasovRanganathan.GenusFiveBridgeRows.bnExists_face_of_two_three_cut (genusFour : Utilities.GenusFourRankOneExistence) {n p : ℕ} (core : Utilities.Certificate.ExplicitPotential.Core n p) (hn : 0 < n) (hLoopless : ∀ (edge : Fin p), core.tail edge ≠ core.head edge) (hConnected : core.Connected) (cut : Utilities.Certificate.CoreVertexCut.Data core) (hValid : cut.Valid) (hLeft : cut.leftGenus = 2) (hRight : cut.rightGenus = 3) (length : Fin p → ℕ) (hForest : Utilities.Certificate.ContractionForestCensusGeneral.IsForest core (Configurations.zeroSlots length)) (hNotLoopy : ¬Utilities.Certificate.ContractionForestCensusGeneral.IsLoopy core (Configurations.zeroSlots length)) : Utilities.BNExists (Configurations.faceSpec core hn length hForest hNotLoopy).graph 1 4

A checked (2,3) articulation on a genus-five core supplies a degree-four pencil on every nonloopy forest face of that core.

theorem AtanasovRanganathan.GenusFiveBridgeRows.rootDouble_closed (genusFour : Utilities.GenusFourRankOneExistence) : Configurations.ClosedSubdivisionDharConstruction GenusFiveCubicAtlas.rootDoubleCore rootDouble_closed._proof_1

theorem AtanasovRanganathan.GenusFiveBridgeRows.oneChord_closed (genusFour : Utilities.GenusFourRankOneExistence) : Configurations.ClosedSubdivisionDharConstruction GenusFiveCubicAtlas.oneChordCore rootDouble_closed._proof_1

theorem AtanasovRanganathan.GenusFiveBridgeRows.square_closed (genusFour : Utilities.GenusFourRankOneExistence) : Configurations.ClosedSubdivisionDharConstruction GenusFiveCubicAtlas.squareCore rootDouble_closed._proof_1

theorem AtanasovRanganathan.GenusFiveBridgeRows.doubleMatching_closed (genusFour : Utilities.GenusFourRankOneExistence) : Configurations.ClosedSubdivisionDharConstruction GenusFiveCubicAtlas.doubleMatchingCore rootDouble_closed._proof_1

theorem AtanasovRanganathan.GenusFiveBridgeRows.bridgeAtlasClosedCoverage (genusFour : Utilities.GenusFourRankOneExistence) : GenusFiveCubicCoverage.BridgeAtlasClosedCoverage

The four bridge rows are all closed structurally by the same checked (2,3) articulation.