Large-period general transmission implies Brill--Noether generality

This is Proposition 6.1 (prop:kgt-bngenl) of the paper. The paper writes the threshold as k ≥ g / 2 + 1. For natural-number parameters its exact, parity-independent form is g + 2 ≤ 2 * k.

The proof separates the graph theory from the combinatorics. The two rank formulas of lem:tauChars identify a rectangular family of crossing inversions. If that family has more than g members, two normalize to the same k-inversion. The interval between those representatives then supplies at least 2k - 1 distinct k-inversions, contradicting the defining bound.

def Bananas.normalizeFirstInversion (k : ℕ) (p : ℤ × ℤ) : ℤ × ℤ

Normalize an ordinary inversion by moving its first coordinate into the fundamental interval [0,k).

Equations

• Bananas.normalizeFirstInversion k p = (p.1 % ↑k, p.2 - p.1 / ↑k * ↑k)

def Bananas.crossingInversions (τ : ℤ → ℤ) : Set (ℤ × ℤ)

The rectangular family of inversions crossing both coordinate axes.

Equations

• Bananas.crossingInversions τ = northwestSet τ 1 0 ×ˢ southeastSet τ 1 0

theorem Bananas.crossingInversions_ncard (τ : ℤ → ℤ) : (crossingInversions τ).ncard = (northwestSet τ 1 0).ncard * (southeastSet τ 1 0).ncard

theorem Bananas.normalizeFirstInversion_mem_kInversions_of_crossing {k : ℕ} {τ : ℤ → ℤ} (hk : 0 < k) (hAffine : IsKAffine k τ) {p : ℤ × ℤ} (hp : p ∈ crossingInversions τ) : normalizeFirstInversion k p ∈ kInversions k τ

theorem Bananas.exists_crossing_collision {k : ℕ} {τ : ℤ → ℤ} (hk : 0 < k) (hAffine : IsKAffine k τ) (hfinite : (kInversions k τ).Finite) (hlarge : kInversionCount k τ < (crossingInversions τ).ncard) : ∃ p ∈ crossingInversions τ, ∃ q ∈ crossingInversions τ, p ≠ q ∧ normalizeFirstInversion k p = normalizeFirstInversion k q

Pigeonhole step in Proposition 6.1: too many crossing inversions give two distinct ordinary inversions representing the same k-inversion.

theorem Bananas.crossing_collision_inversion_lower_bound {k : ℕ} {τ : ℤ → ℤ} (hk : 0 < k) (hAffine : IsKAffine k τ) (hfinite : (kInversions k τ).Finite) {p q : ℤ × ℤ} (hp : p ∈ crossingInversions τ) (hq : q ∈ crossingInversions τ) (hpq : p ≠ q) (hnorm : normalizeFirstInversion k p = normalizeFirstInversion k q) : 2 * k - 1 ≤ kInversionCount k τ

The combinatorial core of Proposition 6.1. Two different axis-crossing inversions in one affine-equivalence class force a block of at least 2k-1 different classes.

theorem Bananas.kGeneralTransmission_brillNoetherGeneral {M : TwiceMarked} {g k : ℕ} (hconn : _root_.graphConnected M.graph) (hgenus : M.graph.genus = ↑g) (hK : KGeneralTransmission M k) (hthreshold : g + 2 ≤ 2 * k) : BrillNoetherGeneral M.graph

Paper Proposition 6.1 (prop:kgt-bngenl), with the corrected natural threshold g + 2 ≤ 2k.

The paper's standing convention is that graphs are connected; it is explicit here because CFGraph itself does not bundle connectedness.

theorem Bananas.banana_not_brillNoetherGeneral {g : ℕ} (hg : 3 ≤ g) (B : Banana g) : ¬BrillNoetherGeneral (Utilities.Certificate.SubdivisionGraph.Spec.graph B)

TeX label: none (Remark 1.18 is unlabeled); the same deduction is the last step of cor:bananasWithKGT (Corollary 6.4).

Every banana of genus at least three is not Brill--Noether general: its endpoint pencil has degree two and rank one although its Brill--Noether number is 2 - g < 0. This formalizes the final observation in the introduction.