Highlights of the chain-of-loops application

A public interface, in one file. Every main theorem of Bananas/ChainOfLoops/ is restated below as an example whose type is written out in full and whose proof is the real theorem. There is not a single new definition or theorem here.

This file plays for Bananas/ChainOfLoops/ the role TwiceMarkedBananas.lean plays for the rest of Bananas. The two are deliberately separate: TwiceMarkedBananas.lean is a paper-order index of the twice-marked banana paper, and Cools–Draisma–Payne–Robeva is not a result of that paper — it is a downstream consumer of its Section 6 chain theorems. Folding these statements into the paper index would break the one invariant that index has.

• For a reader. The complete statement of Cools–Draisma–Payne–Robeva's main theorem, as formalized, is visible here in one screen.
• For the build. Each example is checked by the kernel against the real declaration, so a change to a statement is detected in this file.

These files formalize the discrete form of CDPR Theorem 1.1 (arXiv:1001.2774): a generic chain of loops is Brill–Noether general. Part (1) is the nonexistence statement cdpr_nonexistence; part (2) is the sharper once-marked form cdpr_no_high_multiplicity, which says no divisor of the expected degree and rank contains (r + ρ + 1) copies of the chain's end vertex.

The key definitions

def ChainOfLoops.Highlights.Loop : Type

A loop of the chain: two positive arc lengths top and bot, CDPR's ℓ_i and m_i. The positivity proofs are bundled into the structure so a List Loop can be List.mapped and List.take/List.droped without List.pmap. (Bananas/ChainOfLoops/CDPR.lean)

Equations

• ChainOfLoops.Highlights.Loop = ChainOfLoops.Loop

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

The torsion order of a loop: (ℓ + m) / gcd(ℓ, m), the order of the class of v_i - v_{i-1} in the Jacobian of that cycle. (Bananas/ChainOfLoops/CDPR.lean)

Equations

• ChainOfLoops.Highlights.torsionOrder = ChainOfLoops.Loop.torsionOrder

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

The chain of loops as a CFGraph: g cycles glued in a row. (Bananas/ChainOfLoops/CDPR.lean)

Equations

• ChainOfLoops.Highlights.chainGraph = ChainOfLoops.chainGraph

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

The chain as a marked graph, whose .left and .right are CDPR's v_0 and v_g. (Bananas/ChainOfLoops/CDPR.lean)

Equations

• ChainOfLoops.Highlights.chainMarked = ChainOfLoops.chainMarked

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

CDPR Definition 4.1, literally: no ratio ℓ_i / m_i equals the ratio of two positive integers whose sum is at most 2g - 2. Cross-multiplied to avoid a division convention. (Bananas/ChainOfLoops/CDPR.lean)

Equations

• ChainOfLoops.Highlights.CDPRGeneric = ChainOfLoops.CDPRGeneric

The genus and the Brill–Noether number

The main theorem

The once-marked form

The sharper statement, and the one that carries the real content: when ρ ≥ 0, no divisor of degree d and rank at least r contains (r + ρ + 1) copies of a marked end vertex.

The orientation is not optional. The theorem holds at the right mark v_g under the prefix torsion budget and at the left mark v_0 under the suffix budget; testing at v_0 under the prefix budget is false.