Once-marked Brill--Noether existence

This file records both the degree-free all-row rank-test definition of the Pflueger--Solomon divisor census and its normalized finite form, together with the exact graph-side interface with Grassmannian transmission. A normalized census witness has degree genus G. If the rows of lambda are lambda_i, the required finite inequalities are

rank (D + (i - lambda_i) u) >= i.

The auxiliary second mark in transmission disappears because every one of these rows lies on the cut b = 0.

theorem Utilities.youngDiagram_rowLens_sum_eq_card (lambda : YoungDiagram) : lambda.rowLens.sum = lambda.card

The sum of the row lengths is the cardinality (number of boxes) of a Young diagram.

theorem Utilities.youngDiagram_transpose_card (lambda : YoungDiagram) : lambda.transpose.card = lambda.card

Transposition preserves the number of boxes.

def Utilities.onceMarkedCorners (lambda : YoungDiagram) : List Corner

The finite pointed rank rows encoded by a Young diagram. We deliberately retain every positive row. Passing to the last row of each constant block is an optional certificate compression, not part of the semantic definition.

Equations

• Utilities.onceMarkedCorners lambda = List.map (fun (p : ℕ × ℕ) => (↑p.2 - ↑p.1, 0, ↑p.2)) lambda.rowLens.zipIdx

def Utilities.onceMarkedPart (lambda : YoungDiagram) (i : ℕ) : ℕ

The ith part of a Young diagram, extended by zero beyond its positive row list.

Equations

• Utilities.onceMarkedPart lambda i = lambda.rowLens.getD i 0

def Utilities.OnceMarkedCensusContains (G : CFGraph) (u : G.V) (lambda : YoungDiagram) : Prop

The degree-free, all-row rank-test formulation of membership in the Pflueger--Solomon divisor census. It is the pole-order inequality lambda_i(D,u) ≥ lambda_i, written without choosing minima:

rank (D + (i + g - deg D - lambda_i)u) ≥ i for every i ≥ 0.

For a connected graph this is equivalent to the finite normalized predicate OnceMarkedBNExists below.

Equations

• Utilities.OnceMarkedCensusContains G u lambda = ∃ (D : CFDiv G), ∀ (i : ℕ), rank G (D + (↑i + G.genus - CFDiv.degree D - ↑(Utilities.onceMarkedPart lambda i)) • oneChip u) ≥ ↑i

def Utilities.OnceMarkedBNExists (G : CFGraph) (u : G.V) (lambda : YoungDiagram) : Prop

The normalized form of membership of lambda in the divisor census of the once-marked graph (G,u).

Equations

• Utilities.OnceMarkedBNExists G u lambda = ∃ (D : CFDiv G), CFDiv.degree D = G.genus ∧ ∀ c ∈ Utilities.onceMarkedCorners lambda, rank G (D + c.1 • oneChip u) ≥ c.2.2

def Utilities.OnceMarkedBNExistence (G : CFGraph) (u : G.V) : Prop

Once-marked Brill--Noether existence for (G,u): every Young diagram of size at most the genus occurs in its divisor census.

Equations

• Utilities.OnceMarkedBNExistence G u = ∀ (lambda : YoungDiagram), ↑lambda.card ≤ G.genus → Utilities.OnceMarkedBNExists G u lambda

def Utilities.OnceMarkedBNConjecture : Prop

The once-marked Brill--Noether existence conjecture for finite connected graphs.

Equations

• Utilities.OnceMarkedBNConjecture = ∀ (G : CFGraph), graphConnected G → ∀ (u : G.V), Utilities.OnceMarkedBNExistence G u

theorem Utilities.onceMarkedBNExists_iff_rank_rows (G : CFGraph) (u : G.V) (lambda : YoungDiagram) : OnceMarkedBNExists G u lambda ↔ ∃ (D : CFDiv G), CFDiv.degree D = G.genus ∧ ∀ (i : ℕ) (hi : i < lambda.rowLens.length), rank G (D + (↑i - ↑lambda.rowLens[i]) • oneChip u) ≥ ↑i

