Generic-genus rank witnesses on bananas

This file is deliberately separate from Statements.lean. It packages the rank facts used by the far-mark construction in Theorem 3.5 of the twice-marked banana paper.

theorem Bananas.rank_eq_neg_one_of_degree_zero_not_linear_equiv (G : CFGraph) (D : CFDiv G) (hDeg : CFDiv.degree D = 0) (hNotPrincipal : ¬linearEquiv G D 0) : rank G D = -1

A degree-zero divisor which is not principal has rank -1.

theorem Bananas.rank_eq_zero_of_effective_of_rank_sub_one_chip_eq_neg_one (G : CFGraph) (D : CFDiv G) (q : G.V) (hEff : effective D) (hSub : rank G (D - oneChip q) = -1) : rank G D = 0

An effective divisor whose deletion at one vertex has rank -1 has rank zero.

theorem Bananas.rank_eq_zero_of_effective_of_qReduced_of_no_chip (G : CFGraph) (q : G.V) (D : CFDiv G) (hEff : effective D) (hRed : qReduced G q D) (hNoChip : D q = 0) : rank G D = 0

A q-reduced effective divisor with no chip at q has rank zero.

theorem Bananas.rank_one_chip_zero_of_banana {g : ℕ} (hg : 1 ≤ g) (B : Banana g) (x : (Utilities.Certificate.SubdivisionGraph.Spec.graph B).V) : rank (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (oneChip x) = 0

The one-chip rank on a nontrivial banana is zero, uniformly in the genus.

theorem Bananas.rank_same_strand_pair_zero_of_not_reflection_generic {g : ℕ} (hg : 2 ≤ g) (B : Banana g) (α : Fin (g + 1)) (i k : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (hNot : ↑i + ↑k ≠ B.length α) : rank (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (oneChip (Utilities.Certificate.SubdivisionGraph.Spec.pathVertex B α i) + oneChip (Utilities.Certificate.SubdivisionGraph.Spec.pathVertex B α k)) = 0

A non-reflected pair on one strand has rank zero in every banana of genus at least two.