Negative rank differences at rank zero

This is the rank-theoretic part of Lemma 3.1(2) in the paper. The paper phrases it using supports of a chosen effective representative; the intrinsic form below avoids choosing representatives and is exactly what the later reduced-divisor calculation consumes.

theorem Bananas.rankDelta_neg_iff_rank_zero_deletions (M : TwiceMarked) (D : CFDiv M.graph) (hD : rank M.graph D = 0) : rankDelta M D < 0 ↔ rank M.graph (D - oneChip M.u) = 0 ∧ rank M.graph (D - oneChip M.v) = 0 ∧ rank M.graph (D - oneChip M.u - oneChip M.v) = -1

At rank zero, a negative marked second difference says precisely that each one-chip deletion remains winnable while the two-chip deletion is not. This formulation is invariant under changing the divisor within its linear equivalence class.