Public genus-four reduction to six closed cubic rows

After fossilization, a genus-four graph is connected and leafless. Its pseudocore has either a semantic loop, which splits off as a rigid genus-one factor from a genus-three base, or no semantic loops. In the latter case stability permits the centipede expansion to a connected loopless cubic core with exactly six vertices and nine slots.

Consequently the whole genus-four critical-pencil theorem reduces directly to closed degree-three pencils on connected loopless cubic 6/9 cores. No 111-row pseudocore catalog is needed by this unmarked proof.

def AtanasovRanganathan.GenusFourPseudocoreCoverage.CubicClosedCoverage : Prop

Exact finite input for the public genus-four reduction: every connected loopless cubic 6/9 core carries a degree-three pencil on all of its nonloopy forest faces.

Equations

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

theorem AtanasovRanganathan.GenusFourPseudocoreCoverage.closedPencil_of_sizes (coverage : CubicClosedCoverage) {n p : ℕ} (candidate : Utilities.Certificate.ExplicitPotential.Core n p) (hVertices : n = 6) (hSlots : p = 9) (hConnected : candidate.Connected) (hLoopless : ∀ (edge : Fin p), candidate.tail edge ≠ candidate.head edge) (hCubic : candidate.Cubic) (length : Fin p → ℕ) (hForest : Utilities.Certificate.ContractionForestCensusGeneral.IsForest candidate (Configurations.zeroSlots length)) (hNotLoopy : ¬Utilities.Certificate.ContractionForestCensusGeneral.IsLoopy candidate (Configurations.zeroSlots length)) : Utilities.BNExists (Configurations.faceSpec candidate ⋯ length hForest hNotLoopy).graph 1 3

Size-indexed form of cubic coverage, for the arithmetically sized centipede expansion.

theorem AtanasovRanganathan.GenusFourPseudocoreCoverage.bnExists_of_loopCount_pos {vertexCount : ℕ} {core : Utilities.Certificate.GenusFourPseudocore.Pseudocore vertexCount} (split : core.SplitMetadata) (hValid : core.ValidAt 4) (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 3

A semantic loop splits off as a rigid genus-one cycle from a connected genus-three base, where the canonical degree-three wedge pencil applies.

theorem AtanasovRanganathan.GenusFourPseudocoreCoverage.bnExists_of_loopCount_zero (coverage : CubicClosedCoverage) {vertexCount : ℕ} {core : Utilities.Certificate.GenusFourPseudocore.Pseudocore vertexCount} (split : core.SplitMetadata) (hValid : core.ValidAt 4) (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 3

A loopless valid genus-four pseudocore expands to the 6/9 cubic closed boundary and therefore inherits its degree-three pencil.

theorem AtanasovRanganathan.GenusFourPseudocoreCoverage.genusFourRankOneExistence_of_cubicClosedCoverage (coverage : CubicClosedCoverage) : Utilities.GenusFourRankOneExistence

Closed coverage of the six cubic rows implies the global genus-four degree-three rank-one theorem.