Certifying transmission from finitely many rank corners

The transmission condition for an ASP permutation τ is indexed by the whole lattice ℤ × ℤ. Two general facts collapse it to a finite check.

• Riemann. Every divisor satisfies rank G E ≥ deg E - genus G, so a transmission row whose threshold is at most τ.χ + a - b costs nothing.
• Chip transport. A single rank bound at one lattice point (a₀, b₀) propagates to every other point, losing one unit for each chip that has to be removed: rank (D + a•u - b•v) ≥ r₀ - max 0 (a₀ - a) - max 0 (b - b₀).

Consequently a divisor satisfies the full transmission condition as soon as it achieves finitely many corner bounds that, together with the Riemann line, dominate the slipface of τ. This is the mechanism behind the classical dictionary: for a Grassmannian τ whose diagram is a rectangle the corner list has a single entry, and transmission becomes an ordinary Brill--Noether condition BNExists G r d; the length of τ is exactly (r+1) * (g - d + r), so ℓ(τ) ≤ g is the Brill--Noether inequality ρ ≥ 0.

Riemann and chip transport

theorem Utilities.rank_ge_deg_sub_genus {G : CFGraph} (hG : graphConnected G) (D : CFDiv G) : rank G D ≥ CFDiv.degree D - G.genus

The Riemann inequality: rank is at least degree minus genus.

theorem Utilities.rank_sub_nsmul_one_chip_ge {G : CFGraph} (D : CFDiv G) (w : G.V) (k : ℕ) : rank G (D - ↑k • oneChip w) ≥ rank G D - ↑k

Removing k chips at one vertex lowers rank by at most k.

theorem Utilities.rank_add_nsmul_one_chip_ge {G : CFGraph} (D : CFDiv G) (w : G.V) (k : ℕ) : rank G (D + ↑k • oneChip w) ≥ rank G D

Adding chips at one vertex never lowers rank.

theorem Utilities.rank_add_zsmul_one_chip_ge {G : CFGraph} (E : CFDiv G) (w : G.V) (p : ℤ) : rank G (E + p • oneChip w) ≥ rank G E - max 0 (-p)

Shifting by an integer multiple of one chip costs at most the number of chips actually removed.

theorem Utilities.rank_transmissionTwist_ge_of_corner {G : CFGraph} (u v : G.V) (D : CFDiv G) {a₀ b₀ r₀ : ℤ} (h : rank G (D + a₀ • oneChip u - b₀ • oneChip v) ≥ r₀) (a b : ℤ) : rank G (D + a • oneChip u - b • oneChip v) ≥ r₀ - max 0 (a₀ - a) - max 0 (b - b₀)

Chip transport. One rank bound at the lattice point (a₀, b₀) propagates to every lattice point.

Corner certificates

@[reducible, inline]

abbrev Utilities.Corner : Type

A corner is a lattice point together with a rank threshold.

Equations

• Utilities.Corner = (ℤ × ℤ × ℤ)

def Utilities.cornerBound (c : Corner) (a b : ℤ) : ℤ

The rank bound that a corner transports to the lattice point (a, b).

Equations

• Utilities.cornerBound c a b = c.2.2 - max 0 (c.1 - a) - max 0 (b - c.2.1)

def Utilities.CornersDominate (τ : AspPerm) (C : List Corner) : Prop

A corner list dominates τ when every transmission threshold is met by one of three things: the trivial bound rank ≥ -1, the Riemann line, or transport from one of the corners.

Equations

• Utilities.CornersDominate τ C = ∀ (a b : ℤ), τ.s.func (a + 1) b - 1 < 0 ∨ τ.s.func (a + 1) b - 1 ≤ τ.χ + a - b ∨ ∃ c ∈ C, τ.s.func (a + 1) b - 1 ≤ Utilities.cornerBound c a b

