Cools--Draisma--Payne--Robeva nonexistence for a chain of loops

(Cools--Draisma--Payne--Robeva, A tropical proof of the Brill--Noether theorem, arXiv:1001.2774).

CDPR Theorem 1.1 (thm:Main) states that a generic chain of loops has no effective divisor in the negative Brill--Noether range, and in the nonnegative range has no such divisor containing the specified multiple of the left endpoint.

CDPR Definition 4.1 (defn:Generic) excludes arc-length ratios represented by two positive integers whose sum is at most 2g - 2.

What is formalized here, and what is not

CDPR work with metric graphs: ℓ_i and m_i are arbitrary positive reals and divisors are ℤ-combinations of arbitrary points of Γ. This file proves the discrete (Baker--Norine) statement, for a chain of cycles with arbitrary positive integer arc lengths, which is the theory the Bananas library speaks. The relationship is:

• the metric theorem implies the discrete one, so this is a priori weaker for any single graph;
• genericity is invariant under subdivision ((ℓ,m) ↦ (nℓ,nm) leaves (ℓ+m)/gcd(ℓ,m) fixed), so the discrete statement quantified over all integer length vectors covers every subdivision of every rational chain of loops -- and CDPR's own suggested instance ℓ_i = 2g-2, m_i = 1 is one of them;
• closing the remaining gap needs rank-invariance under subdivision (Hladky--Kral--Norine / Luo), which this repository does not have.

CDPR's loops are glued directly at the vertices v_i; there are no bridges. That is exactly Utilities.MarkedGraph.chain.

The route

Part (1) is a pure instantiation of theorems already proved in Bananas/:

• Bananas.cycle_kGeneralTransmission (Pflueger--Solomon Example 1.11): a cycle with arcs of lengths a and b, marked at its two junction vertices, has k-general transmission at k = (a+b)/gcd(a,b);
• Bananas.brillNoetherGeneral_mixedTorsionChain_of_minBudget (Pflueger--Solomon Theorem 1.13(2) = Corollary 6.16(2)).

Bananas/Examples/ExampleBngChain.lean is the worked five-factor instance of the same assembly.

Part (2) adds one genuinely new lemma, finitePointedDiagram_card_ge_of_vanishing: the bridge from the repository's Young-diagram formulation of once-marked Brill--Noether generality (Bananas.OnceMarkedBrillNoetherGeneral) to CDPR's "no divisor contains m v" phrasing. It consumes Bananas.onceMarkedBrillNoetherGeneral_mixedTorsionChain (Theorem 1.13(1) = Corollary 6.16(1)) at the chain's right mark, and its reversed counterpart at the left.

Endpoint orientation is load-bearing. The marked chain theorem concludes at the chain's right mark under the prefix budget k_i > g_1 + ... + g_i; CDPR state part (2) at v_0, the left end, which needs the suffix budget k_i > g_i + ... + g_l instead. Under CDPR genericity both hold, so the distinction costs nothing here -- but it is not cosmetic: a numeric screen run at v_0 under the prefix budget reports immediate counterexamples at g = 2 (ℓ_1 = m_1, torsion order two, so 2 v_0 has rank one).

Loops

structure ChainOfLoops.Loop : Type

One loop of a chain of loops: a cycle subdivided into a top arc of length top and a bottom arc of length bot, both positive. These are CDPR's ℓ_i and m_i.

The positivity hypotheses are bundled into the structure on purpose: a List Loop can then be List.mapped, and List.take/List.drop lemmas apply, where a List (ℕ × ℕ) with side conditions would force List.pmap throughout the ChainMinBudget arithmetic.

• top : ℕ

  The positive number of edges in the upper strand of the loop.

• bot : ℕ

  The positive number of edges in the lower strand of the loop.

• top_pos : 0 < self.top
• bot_pos : 0 < self.bot

noncomputable def ChainOfLoops.Loop.banana (P : Loop) : Bananas.Banana 1

The loop as a genus-one banana, i.e. a cycle: two parallel strands of lengths top and bot between the two junction vertices.

Equations

• P.banana = Bananas.bananaOfLengths 1 ![P.top, P.bot] ⋯

@[simp]

theorem ChainOfLoops.Loop.banana_length_zero (P : Loop) : P.banana.length 0 = P.top

@[simp]

theorem ChainOfLoops.Loop.banana_length_one (P : Loop) : P.banana.length 1 = P.bot

def ChainOfLoops.Loop.torsionOrder (P : Loop) : ℕ

