Quotient certificates for the displayed banana relation lattice

This module packages the arithmetic invariant used by the reduction algorithm in Proposition 2.14. After a common diagonal shift, suppose each coordinate is written as a valid strand position plus an integral multiple of that strand's length. If the length quotients sum to zero, the original vector and the position vector differ by an explicit combination of the paper's displayed relation generators.

theorem Bananas.sub_positionCoordinates_mem_displayedRelations_of_quotients {g : ℕ} (B : Banana g) (a : Fin (g + 1) → ℤ) (p : (alpha : Fin (g + 1)) → Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B alpha) (c : ℤ) (q : Fin (g + 1) → ℤ) (hCoordinates : ∀ (alpha : Fin (g + 1)), a alpha + c = ↑↑(p alpha) + ↑(B.length alpha) * q alpha) (hSum : ∑ alpha : Fin (g + 1), q alpha = 0) : a - bananaPositionCoordinates B p ∈ bananaDisplayedRelations B

Arithmetic certificate for membership in the displayed lattice. The integers q_alpha record how many strand lengths were removed after a common diagonal shift c; their sum-zero condition is exactly what makes the strand-zero coordinate agree with the other displayed generators.