Uniqueness of the paper's reduced banana coordinates

This is the uniqueness layer in Proposition 2.14. Two preferred position vectors differing by the displayed lattice first give linearly equivalent left-reduced divisors, hence equal divisors by uniqueness of q-reduction.

theorem Bananas.bananaPositionCoordinateDivisor_eq_of_paperReduced_mod_displayed {g : ℕ} (B : Banana g) (p q : (alpha : Fin (g + 1)) → Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B alpha) (hp : IsPaperReducedPositionCoordinates B p) (hq : IsPaperReducedPositionCoordinates B q) (hrel : bananaPositionCoordinates B p - bananaPositionCoordinates B q ∈ bananaDisplayedRelations B) : bananaPositionCoordinateDivisor B p = bananaPositionCoordinateDivisor B q

The q-reduced core of uniqueness: displayed-equivalent paper representatives have exactly the same position-coordinate divisor.

theorem Bananas.paperCoordinateChips_eq_of_positionCoordinateDivisor_eq {g : ℕ} (B : Banana g) (p q : (alpha : Fin (g + 1)) → Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B alpha) (hDiv : bananaPositionCoordinateDivisor B p = bananaPositionCoordinateDivisor B q) : paperCoordinateChips B p = paperCoordinateChips B q

Equality of position-coordinate divisors remembers the semibreak chip on each individual strand, despite the common endpoint aliases.

theorem Bananas.positionCoordinate_eq_of_interior_of_divisor_eq {g : ℕ} (B : Banana g) (p q : (alpha : Fin (g + 1)) → Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B alpha) (hDiv : bananaPositionCoordinateDivisor B p = bananaPositionCoordinateDivisor B q) (alpha : Fin (g + 1)) (hpInterior : IsPaperInteriorCoordinate B p alpha) : p alpha = q alpha

An interior coordinate is recovered strand-by-strand from the associated position-coordinate divisor.

theorem Bananas.paperReducedPositionCoordinates_eq_of_divisor_eq {g : ℕ} (B : Banana g) (p q : (alpha : Fin (g + 1)) → Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B alpha) (hp : IsPaperReducedPositionCoordinates B p) (hq : IsPaperReducedPositionCoordinates B q) (hDiv : bananaPositionCoordinateDivisor B p = bananaPositionCoordinateDivisor B q) : p = q

The apparent endpoint aliases do not create a second preferred representative: the ordering clause makes the endpoint assignment unique.

theorem Bananas.paperReducedPositionCoordinates_eq_mod_displayedRelations {g : ℕ} (B : Banana g) (p q : (alpha : Fin (g + 1)) → Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B alpha) (hp : IsPaperReducedPositionCoordinates B p) (hq : IsPaperReducedPositionCoordinates B q) (hrel : bananaPositionCoordinates B p - bananaPositionCoordinates B q ∈ bananaDisplayedRelations B) : p = q

Full uniqueness/injectivity statement for Proposition 2.14.