Closed construction coverage of the cubic genus-five atlas

The canonical classifier returns occurrence-sensitive core relabelings. The first sixteen rows are exactly the Atanasov--Ranganathan construction atlas; the remaining four rows are the bridge types and are deliberately left as a separate structural branch.

def AtanasovRanganathan.GenusFiveCubicCoverage.BridgeAtlasClosedCoverage : Prop

The finite structural obligation left after the sixteen AR rows: every closed face of each of the four cubic bridge cores carries a degree-four rank-one pencil.

Equations

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

theorem AtanasovRanganathan.GenusFiveCubicCoverage.closedConstruction_of_mem_arAtlas (constructions : GenusFiveConstructions.CubicAtlasConstructions) (row : GenusFiveCubicAtlas.Row) (hRow : row ∈ GenusFiveCubicAtlas.arAtlas) : Configurations.ClosedSubdivisionDharConstruction row.core BridgeAtlasClosedCoverage._proof_1

Read the aggregate of sixteen public AR constructions against the public cubic-atlas row type.

theorem AtanasovRanganathan.GenusFiveCubicCoverage.classified_closed_or_bridge (constructions : GenusFiveConstructions.CubicAtlasConstructions) (candidate : Utilities.Certificate.ExplicitPotential.Core 8 12) (hConnected : candidate.Connected) (hLoopless : ∀ (edge : Fin 12), candidate.tail edge ≠ candidate.head edge) (hCubic : candidate.Cubic) : Configurations.ClosedSubdivisionDharConstruction candidate BridgeAtlasClosedCoverage._proof_1 ∨ ∃ row ∈ GenusFiveCubicAtlas.bridgeAtlas, Nonempty (candidate.Relabeling row.core)

A classified cubic core either inherits one of the sixteen closed AR constructions or is one of the four explicit bridge rows.

theorem AtanasovRanganathan.GenusFiveCubicCoverage.classified_closed_or_bridge_of_sizes {n p : ℕ} (candidate : Utilities.Certificate.ExplicitPotential.Core n p) (hVertices : n = 8) (hSlots : p = 12) (constructions : GenusFiveConstructions.CubicAtlasConstructions) (hConnected : candidate.Connected) (hLoopless : ∀ (edge : Fin p), candidate.tail edge ≠ candidate.head edge) (hCubic : candidate.Cubic) : Configurations.ClosedSubdivisionDharConstruction candidate ⋯ ∨ ∃ row ∈ GenusFiveCubicAtlas.bridgeAtlas, Nonempty (candidate.Relabeling row.core)

Size-indexed wrapper used by trivalent expansion. The expansion computes its cubic size arithmetically, so keeping the equalities explicit avoids any ad-hoc cast of ordered core occurrences.

theorem AtanasovRanganathan.GenusFiveCubicCoverage.classified_closed_of_bridgeCoverage (constructions : GenusFiveConstructions.CubicAtlasConstructions) (bridges : BridgeAtlasClosedCoverage) (candidate : Utilities.Certificate.ExplicitPotential.Core 8 12) (hConnected : candidate.Connected) (hLoopless : ∀ (edge : Fin 12), candidate.tail edge ≠ candidate.head edge) (hCubic : candidate.Cubic) : Configurations.ClosedSubdivisionDharConstruction candidate BridgeAtlasClosedCoverage._proof_1

Once the four bridge rows are closed structurally, the public classifier returns a closed construction for every connected loopless cubic 8/12 core.

theorem AtanasovRanganathan.GenusFiveCubicCoverage.classified_closed_of_sizes {n p : ℕ} (candidate : Utilities.Certificate.ExplicitPotential.Core n p) (hVertices : n = 8) (hSlots : p = 12) (constructions : GenusFiveConstructions.CubicAtlasConstructions) (bridges : BridgeAtlasClosedCoverage) (hConnected : candidate.Connected) (hLoopless : ∀ (edge : Fin p), candidate.tail edge ≠ candidate.head edge) (hCubic : candidate.Cubic) : Configurations.ClosedSubdivisionDharConstruction candidate ⋯

Size-indexed form of classified_closed_of_bridgeCoverage, for the arithmetically sized output of trivalent expansion.