The torsion order of (loop, v_{i-1}, v_i): the order of the class of v_i - v_{i-1} in the Jacobian of the cycle, which is (ℓ+m)/gcd(ℓ,m) (Bananas.cycle_isTorsionOrder, Pflueger--Solomon Example 1.11).

Equations

• P.torsionOrder = (P.top + P.bot) / P.top.gcd P.bot

The reduced pair (ℓ/d, m/d)

The arithmetic behind cdprGeneric_iff: writing d = gcd(ℓ,m), the pair (ℓ/d, m/d) is the least positive solution of ℓ q = m p, and its coordinate sum is exactly torsionOrder.

theorem ChainOfLoops.Loop.gcd_pos (P : Loop) : 0 < P.top.gcd P.bot

theorem ChainOfLoops.Loop.gcd_mul_top_div (P : Loop) : P.top.gcd P.bot * (P.top / P.top.gcd P.bot) = P.top

theorem ChainOfLoops.Loop.gcd_mul_bot_div (P : Loop) : P.top.gcd P.bot * (P.bot / P.top.gcd P.bot) = P.bot

theorem ChainOfLoops.Loop.top_div_gcd_pos (P : Loop) : 0 < P.top / P.top.gcd P.bot

theorem ChainOfLoops.Loop.bot_div_gcd_pos (P : Loop) : 0 < P.bot / P.top.gcd P.bot

theorem ChainOfLoops.Loop.coprime_div_gcd (P : Loop) : (P.top / P.top.gcd P.bot).Coprime (P.bot / P.top.gcd P.bot)

theorem ChainOfLoops.Loop.torsionOrder_eq (P : Loop) : P.torsionOrder = P.top / P.top.gcd P.bot + P.bot / P.top.gcd P.bot

(ℓ + m)/d = ℓ/d + m/d.

theorem ChainOfLoops.Loop.torsionOrder_pos (P : Loop) : 0 < P.torsionOrder

theorem ChainOfLoops.Loop.top_mul_bot_div_gcd (P : Loop) : P.top * (P.bot / P.top.gcd P.bot) = P.bot * (P.top / P.top.gcd P.bot)

The reduced pair is itself a solution of ℓ q = m p.

theorem ChainOfLoops.Loop.reduced_mul_eq_mul (P : Loop) {p q : ℕ} (heq : P.top * q = P.bot * p) : P.top / P.top.gcd P.bot * q = P.bot / P.top.gcd P.bot * p

Any solution of ℓ q = m p reduces: (ℓ/d) q = (m/d) p.

noncomputable def ChainOfLoops.Loop.factor (P : Loop) : Bananas.KGeneralChainFactor

The loop packaged as a chain factor, carrying its k-general transmission at k = torsionOrder.

Equations

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

@[simp]

theorem ChainOfLoops.Loop.factor_period (P : Loop) : P.factor.period = P.torsionOrder

@[simp]

theorem ChainOfLoops.Loop.factor_marked_graph (P : Loop) : P.factor.marked.graph = Utilities.Certificate.SubdivisionGraph.Spec.graph P.banana

theorem ChainOfLoops.Loop.genus_factor (P : Loop) : P.factor.marked.graph.genus = 1

Every loop has genus one.

The chain

noncomputable def ChainOfLoops.chainMarked (P : Loop) (L : List Loop) : Utilities.MarkedGraph

The chain of loops with first loop P and remaining loops L, as a twice-marked graph: left is CDPR's v_0 and right is v_g.

g = L.length + 1. The head/tail shape, and the doubly mapped factor list, match Utilities.MarkedGraph.chain and every chain theorem in Bananas/ on the nose: List.map_map is not a definitional equality, so writing the list as (L.map Loop.factor).map KGeneralChainFactor.marked rather than the fused L.map (·.factor.marked) is what lets the bananas conclusions and the reversal isomorphism apply without any list transport.

Equations

• ChainOfLoops.chainMarked P L = P.factor.marked.chain (List.map Bananas.KGeneralChainFactor.marked (List.map ChainOfLoops.Loop.factor L))

noncomputable def ChainOfLoops.chainGraph (P : Loop) (L : List Loop) : CFGraph

The underlying graph of a chain of loops.

Equations

• ChainOfLoops.chainGraph P L = (ChainOfLoops.chainMarked P L).graph

theorem ChainOfLoops.graph_connected_chainGraph (P : Loop) (L : List Loop) : graphConnected (chainGraph P L)

A chain of loops is connected.

