Degree-one representatives

This small interface isolates the standard step in the theta proof: a rank-zero, degree-one divisor class is represented by one vertex; on a nontrivial banana that vertex is unique.

theorem Bananas.one_chip_representative_unique_on_banana {g : ℕ} (hg : 1 ≤ g) (B : Banana g) {D : CFDiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B)} {x y : (Utilities.Certificate.SubdivisionGraph.Spec.graph B).V} (hDx : linearEquiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B) D (oneChip x)) (hDy : linearEquiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B) D (oneChip y)) : x = y

On a nontrivial banana the vertex representative in the previous theorem is unique.