Gonality forced by k-general transmission

The Hurwitz--Brill--Noether consequence needed here is considerably smaller than the full splitting-type census. If a divisor D has degree d < k, then D - k u has negative degree. In the transmission permutation of D this says that the deeper southeast quadrant is empty. Hence the dots in the ordinary southeast quadrant occupy distinct residue classes modulo k, and normalizing the full northwest-by-southeast rectangle gives an injection into the k-inversions.

Together with the defining inversion bound, this excludes rank-one divisors of degree below k whenever k is at most the generic gonality. The reverse inequality is the elementary observation from Pflueger--Solomon Lemma lem:Fg1k: affine periodicity applied to the transmission permutation of the zero divisor gives a rank-one divisor k u.

theorem Bananas.normalizeFirstInversion_injective_on_crossing_of_deep_empty {k : ℕ} {tau : ℤ → ℤ} (hk : 0 < k) (hAffine : IsKAffine k tau) (hDeep : southeastSet tau (1 - ↑k) 0 = ∅) : Set.InjOn (normalizeFirstInversion k) (crossingInversions tau)

If the deeper southeast quadrant is empty, normalization is injective on the rectangle of inversions crossing the origin. The point is that a collision would put two southeast dots in the same residue class; translating the lower one by affine periodicity would then put a dot in the forbidden deeper quadrant.

theorem Bananas.crossingInversions_ncard_le_kInversionCount_of_degree_lt_period {M : TwiceMarked} {D : CFDiv M.graph} {d : ℤ} {k : ℕ} (hk : 0 < k) (hconn : _root_.graphConnected M.graph) (hdeg : CFDiv.degree D = d) (hdk : d < ↑k) {tau : ℤ → ℤ} (hTau : IsTransmissionPermutation M D tau) (hAffine : IsKAffine k tau) : (crossingInversions tau).ncard ≤ kInversionCount k tau

A rank-positive divisor of degree below the affine period forces its full Brill--Noether rectangle to inject into the k-inversions.

theorem Bananas.KGeneralTransmission.rank_period_smul_one_chip_ge_one {M : TwiceMarked} {k : ℕ} (hK : KGeneralTransmission M k) (hconn : _root_.graphConnected M.graph) : rank M.graph (↑k • oneChip M.u) ≥ 1

Pflueger--Solomon Lemma lem:Fg1k, rank half: k-general transmission supplies the degree-k pencil k u.

theorem Bananas.KGeneralTransmission.no_rank_one_below_period {M : TwiceMarked} {g k : ℕ} (hconn : _root_.graphConnected M.graph) (hgenus : M.graph.genus = ↑g) (hK : KGeneralTransmission M k) (hsmall : k ≤ (g + 3) / 2) {D : CFDiv M.graph} {d : ℤ} (hdeg : CFDiv.degree D = d) (hrank : rank M.graph D ≥ 1) (hdk : d < ↑k) : False

A k-general twice-marked graph has no positive-rank divisor of degree below k, provided k is no larger than the generic gonality floor((g+3)/2).

theorem Bananas.KGeneralTransmission.exact_gonality {M : TwiceMarked} {g k : ℕ} (hconn : _root_.graphConnected M.graph) (hgenus : M.graph.genus = ↑g) (hK : KGeneralTransmission M k) (hsmall : k ≤ (g + 3) / 2) : Utilities.BNExists M.graph 1 ↑k ∧ ∀ d < ↑k, ¬Utilities.BNExists M.graph 1 d

Exact witness-form gonality for a k-general twice-marked graph in the special range.