Closed genus-four row 098 from its separating vertex

Row 098 is the unique bridge-bearing member of the six loopless cubic genus-four cores. Removing vertex 1 separates two genus-two lobes. The checked core cut below is independent of edge lengths, and the public degenerate-cut theorem shows that it survives every nonloopy forest face.

This gives a short structural proof on the whole closed orthant; the generated g4row098.rpf cut-vertex certificate is therefore no longer load-bearing.

def AtanasovRanganathan.GenusFourRow098Closed.cut : Utilities.Certificate.CoreVertexCut.Data GenusFourCubicAtlas.row098Core

The two genus-two lobes of row 098 meet at vertex 1.

Equations

• AtanasovRanganathan.GenusFourRow098Closed.cut = { glue := 1, left := {0, 1, 4, 5} }

theorem AtanasovRanganathan.GenusFourRow098Closed.cut_valid : cut.Valid

theorem AtanasovRanganathan.GenusFourRow098Closed.cut_leftGenus : cut.leftGenus = 2

theorem AtanasovRanganathan.GenusFourRow098Closed.cut_rightGenus : cut.rightGenus = 2

theorem AtanasovRanganathan.GenusFourRow098Closed.bnExists_closed (length : Fin 9 → ℕ) (hForest : Utilities.Certificate.ContractionForestCensusGeneral.IsForest GenusFourCubicAtlas.row098Core (Configurations.zeroSlots length)) (hNotLoopy : ¬Utilities.Certificate.ContractionForestCensusGeneral.IsLoopy GenusFourCubicAtlas.row098Core (Configurations.zeroSlots length)) : Utilities.BNExists (Configurations.faceSpec GenusFourCubicAtlas.row098Core bnExists_closed._proof_1 length hForest hNotLoopy).graph 1 3

Every subdivision and every equal-genus contraction of row 098 carries a degree-three rank-one divisor.