Rank-zero witnesses as reduced one-chip classes

The theta argument starts with a negative second-difference witness. In genus two its deletion at either mark has degree one and rank zero. Reducing that deletion at the other mark therefore gives a single vertex rather than an arbitrary divisor. This file records that passage in the precise form needed before applying the banana cut calculation.

theorem Bananas.exists_one_chip_representative_of_rank_zero_degree_one (G : CFGraph) (A : CFDiv G) (hRank : rank G A = 0) (hDeg : CFDiv.degree A = 1) : ∃ (x : G.V), linearEquiv G A (oneChip x)

A degree-one winnable divisor has a representative consisting of one chip.

theorem Bananas.exists_qReduced_vertex_rep_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) : ∃ (w : M.graph.V), linearEquiv M.graph (D - oneChip M.u) (oneChip w) ∧ qReduced M.graph M.v (oneChip w) ∧ w ≠ M.v ∧ rank M.graph (oneChip w + oneChip M.u - oneChip M.v) = 0

In the genus-two negative-Δ situation, reducing D-u at v produces a unique one-chip representative. It is not v, and translating back identifies the rank-zero divisor to which the SameStrand lemma is applied in the paper.