Structural coverage of genus-five pseudocores

A semantic loop in the pseudocore split is a pointed rigid genus-one wedge factor. Removing it leaves a connected genus-four base, so the public genus-four pencil theorem and the generic corrected wedge construction give a degree-four pencil on the original subdivision. Thus the finite cubic atlas only has to handle the loopless pseudocore branch.

theorem AtanasovRanganathan.GenusFivePseudocoreCoverage.bnExists_of_loopCount_pos (genusFour : Utilities.GenusFourRankOneExistence) {vertexCount : ℕ} {core : Utilities.Certificate.GenusFourPseudocore.Pseudocore vertexCount} (split : core.SplitMetadata) (hValid : core.ValidAt 5) (hCompatible : Utilities.Certificate.PseudocoreSplitGlue.Compatible split) (spec : Utilities.Certificate.SubdivisionGraph.Spec (vertexCount + core.loopCount) core.splitEdgeCount) (hCore : spec.core = split.splitCore) (hLoopCount : 0 < core.loopCount) : Utilities.BNExists spec.graph 1 4

Every valid genus-five pseudocore carrying at least one semantic loop is solved by splitting off one displayed rigid cycle.

theorem AtanasovRanganathan.GenusFivePseudocoreCoverage.bnExists_or_bridge_of_loopCount_zero (constructions : GenusFiveConstructions.CubicAtlasConstructions) {vertexCount : ℕ} {core : Utilities.Certificate.GenusFourPseudocore.Pseudocore vertexCount} (split : core.SplitMetadata) (hValid : core.ValidAt 5) (hCompatible : Utilities.Certificate.PseudocoreSplitGlue.Compatible split) (spec : Utilities.Certificate.SubdivisionGraph.Spec (vertexCount + core.loopCount) core.splitEdgeCount) (hCore : spec.core = split.splitCore) (hLoopCount : core.loopCount = 0) : Utilities.BNExists spec.graph 1 4 ∨ ∃ row ∈ GenusFiveCubicAtlas.bridgeAtlas, Nonempty ((Utilities.Subdivision.TrivalentExpansion.data spec.core ⋯).bigCore.Relabeling row.core)

In the absence of semantic loops, stability makes the displayed core a minimum-valence-three core. Its centipede expansion is a cubic 8/12 core. The public classifier therefore either supplies one of the sixteen closed AR constructions, which immediately descends to the original subdivision, or identifies one of the four explicit bridge rows.

theorem AtanasovRanganathan.GenusFivePseudocoreCoverage.bnExists_of_loopCount_zero (constructions : GenusFiveConstructions.CubicAtlasConstructions) (bridges : GenusFiveCubicCoverage.BridgeAtlasClosedCoverage) {vertexCount : ℕ} {core : Utilities.Certificate.GenusFourPseudocore.Pseudocore vertexCount} (split : core.SplitMetadata) (hValid : core.ValidAt 5) (hCompatible : Utilities.Certificate.PseudocoreSplitGlue.Compatible split) (spec : Utilities.Certificate.SubdivisionGraph.Spec (vertexCount + core.loopCount) core.splitEdgeCount) (hCore : spec.core = split.splitCore) (hLoopCount : core.loopCount = 0) : Utilities.BNExists spec.graph 1 4

Closed structural coverage of the four bridge rows turns the loopless pseudocore reduction into an unconditional pencil.

theorem AtanasovRanganathan.GenusFivePseudocoreCoverage.genusFivePseudocorePencils_of_bridgeCoverage (genusFour : Utilities.GenusFourRankOneExistence) (bridges : GenusFiveCubicCoverage.BridgeAtlasClosedCoverage) : GenusFivePseudocorePencils

The genus-four theorem and the finite four-row bridge obligation discharge the exact public genus-five pseudocore interface.

theorem AtanasovRanganathan.GenusFivePseudocoreCoverage.brillNoetherExistenceThroughFive_of_bridgeCoverage (genusFour : Utilities.GenusFourRankOneExistence) (bridges : GenusFiveCubicCoverage.BridgeAtlasClosedCoverage) : Utilities.BrillNoetherExistenceThroughFive

Public end-to-end assembly with only the genus-four theorem and the four structural bridge rows exposed as inputs.