theorem ChainOfLoops.genus_markedChain_map (M : Utilities.MarkedGraph) (Ls : List Bananas.KGeneralChainFactor) : (M.chain (List.map Bananas.KGeneralChainFactor.marked Ls)).graph.genus = M.graph.genus + Bananas.chainFactorGenus Ls

The genus of a chain of factors is the head genus plus the factor genus sum.

@[simp]

theorem ChainOfLoops.chainFactorGenus_map (L : List Loop) : Bananas.chainFactorGenus (List.map Loop.factor L) = ↑L.length

chainFactorGenus of a mapped loop list is its length: every factor has genus one.

theorem ChainOfLoops.genus_chainGraph (P : Loop) (L : List Loop) : (chainGraph P L).genus = ↑L.length + 1

The genus of a chain of g loops is g.

Genericity

def ChainOfLoops.CDPRGeneric (L : List Loop) : Prop

CDPR Definition 4.1, literally: none of the ratios ℓ_i / m_i equals the ratio of two positive integers whose sum is at most 2g - 2.

Cross multiplication avoids a division convention, exactly as in Bananas.EvenlyMarkedTheta.

Equations

• ChainOfLoops.CDPRGeneric L = ∀ P ∈ L, ∀ (p q : ℕ), 0 < p → 0 < q → p + q ≤ 2 * L.length - 2 → P.top * q ≠ P.bot * p

theorem ChainOfLoops.cdprGeneric_iff (L : List Loop) : CDPRGeneric L ↔ ∀ P ∈ L, 2 * L.length - 2 < P.torsionOrder

CDPR genericity is exactly a lower bound on the torsion orders.

Writing d = gcd(ℓ,m), every positive solution of ℓ q = m p is (p,q) = t · (ℓ/d, m/d), so the least attainable p + q is (ℓ+m)/d = torsionOrder.

The budget inequalities

theorem ChainOfLoops.factor_get_period (L : List Loop) (i : ℕ) (hi : i < (List.map Loop.factor L).length) (hi' : i < L.length) : ((List.map Loop.factor L).get ⟨i, hi⟩).period = (L.get ⟨i, hi'⟩).torsionOrder

The period of the i-th mapped chain factor is the i-th torsion order.

theorem ChainOfLoops.chainMinBudget_of_torsion (P : Loop) (L : List Loop) (h : ∀ (i : ℕ) (hi : i < (P :: L).length), min (↑i + 1) (↑(P :: L).length - ↑i) < ↑((P :: L).get ⟨i, hi⟩).torsionOrder) : Bananas.ChainMinBudget (List.map Loop.factor (P :: L))

The ChainMinBudget hypothesis of Corollary 6.16(2), specialised to genus-one factors: min(i+1, g-i) < k_i.

theorem ChainOfLoops.chainPrefixBudget_of_torsion (P : Loop) (L : List Loop) (h : ∀ (i : ℕ) (hi : i < (P :: L).length), ↑i + 1 < ↑((P :: L).get ⟨i, hi⟩).torsionOrder) : Bananas.ChainPrefixBudget P.factor.marked.graph.genus (List.map Loop.factor L)

The ChainPrefixBudget hypothesis of Corollary 6.16(1), specialised to genus-one factors: i + 1 < k_i.

theorem ChainOfLoops.chainSuffixBudget_of_torsion (P : Loop) (L : List Loop) (h : ∀ (i : ℕ) (hi : i < (P :: L).length), ↑(P :: L).length - ↑i < ↑((P :: L).get ⟨i, hi⟩).torsionOrder) : Bananas.ChainSuffixBudget (List.map Loop.factor (P :: L))

The ChainSuffixBudget hypothesis of the reversed chain theorem, specialised to genus-one factors: g - i < k_i. This is the budget that puts CDPR's own mark v_0 at the general end.

theorem ChainOfLoops.torsion_bounds_of_cdprGeneric (P : Loop) (L : List Loop) (hg : 2 ≤ L.length + 1) (hGeneric : CDPRGeneric (P :: L)) : (∀ (i : ℕ) (hi : i < (P :: L).length), min (↑i + 1) (↑(P :: L).length - ↑i) < ↑((P :: L).get ⟨i, hi⟩).torsionOrder) ∧ ∀ (i : ℕ) (hi : i < (P :: L).length), ↑i + 1 < ↑((P :: L).get ⟨i, hi⟩).torsionOrder

CDPR genericity implies both budgets: 2g - 2 ≥ g > min(i+1, g-i) and 2g - 2 ≥ g > i + 1 for g ≥ 2.

