A readable closed-face proof for cubic genus-four row 095

The positive face is the symbolic signed-window proof transcribed from the Atanasov--Ranganathan argument. The twenty-four proper nonloopy forest faces are dispatched by their exact zero sets:

• rows 031, 032, 034, and 068 use contractions of the readable closed row-097 proof;
• rows 029 and 069 use checked (2,2) vertex cuts;
• rows 002, 009, and 010 use the core-cardinality criterion.

The repetitive contraction witnesses are isolated as passive checked data in LowGenus.Generated.GenusFourRow095FaceData.

The exact 25-face ledger

def AtanasovRanganathan.GenusFourRow095Closed.validFaces : List (Finset (Fin 9))

The 25 explicitly enumerated zero-slot sets that are nonloopy forests in row 095, including the empty face and all valid lower-dimensional contractions.

Equations

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

theorem AtanasovRanganathan.GenusFourRow095Closed.validFaces_complete (F : Finset (Fin 9)) (hForest : Utilities.Certificate.ContractionForestCensusGeneral.IsForest LowGenus.GenusFourRow095.core F) (hNotLoopy : ¬Utilities.Certificate.ContractionForestCensusGeneral.IsLoopy LowGenus.GenusFourRow095.core F) : F ∈ validFaces

Kernel enumeration: these are exactly all nonloopy forest zero sets of row 095. The theorem is used only to turn the semantic face hypotheses into the displayed readable disjunction.

The nine quotient types

def AtanasovRanganathan.GenusFourRow095Closed.cut029 : Utilities.Certificate.CoreVertexCut.Data Generated.GenusFourRow095FaceData.core029

The vertex cut of contraction core 029 at glue vertex 3, with left vertex set {0, 3}; both pieces have genus two.

Equations

• AtanasovRanganathan.GenusFourRow095Closed.cut029 = { glue := 3, left := {0, 3} }

def AtanasovRanganathan.GenusFourRow095Closed.cut069 : Utilities.Certificate.CoreVertexCut.Data Generated.GenusFourRow095FaceData.core069

The vertex cut of contraction core 069 at glue vertex 3, with left vertex set {0, 3, 4}; both pieces have genus two.

Equations

• AtanasovRanganathan.GenusFourRow095Closed.cut069 = { glue := 3, left := {0, 3, 4} }

theorem AtanasovRanganathan.GenusFourRow095Closed.bnExists029 (s : Utilities.Certificate.SubdivisionGraph.Spec 4 7) (hCore : s.core = Generated.GenusFourRow095FaceData.core029) : Utilities.BNExists s.graph 1 3

theorem AtanasovRanganathan.GenusFourRow095Closed.bnExists069 (s : Utilities.Certificate.SubdivisionGraph.Spec 5 8) (hCore : s.core = Generated.GenusFourRow095FaceData.core069) : Utilities.BNExists s.graph 1 3

theorem AtanasovRanganathan.GenusFourRow095Closed.bnExists002 (s : Utilities.Certificate.SubdivisionGraph.Spec 2 5) (hCore : s.core = Generated.GenusFourRow095FaceData.core002) : Utilities.BNExists s.graph 1 3

theorem AtanasovRanganathan.GenusFourRow095Closed.bnExists009 (s : Utilities.Certificate.SubdivisionGraph.Spec 3 6) (hCore : s.core = Generated.GenusFourRow095FaceData.core009) : Utilities.BNExists s.graph 1 3

theorem AtanasovRanganathan.GenusFourRow095Closed.bnExists010 (s : Utilities.Certificate.SubdivisionGraph.Spec 3 6) (hCore : s.core = Generated.GenusFourRow095FaceData.core010) : Utilities.BNExists s.graph 1 3

Generic one-line use of a ledger entry

The closed theorem

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

Every subdivision and every equal-genus proper face of public cubic row 095 carries a degree-three rank-one divisor. Its conclusion exactly matches the row-095 obligation in GenusFourCubicCoverage.RowClosedCoverage.