Independent generated check. This module provides an additional generated proof of row 04 and is not imported by the main LowGenus root.

Generated cell chunk 0 of 2 for the AR row-04 chamber cover (cells 0-97). Split across modules because the kernel cost of replaying a cell is cumulative within one Lean process.

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell0 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 0 for the fixed row-04 divisor, with 22 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 2, 3, 0, 0, 4]; cell0_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell0_check : cell0.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell1 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 1 for the fixed row-04 divisor, with 23 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 2, 3, 0, 0, 5]; cell1_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell1_check : cell1.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell2 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 2 for the fixed row-04 divisor, with 23 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 2, 3, 0, 0, 6]; cell2_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell2_check : cell2.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell3 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 3 for the fixed row-04 divisor, with 23 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 2, 3, 0, 0, 7]; cell3_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell3_check : cell3.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell4 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 4 for the fixed row-04 divisor, with 23 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 2, 8, 0, 0, 4]; cell4_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell4_check : cell4.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell5 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 5 for the fixed row-04 divisor, with 23 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 2, 9, 0, 0, 4]; cell5_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell5_check : cell5.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell6 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 6 for the fixed row-04 divisor, with 23 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 2, 10, 0, 0, 4]; cell6_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell6_check : cell6.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell7 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 7 for the fixed row-04 divisor, with 24 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 2, 8, 0, 0, 5]; cell7_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell7_check : cell7.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell8 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 8 for the fixed row-04 divisor, with 24 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 2, 8, 0, 0, 6]; cell8_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell8_check : cell8.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell9 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 9 for the fixed row-04 divisor, with 24 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 2, 8, 0, 0, 7]; cell9_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell9_check : cell9.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell10 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 10 for the fixed row-04 divisor, with 24 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 2, 9, 0, 0, 5]; cell10_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell10_check : cell10.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell11 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 11 for the fixed row-04 divisor, with 24 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 2, 9, 0, 0, 6]; cell11_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell11_check : cell11.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell12 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 12 for the fixed row-04 divisor, with 24 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 2, 9, 0, 0, 7]; cell12_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell12_check : cell12.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell13 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 13 for the fixed row-04 divisor, with 24 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 2, 10, 0, 0, 5]; cell13_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell13_check : cell13.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell14 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 14 for the fixed row-04 divisor, with 24 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 2, 10, 0, 0, 6]; cell14_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell14_check : cell14.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell15 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 15 for the fixed row-04 divisor, with 24 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 2, 10, 0, 0, 7]; cell15_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell15_check : cell15.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell16 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 16 for the fixed row-04 divisor, with 22 affine cone constraints. Anchors zero through seven use witness indices [0, 11, 0, 2, 12, 0, 0, 4]; cell16_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell16_check : cell16.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell17 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 17 for the fixed row-04 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 8, 0, 2, 8, 0, 0, 4]; cell17_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell17_check : cell17.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell18 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 18 for the fixed row-04 divisor, with 23 affine cone constraints. Anchors zero through seven use witness indices [0, 13, 0, 2, 14, 0, 0, 4]; cell18_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell18_check : cell18.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell19 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 19 for the fixed row-04 divisor, with 23 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 0, 2, 8, 0, 0, 4]; cell19_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell19_check : cell19.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell20 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 20 for the fixed row-04 divisor, with 22 affine cone constraints. Anchors zero through seven use witness indices [0, 16, 0, 2, 9, 0, 0, 4]; cell20_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell20_check : cell20.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell21 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 21 for the fixed row-04 divisor, with 24 affine cone constraints. Anchors zero through seven use witness indices [0, 17, 0, 2, 18, 0, 0, 4]; cell21_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell21_check : cell21.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell22 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 22 for the fixed row-04 divisor, with 24 affine cone constraints. Anchors zero through seven use witness indices [0, 17, 0, 2, 10, 0, 0, 4]; cell22_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell22_check : cell22.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell23 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 23 for the fixed row-04 divisor, with 24 affine cone constraints. Anchors zero through seven use witness indices [0, 19, 0, 2, 14, 0, 0, 4]; cell23_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell23_check : cell23.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell24 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 24 for the fixed row-04 divisor, with 23 affine cone constraints. Anchors zero through seven use witness indices [0, 20, 0, 2, 14, 0, 0, 4]; cell24_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell24_check : cell24.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell25 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 25 for the fixed row-04 divisor, with 24 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 0, 2, 8, 0, 0, 5]; cell25_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell25_check : cell25.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell26 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 26 for the fixed row-04 divisor, with 24 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 0, 2, 8, 0, 0, 6]; cell26_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell26_check : cell26.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell27 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 27 for the fixed row-04 divisor, with 24 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 0, 2, 8, 0, 0, 7]; cell27_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell27_check : cell27.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell28 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 28 for the fixed row-04 divisor, with 25 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 0, 2, 14, 0, 0, 5]; cell28_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell28_check : cell28.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell29 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 29 for the fixed row-04 divisor, with 25 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 0, 2, 14, 0, 0, 6]; cell29_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell29_check : cell29.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell30 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 30 for the fixed row-04 divisor, with 25 affine cone constraints. Anchors zero through seven use witness indices [0, 15, 0, 2, 14, 0, 0, 7]; cell30_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell30_check : cell30.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell31 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 31 for the fixed row-04 divisor, with 25 affine cone constraints. Anchors zero through seven use witness indices [0, 19, 0, 2, 14, 0, 0, 5]; cell31_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell31_check : cell31.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell32 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 32 for the fixed row-04 divisor, with 25 affine cone constraints. Anchors zero through seven use witness indices [0, 19, 0, 2, 14, 0, 0, 6]; cell32_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell32_check : cell32.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell33 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 33 for the fixed row-04 divisor, with 25 affine cone constraints. Anchors zero through seven use witness indices [0, 19, 0, 2, 14, 0, 0, 7]; cell33_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell33_check : cell33.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell34 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 34 for the fixed row-04 divisor, with 22 affine cone constraints. Anchors zero through seven use witness indices [0, 8, 0, 2, 8, 0, 0, 5]; cell34_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell34_check : cell34.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell35 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 35 for the fixed row-04 divisor, with 22 affine cone constraints. Anchors zero through seven use witness indices [0, 8, 0, 2, 8, 0, 0, 6]; cell35_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell35_check : cell35.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell36 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 36 for the fixed row-04 divisor, with 22 affine cone constraints. Anchors zero through seven use witness indices [0, 8, 0, 2, 8, 0, 0, 7]; cell36_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell36_check : cell36.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell37 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 37 for the fixed row-04 divisor, with 24 affine cone constraints. Anchors zero through seven use witness indices [0, 13, 0, 2, 14, 0, 0, 5]; cell37_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell37_check : cell37.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell38 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 38 for the fixed row-04 divisor, with 24 affine cone constraints. Anchors zero through seven use witness indices [0, 13, 0, 2, 14, 0, 0, 6]; cell38_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell38_check : cell38.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell39 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 39 for the fixed row-04 divisor, with 24 affine cone constraints. Anchors zero through seven use witness indices [0, 13, 0, 2, 14, 0, 0, 7]; cell39_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell39_check : cell39.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell40 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 40 for the fixed row-04 divisor, with 23 affine cone constraints. Anchors zero through seven use witness indices [0, 16, 0, 2, 9, 0, 0, 5]; cell40_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell40_check : cell40.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell41 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 41 for the fixed row-04 divisor, with 23 affine cone constraints. Anchors zero through seven use witness indices [0, 16, 0, 2, 9, 0, 0, 6]; cell41_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell41_check : cell41.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell42 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 42 for the fixed row-04 divisor, with 23 affine cone constraints. Anchors zero through seven use witness indices [0, 16, 0, 2, 9, 0, 0, 7]; cell42_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell42_check : cell42.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell43 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 43 for the fixed row-04 divisor, with 25 affine cone constraints. Anchors zero through seven use witness indices [0, 17, 0, 2, 18, 0, 0, 5]; cell43_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell43_check : cell43.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell44 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 44 for the fixed row-04 divisor, with 25 affine cone constraints. Anchors zero through seven use witness indices [0, 17, 0, 2, 10, 0, 0, 5]; cell44_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell44_check : cell44.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell45 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 45 for the fixed row-04 divisor, with 25 affine cone constraints. Anchors zero through seven use witness indices [0, 17, 0, 2, 18, 0, 0, 6]; cell45_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell45_check : cell45.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell46 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 46 for the fixed row-04 divisor, with 25 affine cone constraints. Anchors zero through seven use witness indices [0, 17, 0, 2, 10, 0, 0, 6]; cell46_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell46_check : cell46.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell47 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 47 for the fixed row-04 divisor, with 25 affine cone constraints. Anchors zero through seven use witness indices [0, 17, 0, 2, 18, 0, 0, 7]; cell47_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell47_check : cell47.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell48 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 48 for the fixed row-04 divisor, with 25 affine cone constraints. Anchors zero through seven use witness indices [0, 17, 0, 2, 10, 0, 0, 7]; cell48_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell48_check : cell48.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell49 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 49 for the fixed row-04 divisor, with 23 affine cone constraints. Anchors zero through seven use witness indices [0, 17, 0, 2, 9, 0, 0, 4]; cell49_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell49_check : cell49.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell50 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 50 for the fixed row-04 divisor, with 24 affine cone constraints. Anchors zero through seven use witness indices [0, 17, 0, 2, 9, 0, 0, 5]; cell50_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell50_check : cell50.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell51 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 51 for the fixed row-04 divisor, with 24 affine cone constraints. Anchors zero through seven use witness indices [0, 17, 0, 2, 9, 0, 0, 6]; cell51_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell51_check : cell51.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell52 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 52 for the fixed row-04 divisor, with 24 affine cone constraints. Anchors zero through seven use witness indices [0, 17, 0, 2, 9, 0, 0, 7]; cell52_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell52_check : cell52.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell53 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 53 for the fixed row-04 divisor, with 22 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 21, 3, 0, 0, 22]; cell53_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell53_check : cell53.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell54 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 54 for the fixed row-04 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 5, 3, 0, 0, 5]; cell54_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell54_check : cell54.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell55 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 55 for the fixed row-04 divisor, with 23 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 23, 3, 0, 0, 24]; cell55_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell55_check : cell55.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell56 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 56 for the fixed row-04 divisor, with 22 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 25, 3, 0, 0, 6]; cell56_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell56_check : cell56.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell57 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 57 for the fixed row-04 divisor, with 23 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 26, 3, 0, 0, 5]; cell57_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell57_check : cell57.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell58 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 58 for the fixed row-04 divisor, with 24 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 27, 3, 0, 0, 28]; cell58_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell58_check : cell58.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell59 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 59 for the fixed row-04 divisor, with 24 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 27, 3, 0, 0, 7]; cell59_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell59_check : cell59.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell60 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 60 for the fixed row-04 divisor, with 24 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 29, 3, 0, 0, 24]; cell60_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell60_check : cell60.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell61 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 61 for the fixed row-04 divisor, with 24 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 26, 3, 0, 0, 24]; cell61_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell61_check : cell61.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell62 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 62 for the fixed row-04 divisor, with 23 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 27, 3, 0, 0, 6]; cell62_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell62_check : cell62.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell63 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 63 for the fixed row-04 divisor, with 23 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 21, 8, 0, 0, 22]; cell63_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell63_check : cell63.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell64 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 64 for the fixed row-04 divisor, with 24 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 26, 8, 0, 0, 5]; cell64_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell64_check : cell64.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell65 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 65 for the fixed row-04 divisor, with 25 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 26, 8, 0, 0, 24]; cell65_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell65_check : cell65.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell66 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 66 for the fixed row-04 divisor, with 22 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 5, 8, 0, 0, 5]; cell66_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell66_check : cell66.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell67 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 67 for the fixed row-04 divisor, with 23 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 25, 8, 0, 0, 6]; cell67_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell67_check : cell67.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell68 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 68 for the fixed row-04 divisor, with 25 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 27, 8, 0, 0, 28]; cell68_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell68_check : cell68.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell69 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 69 for the fixed row-04 divisor, with 25 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 27, 8, 0, 0, 7]; cell69_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell69_check : cell69.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell70 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 70 for the fixed row-04 divisor, with 24 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 23, 8, 0, 0, 24]; cell70_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell70_check : cell70.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell71 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 71 for the fixed row-04 divisor, with 25 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 29, 8, 0, 0, 24]; cell71_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell71_check : cell71.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell72 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 72 for the fixed row-04 divisor, with 23 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 21, 9, 0, 0, 22]; cell72_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell72_check : cell72.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell73 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 73 for the fixed row-04 divisor, with 22 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 5, 9, 0, 0, 5]; cell73_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell73_check : cell73.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell74 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 74 for the fixed row-04 divisor, with 24 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 23, 9, 0, 0, 24]; cell74_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell74_check : cell74.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell75 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 75 for the fixed row-04 divisor, with 24 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 26, 9, 0, 0, 5]; cell75_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell75_check : cell75.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell76 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 76 for the fixed row-04 divisor, with 23 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 25, 9, 0, 0, 6]; cell76_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell76_check : cell76.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell77 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 77 for the fixed row-04 divisor, with 25 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 27, 9, 0, 0, 28]; cell77_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell77_check : cell77.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell78 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 78 for the fixed row-04 divisor, with 25 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 27, 9, 0, 0, 7]; cell78_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell78_check : cell78.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell79 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 79 for the fixed row-04 divisor, with 25 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 29, 9, 0, 0, 24]; cell79_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell79_check : cell79.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell80 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 80 for the fixed row-04 divisor, with 23 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 21, 10, 0, 0, 22]; cell80_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell80_check : cell80.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell81 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 81 for the fixed row-04 divisor, with 22 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 5, 10, 0, 0, 5]; cell81_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell81_check : cell81.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell82 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 82 for the fixed row-04 divisor, with 24 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 23, 10, 0, 0, 24]; cell82_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell82_check : cell82.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell83 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 83 for the fixed row-04 divisor, with 24 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 26, 10, 0, 0, 5]; cell83_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell83_check : cell83.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell84 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 84 for the fixed row-04 divisor, with 23 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 25, 10, 0, 0, 6]; cell84_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell84_check : cell84.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell85 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 85 for the fixed row-04 divisor, with 25 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 27, 10, 0, 0, 28]; cell85_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell85_check : cell85.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell86 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 86 for the fixed row-04 divisor, with 25 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 27, 10, 0, 0, 7]; cell86_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell86_check : cell86.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell87 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 87 for the fixed row-04 divisor, with 25 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 29, 10, 0, 0, 24]; cell87_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell87_check : cell87.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell88 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 88 for the fixed row-04 divisor, with 24 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 27, 8, 0, 0, 6]; cell88_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell88_check : cell88.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell89 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 89 for the fixed row-04 divisor, with 24 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 27, 9, 0, 0, 6]; cell89_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell89_check : cell89.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell90 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 90 for the fixed row-04 divisor, with 24 affine cone constraints. Anchors zero through seven use witness indices [0, 1, 0, 27, 10, 0, 0, 6]; cell90_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell90_check : cell90.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell91 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 91 for the fixed row-04 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 8, 0, 21, 8, 0, 0, 22]; cell91_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell91_check : cell91.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell92 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 92 for the fixed row-04 divisor, with 20 affine cone constraints. Anchors zero through seven use witness indices [0, 8, 0, 5, 8, 0, 0, 5]; cell92_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell92_check : cell92.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell93 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 93 for the fixed row-04 divisor, with 22 affine cone constraints. Anchors zero through seven use witness indices [0, 8, 0, 26, 8, 0, 0, 5]; cell93_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell93_check : cell93.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell94 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 94 for the fixed row-04 divisor, with 21 affine cone constraints. Anchors zero through seven use witness indices [0, 8, 0, 25, 8, 0, 0, 6]; cell94_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell94_check : cell94.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell95 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 95 for the fixed row-04 divisor, with 23 affine cone constraints. Anchors zero through seven use witness indices [0, 8, 0, 27, 8, 0, 0, 28]; cell95_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell95_check : cell95.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell96 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 96 for the fixed row-04 divisor, with 23 affine cone constraints. Anchors zero through seven use witness indices [0, 8, 0, 27, 8, 0, 0, 7]; cell96_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell96_check : cell96.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.cell97 : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core

Closed-cover cell 97 for the fixed row-04 divisor, with 22 affine cone constraints. Anchors zero through seven use witness indices [0, 8, 0, 23, 8, 0, 0, 24]; cell97_check verifies its explicit-potential certificate.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.cell97_check : cell97.certificate.checkClosed 4 = true

def AtanasovRanganathan.GenusFiveRow04CoverCells0.chunk : List (GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core)

The ordered row-04 closed-cover cell block with global indices 0 through 97, used when assembling the full 195-cell cover.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow04CoverCells0.chunk_check : (chunk.all fun (cell : GenusFiveClosedCover.CoordinateCell GenusFiveCoreAtlas.row04Core) => cell.certificate.checkClosed 4) = true