Row-indexed form of OnceMarkedBNExists. This is convenient both for handwritten shape arguments and for generated finite catalogs.

Marked Riemann--Roch duality

theorem Utilities.onceMarkedBNExists_iff_rank_cells (G : CFGraph) (u : G.V) (lambda : YoungDiagram) : OnceMarkedBNExists G u lambda ↔ ∃ (D : CFDiv G), CFDiv.degree D = G.genus ∧ ∀ (i j : ℕ), (i, j) ∈ lambda → rank G (D + (↑i - ↑j - 1) • oneChip u) ≥ ↑i

Cellwise form of the pointed partition rank conditions. A cell (i,j) asks for rank at least i after twisting by (i-j-1)u. This symmetric form is the convenient interface for transposing a partition.

def Utilities.onceMarkedDualDivisor (G : CFGraph) (u : G.V) (D : CFDiv G) : CFDiv G

The degree-g representative of the marked Riemann--Roch dual of D. The extra 2u normalizes the degree; twisting a divisor at the marked point does not change its Weierstrass partition.

Equations

• Utilities.onceMarkedDualDivisor G u D = canonicalDivisor G - D + 2 • oneChip u

@[simp]

theorem Utilities.deg_onceMarkedDualDivisor {G : CFGraph} (u : G.V) (D : CFDiv G) (hDegree : CFDiv.degree D = G.genus) : CFDiv.degree (onceMarkedDualDivisor G u D) = G.genus

theorem Utilities.rank_onceMarkedDualDivisor_add_zsmul {G : CFGraph} (hG : graphConnected G) (u : G.V) (D : CFDiv G) (hDegree : CFDiv.degree D = G.genus) (ell : ℤ) : rank G (onceMarkedDualDivisor G u D + ell • oneChip u) = rank G (D - (ell + 2) • oneChip u) + ell + 1

Exact marked Riemann--Roch identity for a normalized divisor.

theorem Utilities.onceMarkedBNExists_transpose {G : CFGraph} (hG : graphConnected G) (u : G.V) (lambda : YoungDiagram) : OnceMarkedBNExists G u lambda → OnceMarkedBNExists G u lambda.transpose

A normalized witness for lambda dualizes to a normalized witness for the transposed Young diagram.

theorem Utilities.onceMarkedBNExists_transpose_iff {G : CFGraph} (hG : graphConnected G) (u : G.V) (lambda : YoungDiagram) : OnceMarkedBNExists G u lambda ↔ OnceMarkedBNExists G u lambda.transpose

Once-marked Brill--Noether existence is invariant under transposing the partition.

theorem Utilities.onceMarkedCensusContains_iff_onceMarkedBNExists {G : CFGraph} (hG : graphConnected G) (u : G.V) (lambda : YoungDiagram) : OnceMarkedCensusContains G u lambda ↔ OnceMarkedBNExists G u lambda

On a connected graph, degree normalization and the Riemann tail identify the original all-row census test with the finite positive-row test.

def Utilities.GrassmannianPartitionProfile (tau : AspPerm) (lambda : YoungDiagram) : Prop

The exact finite corner data needed for an ASP permutation to encode the once-marked partition lambda at the cut b = 0.

For the Grassmannian permutation attached to lambda, these facts follow from its essential-set formula. Packaging them separately keeps the graph side independent of the particular construction of that permutation.

Equations

• One or more equations did not get rendered due to their size.

theorem Utilities.transmissionExists_iff_onceMarkedBNExists {G : CFGraph} (hG : graphConnected G) (u v : G.V) (tau : AspPerm) (lambda : YoungDiagram) (hProfile : GrassmannianPartitionProfile tau lambda) : TransmissionExists G u v tau ↔ OnceMarkedBNExists G u lambda

A Grassmannian partition profile makes its twice-marked transmission existence condition exactly the once-marked divisor-census condition. In particular, the result is independent of the auxiliary second mark.