Brill--Noether existence through genus five from the two critical pencils

Atanasov--Ranganathan reduce Brill--Noether existence in genera at most five to two rank-one statements:

• every connected genus-four graph has a degree-three rank-one divisor;
• every connected genus-five graph has a degree-four rank-one divisor.

This file formalizes that reduction independently of their geometric case analysis. In particular, the two inputs below are the exact public boundary for a direct formalization of their proof. No marked divisor, contraction compatibility, or transmission condition occurs here.

The library's BNExists G r d uses the equivalent convenient convention "degree exactly d and rank at least r". The dependency's brillNoetherConjecture uses the same convention with the Brill--Noether inequality exposed as an implication.

def Utilities.GenusFourRankOneExistence : Prop

The genus-four geometric heart of the Atanasov--Ranganathan theorem.

Equations

• Utilities.GenusFourRankOneExistence = ∀ (G : CFGraph), graphConnected G → G.genus = 4 → Utilities.BNExists G 1 3

def Utilities.GenusFiveRankOneExistence : Prop

The genus-five geometric heart of the Atanasov--Ranganathan theorem.

Equations

• Utilities.GenusFiveRankOneExistence = ∀ (G : CFGraph), graphConnected G → G.genus = 5 → Utilities.BNExists G 1 4

structure Utilities.LowGenusCriticalPencils : Prop

The two genuinely geometric inputs left after the low-genus arithmetic reduction.

• genusFour : GenusFourRankOneExistence
• genusFive : GenusFiveRankOneExistence

theorem Utilities.bnNumber_nonneg_iff_rectangle_area_le (G : CFGraph) (r d : ℤ) : 0 ≤ bnNumber G r d ↔ (r + 1) * rectangleWidth G r d ≤ G.genus

Nonnegativity of the Brill--Noether number is the rectangle-area bound.

theorem Utilities.bnExists_of_genus_le_three {G : CFGraph} (hG : graphConnected G) (hGenus : G.genus ≤ 3) {r d : ℤ} (hR : 0 ≤ r) (hRho : 0 ≤ bnNumber G r d) : BNExists G r d

Every admissible Brill--Noether parameter pair on a connected graph of genus at most three is elementary.

theorem Utilities.bnExists_genus_four_of_rankOneDegreeThree {G : CFGraph} (hG : graphConnected G) (hGenus : G.genus = 4) (hCritical : BNExists G 1 3) {r d : ℤ} (hR : 0 ≤ r) (hRho : 0 ≤ bnNumber G r d) : BNExists G r d

In genus four, r = 1, d = 3 is the only admissible pair outside the elementary range.

theorem Utilities.bnExists_genus_five_of_rankOneDegreeFour {G : CFGraph} (hG : graphConnected G) (hGenus : G.genus = 5) (hCritical : BNExists G 1 4) {r d : ℤ} (hR : 0 ≤ r) (hRho : 0 ≤ bnNumber G r d) : BNExists G r d

In genus five, r = 1, d = 4 is the only admissible pair outside the elementary range.

theorem Utilities.bnExists_of_genus_le_five_of_criticalPencils (critical : LowGenusCriticalPencils) {G : CFGraph} (hG : graphConnected G) (hGenus : G.genus ≤ 5) {r d : ℤ} (hR : 0 ≤ r) (hRho : 0 ≤ bnNumber G r d) : BNExists G r d

The two critical pencils imply BNExists for every nonnegative rank and every admissible parameter pair in genus at most five.

theorem Utilities.brillNoetherConjecture_of_genus_le_five_of_criticalPencils (critical : LowGenusCriticalPencils) (G : CFGraph) (hG : graphConnected G) (hGenus : G.genus ≤ 5) (r d : ℤ) : brillNoetherConjecture hG r d

Atanasov--Ranganathan's two critical rank-one assertions imply the full Brill--Noether existence conjecture for every connected graph of genus at most five.

def Utilities.BrillNoetherExistenceThroughFive : Prop

The proposition represented by the paper's main theorem in the library's degree-exact, rank-lower-bound convention.

Equations

• Utilities.BrillNoetherExistenceThroughFive = ∀ (G : CFGraph) (hG : graphConnected G), G.genus ≤ 5 → ∀ (r d : ℤ), brillNoetherConjecture hG r d

theorem Utilities.criticalPencils_imply_brillNoetherExistenceThroughFive (critical : LowGenusCriticalPencils) : BrillNoetherExistenceThroughFive