The genus-two rank reduction

The first part of the theta analysis is independent of strand coordinates: a negative marked second difference on a genus-two graph with inequivalent marks is necessarily represented in degree two.

theorem Bananas.two_le_degree_of_rankDelta_neg (M : TwiceMarked) (D : CFDiv M.graph) (hDistinct : ¬linearEquiv M.graph (oneChip M.u - oneChip M.v) 0) (hNeg : rankDelta M D < 0) : 2 ≤ CFDiv.degree D

A negative second difference cannot occur in degree at most one when the two marked degree-one classes are distinct.

theorem Bananas.degree_eq_two_of_rankDelta_neg_genus_two (M : TwiceMarked) (D : CFDiv M.graph) (hConn : _root_.graphConnected M.graph) (hGenus : M.graph.genus = 2) (hDistinct : ¬linearEquiv M.graph (oneChip M.u - oneChip M.v) 0) (hNeg : rankDelta M D < 0) : CFDiv.degree D = 2

On a connected genus-two graph, the preceding lower bound and Riemann--Roch duality force every negative second-difference witness to have degree exactly two.

theorem Bananas.rank_eq_zero_of_rankDelta_neg_genus_two (M : TwiceMarked) (D : CFDiv M.graph) (hConn : _root_.graphConnected M.graph) (hGenus : M.graph.genus = 2) (hDistinct : ¬linearEquiv M.graph (oneChip M.u - oneChip M.v) 0) (hNeg : rankDelta M D < 0) : rank M.graph D = 0

The complete intrinsic rank reduction used in the theta classification. The Riemann--Roch term is handled explicitly: in genus two it is 1, not 0, so a possible rank-one degree-two witness must be ruled out using the inequivalence of the marks.

theorem Bananas.degree_and_rank_eq_of_rankDelta_neg_genus_two (M : TwiceMarked) (D : CFDiv M.graph) (hConn : _root_.graphConnected M.graph) (hGenus : M.graph.genus = 2) (hDistinct : ¬linearEquiv M.graph (oneChip M.u - oneChip M.v) 0) (hNeg : rankDelta M D < 0) : CFDiv.degree D = 2 ∧ rank M.graph D = 0

Combined form of the genus-two reduction, matching the usable content of Lemma 3.1(1) in the paper.