One canonical construction for six positive genus-five rows #

Two connected leafless genus-two factors carry effective canonical pencils. The three-case connector lemma reaches the four attachment vertices, and all other core vertices already carry chips. The finite data choose each connector in turn; no length chamber or graph-isomorphism certificate is used.

The theorem here concerns positive subdivisions. GenusFiveTwoPoleClosed extends the same weights to contraction faces by discrete specialization.

source

theorem AtanasovRanganathan.GenusFiveTwoPole.rank_ge_one_of_twoPoleData {n p : ℕ} (s : Utilities.Certificate.SubdivisionGraph.Spec n p) (hConnected : graphConnected s.graph) (weight : Fin n → ℤ) (hNonnegative : ∀ (v : Fin n), 0 ≤ weight v) (data : Fin 2 → Utilities.Certificate.TwoPoleSubdivision.Data s.core 4 5 4 5) (hLeftConnected : ∀ (i : Fin 2), (data i).leftCore.Connected) (hRightConnected : ∀ (i : Fin 2), (data i).rightCore.Connected) (hLeftLeafless : ∀ (i : Fin 2) (v : Fin 4), 2 ≤ (data i).leftCore.incidenceDegree v) (hRightLeafless : ∀ (i : Fin 2) (v : Fin 4), 2 ≤ (data i).rightCore.incidenceDegree v) (hWeightLeft : ∀ (i : Fin 2) (a : Fin 4), weight ((data i).vertices (Sum.inl a)) = ↑((data i).leftCore.incidenceDegree a) - 2) (hWeightRight : ∀ (i : Fin 2) (b : Fin 4), weight ((data i).vertices (Sum.inr b)) = ↑((data i).rightCore.incidenceDegree b) - 2) (hCover : ∀ (v : Fin n), 1 ≤ weight v ∨ ∃ (i : Fin 2), v = (data i).vertices (Sum.inl ((data i).leftPole 0)) ∨ v = (data i).vertices (Sum.inr ((data i).rightPole 0))) :

rank s.graph (Utilities.Subdivision.SubdivisionCoreSupport.coreDivisor s weight) ≥ 1

The fixed core-supported sum of the two local canonical divisors has rank at least one when every unsupported core vertex is an attachment vertex in one of the two displayed connector orders.

source

theorem AtanasovRanganathan.GenusFiveTwoPole.bnExists_of_twoPoleData {n p : ℕ} (s : Utilities.Certificate.SubdivisionGraph.Spec n p) (hConnected : graphConnected s.graph) (weight : Fin n → ℤ) (hNonnegative : ∀ (v : Fin n), 0 ≤ weight v) (hDegree : ∑ v : Fin n, weight v = 4) (data : Fin 2 → Utilities.Certificate.TwoPoleSubdivision.Data s.core 4 5 4 5) (hLeftConnected : ∀ (i : Fin 2), (data i).leftCore.Connected) (hRightConnected : ∀ (i : Fin 2), (data i).rightCore.Connected) (hLeftLeafless : ∀ (i : Fin 2) (v : Fin 4), 2 ≤ (data i).leftCore.incidenceDegree v) (hRightLeafless : ∀ (i : Fin 2) (v : Fin 4), 2 ≤ (data i).rightCore.incidenceDegree v) (hWeightLeft : ∀ (i : Fin 2) (a : Fin 4), weight ((data i).vertices (Sum.inl a)) = ↑((data i).leftCore.incidenceDegree a) - 2) (hWeightRight : ∀ (i : Fin 2) (b : Fin 4), weight ((data i).vertices (Sum.inr b)) = ↑((data i).rightCore.incidenceDegree b) - 2) (hCover : ∀ (v : Fin n), 1 ≤ weight v ∨ ∃ (i : Fin 2), v = (data i).vertices (Sum.inl ((data i).leftPole 0)) ∨ v = (data i).vertices (Sum.inr ((data i).rightPole 0))) :

Utilities.BNExists s.graph 1 4

Package the fixed canonical divisor as the existing degree-four Brill–Noether existence statement.

source