The endpoint rank-one criterion for banana graphs

The paper proves lem-BananaRDS by invoking Luo's characterization of a rank-determining set: it is enough to show that a divisor has rank at least one whenever subtracting either member of the proposed set leaves a winnable divisor. The imported chip-firing library does not currently define rank-determining sets or contain Luo's characterization. This file proves the complete banana-specific input to that characterization.

The proof uses the already formalized endpoint/semibreak normal form. The left endpoint test forces the unrestricted left coefficient to be positive. If the Riemann--Roch term does not already give rank one, the right endpoint test forces the bounded right coefficient to be positive as well.

theorem Bananas.banana_rank_one_of_endpoint_residuals {g : ℕ} (B : Banana g) (D : CFDiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) (hLeft : 0 ≤ rank (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (D - oneChip (leftEndpoint B))) (hRight : 0 ≤ rank (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (D - oneChip (rightEndpoint B))) : 1 ≤ rank (Utilities.Certificate.SubdivisionGraph.Spec.graph B) D

TeX label: lem-BananaRDS (Lemma 2.21), banana-specific rank-one criterion used with Luo's rank-determining-set characterization.

If subtracting either multivalent endpoint from a divisor leaves nonnegative rank, then the original divisor has rank at least one. This is exactly the graph-specific assertion proved in the paper after the reduction to rank one; packaging it as the full rank-determining-set statement only requires the currently absent generic definition and Luo equivalence.