theorem Utilities.satisfiesTransmission_of_corners {G : CFGraph} (hG : graphConnected G) (u v : G.V) (τ : AspPerm) (D : CFDiv G) (C : List Corner) (hDegree : CFDiv.degree D = G.genus + τ.χ) (hDom : CornersDominate τ C) (hCorners : ∀ c ∈ C, rank G (D + c.1 • oneChip u - c.2.1 • oneChip v) ≥ c.2.2) : SatisfiesTransmission G u v τ D

Corner certificate. A divisor of the right degree that achieves every corner bound satisfies the full transmission condition.

Existence: the Brill--Noether dictionary

theorem Utilities.transmissionExists_of_riemann {G : CFGraph} (hG : graphConnected G) (u v : G.V) (τ : AspPerm) (hDom : ∀ (a b : ℤ), τ.s.func (a + 1) b - 1 ≤ τ.χ + a - b) : TransmissionExists G u v τ

A slipface dominated by the Riemann line alone is realized by every divisor of the correct degree. This covers exactly the ASP permutations of length zero.

theorem Utilities.transmissionExists_of_corner_of_BNExists {G : CFGraph} (hG : graphConnected G) (u v : G.V) (τ : AspPerm) (a₀ b₀ r₀ : ℤ) (hDom : CornersDominate τ [(a₀, b₀, r₀)]) (hBN : BNExists G r₀ (G.genus + τ.χ + a₀ - b₀)) : TransmissionExists G u v τ

One corner is an ordinary Brill--Noether condition. If a single corner (a₀, b₀, r₀) dominates the slipface of τ, then transmission for τ follows from BNExists at rank r₀ and the corresponding affine degree.

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

The converse for a corner that records the true slipface value: transmission returns the Brill--Noether witness. Together with transmissionExists_of_corner_of_BNExists this is an equivalence.

theorem Utilities.transmissionExists_iff_BNExists_of_corner {G : CFGraph} (hG : graphConnected G) (u v : G.V) (τ : AspPerm) (a₀ b₀ r₀ : ℤ) (hDom : CornersDominate τ [(a₀, b₀, r₀)]) (hThreshold : r₀ ≤ τ.s.func (a₀ + 1) b₀ - 1) : TransmissionExists G u v τ ↔ BNExists G r₀ (G.genus + τ.χ + a₀ - b₀)

Dictionary. For a permutation whose slipface has a single dominating corner recording its true value, transmission on a twice-marked graph is equivalent to ordinary Brill--Noether existence, and in particular does not depend on the two marks.

The elementary range

The Brill--Noether input of a single-corner permutation is elementary exactly in the two ranges already available unconditionally: rank zero, and rectangle width at most one. For a single-corner τ the corner rank r₀ and rectangle width w₀ = g - d₀ + r₀ = b₀ - a₀ - τ.χ + r₀ satisfy ℓ(τ) = (r₀ + 1) * w₀, so ℓ(τ) ≤ 3 forces r₀ = 0 or w₀ ≤ 1. The first genuinely new input appears at ℓ(τ) = 4 with r₀ = 1 and w₀ = 2, which is the critical rank-one width-two column W^1_{g-1}.

theorem Utilities.transmissionExists_of_corner_elementary {G : CFGraph} (hG : graphConnected G) (u v : G.V) (τ : AspPerm) (a₀ b₀ r₀ : ℤ) (hDom : CornersDominate τ [(a₀, b₀, r₀)]) (hR : 0 ≤ r₀) (hRho : 0 ≤ bnNumber G r₀ (G.genus + τ.χ + a₀ - b₀)) (hEasy : r₀ = 0 ∨ rectangleWidth G r₀ (G.genus + τ.χ + a₀ - b₀) ≤ 1) : TransmissionExists G u v τ

Transmission in the elementary Brill--Noether range.

theorem Utilities.transmissionExists_of_corner_rank_zero {G : CFGraph} (hG : graphConnected G) (u v : G.V) (τ : AspPerm) (a₀ b₀ : ℤ) (hDom : CornersDominate τ [(a₀, b₀, 0)]) (hDeg : 0 ≤ G.genus + τ.χ + a₀ - b₀) : TransmissionExists G u v τ

Rank-zero corner: the transmission witness is an effective divisor.