theorem ChainOfLoops.torsion_suffix_bound_of_cdprGeneric (P : Loop) (L : List Loop) (hg : 2 ≤ L.length + 1) (hGeneric : CDPRGeneric (P :: L)) (i : ℕ) (hi : i < (P :: L).length) : ↑(P :: L).length - ↑i < ↑((P :: L).get ⟨i, hi⟩).torsionOrder

CDPR genericity also implies the suffix budget g - i < k_i, which is what puts the left mark v_0 at the general end.

CDPR Theorem 1.1

theorem ChainOfLoops.brillNoetherGeneral_chainOfLoops (P : Loop) (L : List Loop) (hBudget : ∀ (i : ℕ) (hi : i < (P :: L).length), min (↑i + 1) (↑(P :: L).length - ↑i) < ↑((P :: L).get ⟨i, hi⟩).torsionOrder) : Bananas.BrillNoetherGeneral (chainGraph P L)

The sharp unmarked statement actually proved: a chain of loops whose torsion orders satisfy the Corollary 6.16(2) budget is Brill--Noether general. Only min(i+1, g-i) < k_i is required, which is far weaker than CDPR's genericity.

theorem ChainOfLoops.cdpr_nonexistence (P : Loop) (L : List Loop) (hg : 2 ≤ L.length + 1) (hGeneric : CDPRGeneric (P :: L)) (r d : ℤ) (hr : 0 ≤ r) (hrho : Utilities.bnNumber (chainGraph P L) r d < 0) : ¬Utilities.BNExists (chainGraph P L) r d

CDPR Theorem 1.1(1), discrete form. A chain of g loops with generic positive integer arc lengths carries no divisor of degree d and rank at least r when the Brill--Noether number is negative.

theorem ChainOfLoops.bnNumber_chainGraph (P : Loop) (L : List Loop) (r d : ℤ) : Utilities.bnNumber (chainGraph P L) r d = ↑L.length + 1 - (r + 1) * (↑L.length + 1 - d + r)

CDPR's Brill--Noether number ρ(g,r,d) = g - (r+1)(g-d+r) for a chain of g loops, written out. Bridges bnNumber to the paper's ρ.

theorem ChainOfLoops.onceMarkedBrillNoetherGeneral_chainOfLoops (P : Loop) (L : List Loop) (hBudget : ∀ (i : ℕ) (hi : i < (P :: L).length), ↑i + 1 < ↑((P :: L).get ⟨i, hi⟩).torsionOrder) : Bananas.OnceMarkedBrillNoetherGeneral (chainGraph P L) (chainMarked P L).right

The sharp once-marked statement: a chain of loops whose torsion orders satisfy the Corollary 6.16(1) prefix budget i + 1 < k_i is once-marked Brill--Noether general at its right-hand mark v_g.

The pointed counting lemma

The bridge from the repository's Young-diagram formulation of once-marked Brill--Noether generality to CDPR's "no divisor contains m v" phrasing. This is the one piece of new mathematics in the campaign; it is the summation of Bananas/Wedge/OnceMarkedWedgeGenerality.lean:340-398 with the i = 0 row strengthened by the extra vanishing hypothesis.

theorem ChainOfLoops.finitePointedDiagram_card_ge_of_vanishing (G : CFGraph) (hG : graphConnected G) (D : CFDiv G) (v : G.V) (r : ℕ) (m : ℤ) (hrank : ↑r ≤ rank G D) (hm : 0 ≤ rank G (D - m • oneChip v)) : (↑r + 1) * (G.genus - CFDiv.degree D + ↑r) + (m - ↑r) ≤ ↑(Bananas.finitePointedDiagram G hG D v r).card

L8. If D has rank at least r and D - m v is still effective in the sense of having nonnegative rank, then the first r + 1 rows of the Weierstrass diagram of (D, v) already contain (r+1)(g - deg D + r) + (m - r) cells.

The r + 1 rows are bounded below by the Brill--Noether rectangle width g - deg D + r, exactly as in Proposition 6.14; the extra m - r comes from the zeroth row, whose threshold is pushed down to -m by the vanishing hypothesis.

theorem ChainOfLoops.rank_sub_high_multiplicity_neg (G : CFGraph) (hG : graphConnected G) (v : G.V) (hOM : Bananas.OnceMarkedBrillNoetherGeneral G v) (D : CFDiv G) (r : ℤ) (hr : 0 ≤ r) (hrank : r ≤ rank G D) : rank G (D - (r + Utilities.bnNumber G r (CFDiv.degree D) + 1) • oneChip v) < 0

