From once-marked Brill--Noether existence to the gonality and Brill--Noether conjectures #
OnceMarkedBNExistence G u (Utilities/Grassmannian/OnceMarked.lean) describes
the Young-diagram divisor census of a once-marked graph (G, u). This file relates it to
two standard statements, both
from the dependency ChipFiringWithLean.RiemannRoch:
gonalityConjecture h_conn : gonality h_conn ≤ (genus G + 3) / 2brillNoetherConjecture h_conn r d : 0 ≤ ρ → ∃ D, rank G D ≥ r ∧ deg D = d
The rectangular Young diagram #
The row form onceMarkedBNExists_iff_rank_rows gives, for a normalized D (deg D = g)
and i < lambda.rowLens.length,
rank G (D + (i - lambda.rowLens[i]) • oneChip u) ≥ i.
The index i here is the target rank, not merely a label: to extract a rank-≥ r
conclusion one must plug in i = r, and lambda.rowLens is 0-indexed with only
positive entries (Mathlib's YoungDiagram.rowLens never stores a zero row). A
single-row diagram therefore only ever supplies the row-0 condition (rank ≥ 0,
trivial) — it cannot produce rank ≥ 1. To reach row index r at all, lambda needs
at least r + 1 (positive-length) rows.
The right shape is the standard Brill--Noether rectangle: r + 1 rows, each of length
n := rectangleWidth G r d = genus G - d + r (Utilities/Foundations/ Parameters.lean). Its row r is exactly the n-length row (rowLens[r] = n, since all
r + 1 rows are equal), so the row-form condition at i = r reads
rank G (D + (r - n) • oneChip u) ≥ r, of degree g + r - n = d.
The diagram's cardinality is (r + 1) * n, so OnceMarkedBNExistence supplies this
witness exactly when (r + 1) * n ≤ g, i.e. bnNumber G r d ≥ 0 — the Brill--Noether
number ρ. This is not the 1 ≤ d bound from the single-row guess; it is the sharp
ρ ≥ 0 condition, and for r = 1 its smallest solution in d is exactly
(genus G + 3) / 2, which is what makes gonalityConjecture_of_onceMarkedBNExistence
below go through with no slack.
When n ≤ 0 (d ≥ genus G + r) the rectangle degenerates and no census input is needed
at all: deg (d • oneChip u) = d ≥ genus G + r makes Riemann's inequality
(rank_ge_deg_sub_genus) alone give rank ≥ r. bnExists_of_onceMarkedBNExistence
below case-splits exactly on this sign.
The (r + 1) x n Brill--Noether rectangle: r + 1 equal rows of length n. Only
used with n > 0; the case n ≤ 0 never needs a Young diagram at all (see the module
docstring), so this definition is never asked about n = 0 downstream, but it is defined
totally (as ⊥) for that input so the surrounding construction stays a plain function.
Equations
- Utilities.bnRectangle r n = if n = 0 then ⊥ else YoungDiagram.ofRowLens (List.replicate (r + 1) n) ⋯
Instances For
The general bridging lemma: OnceMarkedBNExistence supplies a rank-≥ r divisor of
every degree d with ρ(r, d) ≥ 0, matching brillNoetherConjecture's hypothesis
exactly (via bnNumber). No hypothesis on the sign of rectangleWidth G r d is needed:
the proof case-splits on it internally (see the module docstring).
The r = 1 specialization, phrased exactly as the reader-recognisable
BNExists G 1 d (Utilities/Foundations/Parameters.lean).
A public replacement for the dependency's private lemma gonality_le_genus_add_one's
proof pattern: any witness of gonalityLeq G k bounds the noncomputable gonality
above by k. The dependency does not export a lemma of this shape (its own version is
private), so this re-derives the two ingredients (BddBelow and csInf_le) from the
public rank_geq_iff / rank_le_degree.
The gonality conjecture in this genus follows from once-marked Brill--Noether
existence: the minimal degree d = (genus G + 3) / 2 with ρ(1, d) ≥ 0 is a rank-≥ 1
divisor degree by bnExists_one_of_onceMarkedBNExistence, and gonality_le_of_ gonalityLeq transports that into a bound on the dependency's noncomputable
gonality.
The Brill--Noether conjecture in this genus follows from once-marked Brill--Noether
existence, for every r d : ℤ. The r ≥ 0 case is bnExists_of_onceMarkedBNExistence
after lifting r to ℕ; the r < 0 case is trivial, since rank G D ≥ -1 always
(rank_geq_neg_one) and r ≤ -1.