Elementary Brill--Noether existence

The predicate BNExists is immediate in three parameter ranges: rank zero, nonpositive rectangle width, and rectangle width one. These arguments use only effective divisors, the degree bound for winnability, and graph Riemann--Roch.

theorem Utilities.BNExists_rank_zero {G : CFGraph} {d : ℤ} (hRho : 0 ≤ bnNumber G 0 d) : BNExists G 0 d

The Brill--Noether inequality at rank zero just says that d is nonnegative, so an effective divisor of degree d is a witness.

theorem Utilities.BNExists_of_width_nonpos {G : CFGraph} (hG : graphConnected G) {r d : ℤ} (hWidth : rectangleWidth G r d ≤ 0) : BNExists G r d

If the rectangle width is nonpositive, every rank test leaves degree at least the genus and is therefore winnable.

theorem Utilities.BNExists_of_width_one {G : CFGraph} (hG : graphConnected G) {r d : ℤ} (_hR : 0 ≤ r) (hWidth : rectangleWidth G r d = 1) (hRho : 0 ≤ bnNumber G r d) : BNExists G r d

At rectangle width one, subtract an effective divisor of degree rho from the canonical divisor and apply Riemann--Roch.

theorem Utilities.BNExists_elementary {G : CFGraph} (hG : graphConnected G) {r d : ℤ} (hR : 0 ≤ r) (hRho : 0 ≤ bnNumber G r d) (hEasy : r = 0 ∨ rectangleWidth G r d ≤ 1) : BNExists G r d

The complete elementary range: rank zero or rectangle width at most one.