The counting lemma, packaged for use: on a once-marked Brill--Noether general pointed graph, no divisor of rank at least r vanishes to order r + ρ + 1 at the mark.

This is the graph-theoretic content of CDPR Theorem 1.1(2); the chain of loops enters only through hOM.

theorem ChainOfLoops.rank_sub_high_multiplicity_neg_of_iso {G : CFGraph} {H : CFGraph} (phi : Utilities.CFGraphIso G H) (hG : graphConnected G) (v : G.V) (hOM : Bananas.OnceMarkedBrillNoetherGeneral H (phi.vertexEquiv v)) (D : CFDiv G) (r : ℤ) (hr : 0 ≤ r) (hrank : r ≤ rank G D) : rank G (D - (r + Utilities.bnNumber G r (CFDiv.degree D) + 1) • oneChip v) < 0

The same, transported along a graph isomorphism: it is enough for the image of the mark to be once-marked Brill--Noether general.

theorem ChainOfLoops.cdpr_no_high_multiplicity (P : Loop) (L : List Loop) (hg : 2 ≤ L.length + 1) (hGeneric : CDPRGeneric (P :: L)) (D : CFDiv (chainGraph P L)) (r d : ℤ) (hr : 0 ≤ r) : r < (chainGraph P L).genus → ∀ (hdeg : CFDiv.degree D = d) (hrank : rank (chainGraph P L) D ≥ r) (hrho : 0 ≤ Utilities.bnNumber (chainGraph P L) r d), rank (chainGraph P L) (D - (r + Utilities.bnNumber (chainGraph P L) r d + 1) • oneChip (chainMarked P L).right) < 0

CDPR Theorem 1.1(2), discrete form, at the chain's right-hand mark v_g. When ρ ≥ 0 no divisor of degree d and rank at least r contains (r + ρ + 1) v_g.

CDPR state this at v_0; see cdpr_no_high_multiplicity_left.

hrbound is CDPR's own standing range restriction (Notation 4.2, via d ≤ 2g - 2 and Clifford) and is kept in the statement for faithfulness; the row estimate of finitePointedDiagram_card_ge_of_vanishing turned out not to need it, since the r + 1 rows it sums exist for every r.

theorem ChainOfLoops.onceMarkedBrillNoetherGeneral_chainOfLoops_left (P : Loop) (L : List Loop) (hBudget : ∀ (i : ℕ) (hi : i < (P :: L).length), ↑(P :: L).length - ↑i < ↑((P :: L).get ⟨i, hi⟩).torsionOrder) : Bananas.OnceMarkedBrillNoetherGeneral (Bananas.reversedMarkedChain P.factor (List.map Loop.factor L)).graph ((Bananas.reversedFactorChainIso P.factor (List.map Loop.factor L)).vertexEquiv (chainMarked P L).left)

Once-marked Brill--Noether generality at the chain's left mark v_0, obtained from the suffix budget through the reversed presentation of the chain and its isomorphism to the canonical one.

Stated as membership of v_0's image under reversedFactorChainIso, which is the form rank_sub_high_multiplicity_neg_of_iso consumes.

theorem ChainOfLoops.cdpr_no_high_multiplicity_left (P : Loop) (L : List Loop) (hg : 2 ≤ L.length + 1) (hGeneric : CDPRGeneric (P :: L)) (D : CFDiv (chainGraph P L)) (r d : ℤ) (hr : 0 ≤ r) : r < (chainGraph P L).genus → ∀ (hdeg : CFDiv.degree D = d) (hrank : rank (chainGraph P L) D ≥ r) (hrho : 0 ≤ Utilities.bnNumber (chainGraph P L) r d), rank (chainGraph P L) (D - (r + Utilities.bnNumber (chainGraph P L) r d + 1) • oneChip (chainMarked P L).left) < 0

CDPR Theorem 1.1(2) at v_0, CDPR's own marked point.

The marked chain theorem concludes at the chain's right mark under the prefix budget; CDPR state part (2) at the left end. The transport is through the reversed (outside-in) presentation Bananas.reversedMarkedChain, which is once-marked general at its right mark under the suffix budget g - i < k_i, and whose isomorphism Bananas.reversedFactorChainIso to the canonical chain carries v_0 to that mark. Under CDPR genericity both budgets hold, so the orientation costs nothing -- but it is not optional: testing at v_0 under the prefix budget is false (blueprint section 6.4).