Ordinary Brill--Noether witnesses from transmission rows

A transmission witness contains many ordinary rank witnesses: fixing one row (a,b) gives a divisor of degree g + χτ + a - b whose rank is at least τ.s (a+1) b - 1. Any smaller target rank therefore yields BNExists.

This is the generic core needed later for the Grassmannian-transmission ⇒ W^r_d implication.

def Utilities.TransmissionTwist (G : CFGraph) (u v : G.V) (D : CFDiv G) (a b : ℤ) : CFDiv G

The marked twist attached to one transmission row.

Equations

• Utilities.TransmissionTwist G u v D a b = D + a • oneChip u - b • oneChip v

theorem Utilities.degree_transmissionTwist {G : CFGraph} {u v : G.V} {τ : AspPerm} {D : CFDiv G} (h : SatisfiesTransmission G u v τ D) (a b : ℤ) : CFDiv.degree (TransmissionTwist G u v D a b) = G.genus + τ.χ + a - b

Exact degree of a transmission-row twist.

theorem Utilities.rank_transmissionTwist {G : CFGraph} {u v : G.V} {τ : AspPerm} {D : CFDiv G} (h : SatisfiesTransmission G u v τ D) (a b : ℤ) : rank G (TransmissionTwist G u v D a b) ≥ τ.s.func (a + 1) b - 1

Exact rank lower bound supplied by one transmission row.

theorem Utilities.BNExists_of_transmission_row {G : CFGraph} {u v : G.V} {τ : AspPerm} {D : CFDiv G} (h : SatisfiesTransmission G u v τ D) (a b r : ℤ) (hTarget : r ≤ τ.s.func (a + 1) b - 1) : BNExists G r (G.genus + τ.χ + a - b)

Any target rank below the row threshold gives an ordinary BN witness at the affine row degree.

theorem Utilities.BNExists_at_transmission_threshold {G : CFGraph} {u v : G.V} {τ : AspPerm} {D : CFDiv G} (h : SatisfiesTransmission G u v τ D) (a b : ℤ) : BNExists G (τ.s.func (a + 1) b - 1) (G.genus + τ.χ + a - b)

At the exact row threshold, transmission directly supplies a BN witness.

theorem Utilities.BNExists_of_transmissionExists_row {G : CFGraph} {u v : G.V} {τ : AspPerm} (h : TransmissionExists G u v τ) (a b r : ℤ) (hTarget : r ≤ τ.s.func (a + 1) b - 1) : BNExists G r (G.genus + τ.χ + a - b)

Existence-level version: a transmission locus witness yields every ordinary BN witness forced by any one of its rows.