A formal interface for the Atanasov--Ranganathan low-genus program

The paper's finite configuration analysis is naturally stated uniformly over all positive integral subdivisions of a fixed loopless core. This file gives that obligation a name and connects it to the public low-genus existence reduction.

It also closes one infinite genus-five family: a loopless two-vertex core with six edge slots. Every such subdivision is a genus-five banana graph, and its two endpoint chips already have rank one. Padding that pencil by two effective chips supplies the critical degree-four divisor.

The remaining work is geometric, not arithmetic: prove the corresponding PositiveSubdivisionPencil assertions for the finitely many loopless cubic cores, and connect the loop, bridge, and contraction reductions to those core statements.

def AtanasovRanganathan.PositiveSubdivisionPencil {n p : ℕ} (core : Utilities.Certificate.ExplicitPotential.Core n p) (core_nonempty : 0 < n) (core_loopless : ∀ (edge : Fin p), core.tail edge ≠ core.head edge) (degree : ℤ) : Prop

A fixed ordered loopless core carries a degree-degree rank-one pencil on every assignment of positive integral edge lengths. This is the exact target proved by each uniform configuration calculation in the paper.

Equations

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

def AtanasovRanganathan.GenusFivePseudocorePencils : Prop

The finite geometric genus-five boundary produced by the public pseudocore normal form. Each input is a valid loop-aware pseudocore with at most eight base vertices; the obligation is uniform over every positive subdivision of its checked loopless split.

This formulation deliberately does not mention the historical numbering of the sixteen cubic pictures. A finite catalog theorem may discharge these quantifiers later, while structural proofs can already handle looped, separated, and small-core families directly.

Equations

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

theorem AtanasovRanganathan.genusFiveRankOneExistence_of_pseudocorePencils (pencils : GenusFivePseudocorePencils) : Utilities.GenusFiveRankOneExistence

The fossil and public pseudocore presentation reduce the whole genus-five critical-pencil theorem to GenusFivePseudocorePencils.

Passing to the fossil contracts every pendant tree and every separating bridge at once. Its rank and genus agree with the source, and its two-edge cut condition supplies the leafless hypothesis needed by the pseudocore presentation. This replaces the former recursive, one-leaf-at-a-time load-bearing reduction.

structure AtanasovRanganathan.GeometricInputs : Prop

Exact high-level inputs for the direct proof: the already-isolated genus-four pencil theorem and the finite genus-five pseudocore family.

• genusFour : Utilities.GenusFourRankOneExistence
• genusFivePseudocores : GenusFivePseudocorePencils

theorem AtanasovRanganathan.GeometricInputs.toCriticalPencils (inputs : GeometricInputs) : Utilities.LowGenusCriticalPencils

The geometric inputs assemble into the two critical pencils consumed by the low-genus arithmetic reduction.

theorem AtanasovRanganathan.brillNoetherExistenceThroughFive_of_geometricInputs (inputs : GeometricInputs) : Utilities.BrillNoetherExistenceThroughFive

Once the two geometric inputs are proved, the full Atanasov--Ranganathan existence theorem follows with no further mathematics.

theorem AtanasovRanganathan.positiveSubdivisionPencil_twoVertex_degreeFour {p : ℕ} (core : Utilities.Certificate.ExplicitPotential.Core 2 p) (core_loopless : ∀ (edge : Fin p), core.tail edge ≠ core.head edge) : PositiveSubdivisionPencil core positiveSubdivisionPencil_twoVertex_degreeFour._proof_1 core_loopless 4

The endpoint pencil proves the degree-four subdivision obligation for every loopless two-vertex core, independently of its number of edge slots.

theorem AtanasovRanganathan.genusFivePseudocorePencil_of_splitVertexCount_eq_two {vertexCount : ℕ} {core : Utilities.Certificate.GenusFourPseudocore.Pseudocore vertexCount} {split : core.SplitMetadata} (hCount : vertexCount + core.loopCount = 2) (spec : Utilities.Certificate.SubdivisionGraph.Spec (vertexCount + core.loopCount) core.splitEdgeCount) (_hCore : spec.core = split.splitCore) : Utilities.BNExists spec.graph 1 4

The two-vertex endpoint pencil directly retires every pseudocore whose loopless split has two vertices. This is phrased at the exact finite boundary used by GenusFivePseudocorePencils.

theorem AtanasovRanganathan.genus_twoVertex_sixEdges (spec : Utilities.Certificate.SubdivisionGraph.Spec 2 6) : spec.graph.genus = 5

A positive subdivision of a two-vertex, six-edge core has genus five.

theorem AtanasovRanganathan.genusFivePencil_twoVertex_sixEdges (spec : Utilities.Certificate.SubdivisionGraph.Spec 2 6) : Utilities.BNExists spec.graph 1 4

The first completed genus-five structural family in the direct Atanasov--Ranganathan track.

theorem AtanasovRanganathan.twoVertexCore_connected_of_edge {p : ℕ} (spec : Utilities.Certificate.SubdivisionGraph.Spec 2 p) (edge : Fin p) : spec.core.Connected

Any loopless two-vertex core with at least one named edge slot is connected. Stating the elementary finite argument here lets the completed banana family feed the semantic Brill--Noether theorem, not merely the subdivision-level pencil interface.

theorem AtanasovRanganathan.graph_connected_twoVertex_sixEdges (spec : Utilities.Certificate.SubdivisionGraph.Spec 2 6) : graphConnected spec.graph

Every positive subdivision of a loopless two-vertex, six-edge core is connected.

theorem AtanasovRanganathan.brillNoetherConjecture_twoVertex_sixEdges (spec : Utilities.Certificate.SubdivisionGraph.Spec 2 6) (r d : ℤ) : brillNoetherConjecture ⋯ r d

The full Brill--Noether existence conjecture, at every admissible (r,d), for the completed genus-five banana family.