Closed coverage of the six cubic genus-four rows

The canonical classifier returns an occurrence-sensitive relabeling to one of the six fixed cubic rows. Closed-face relabeling therefore turns six named row proofs into the classifier-facing coverage theorem consumed by the public pseudocore reduction.

def AtanasovRanganathan.GenusFourCubicCoverage.RowClosedCoverage : Prop

The six concrete closed-row obligations.

Equations

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

theorem AtanasovRanganathan.GenusFourCubicCoverage.cubicClosedCoverage_of_rows (rows : RowClosedCoverage) : GenusFourPseudocoreCoverage.CubicClosedCoverage

Six closed row proofs and the public canonical classifier cover every connected loopless cubic 6/9 core.