Integer-lattice reduction for banana coordinates

This file formalizes two elementary moves in the reduction algorithm used in Proposition 2.14. Subtracting the least coordinate times the diagonal makes all coordinates nonnegative and leaves a zero coordinate. Once coordinates lie in their strand intervals, an out-of-order terminal/zero pair can be swapped by a difference of two displayed strand-length relations.

The remaining existence step is the terminating iteration which alternates diagonal normalization with reducing coordinates larger than their strand length. The lemmas here record the algebraic invariants needed by that iteration without hiding them in the full kernel of the class map.

def Bananas.bananaDisplayedRelations {g : ℕ} (B : Banana g) : AddSubgroup (Fin (g + 1) → ℤ)

The relation lattice displayed in Proposition 2.14: it is generated by the diagonal vector and the strand-length relations based at strand zero.

Equations

• Bananas.bananaDisplayedRelations B = AddSubgroup.closure ({Bananas.bananaDiagonalRelation} ∪ Set.range (Bananas.bananaStrandLengthRelation B))

theorem Bananas.bananaDiagonalRelation_mem_displayedRelations {g : ℕ} (B : Banana g) : bananaDiagonalRelation ∈ bananaDisplayedRelations B

theorem Bananas.bananaStrandLengthRelation_mem_displayedRelations {g : ℕ} (B : Banana g) (beta : Fin (g + 1)) : bananaStrandLengthRelation B beta ∈ bananaDisplayedRelations B

theorem Bananas.bananaDisplayedRelations_le_coordinateRelations {g : ℕ} (B : Banana g) : bananaDisplayedRelations B ≤ bananaCoordinateRelations B

Every displayed relation is an actual relation of the graph-level class map.

def Bananas.bananaDiagonalNormalize {g : ℕ} (a : Fin (g + 1) → ℤ) (pivot : Fin (g + 1)) : Fin (g + 1) → ℤ

Subtract the coordinate at pivot from every coordinate.

Equations

• Bananas.bananaDiagonalNormalize a pivot = a - a pivot • Bananas.bananaDiagonalRelation

@[simp]

theorem Bananas.bananaDiagonalNormalize_apply {g : ℕ} (a : Fin (g + 1) → ℤ) (pivot alpha : Fin (g + 1)) : bananaDiagonalNormalize a pivot alpha = a alpha - a pivot

theorem Bananas.bananaDiagonalNormalize_pivot {g : ℕ} (a : Fin (g + 1) → ℤ) (pivot : Fin (g + 1)) : bananaDiagonalNormalize a pivot pivot = 0

theorem Bananas.sub_bananaDiagonalNormalize {g : ℕ} (a : Fin (g + 1) → ℤ) (pivot : Fin (g + 1)) : a - bananaDiagonalNormalize a pivot = a pivot • bananaDiagonalRelation

Diagonal normalization changes a vector by an explicit multiple of the paper's diagonal generator.

theorem Bananas.sub_bananaDiagonalNormalize_mem_relations {g : ℕ} (B : Banana g) (a : Fin (g + 1) → ℤ) (pivot : Fin (g + 1)) : a - bananaDiagonalNormalize a pivot ∈ bananaCoordinateRelations B

Hence diagonal normalization preserves the presented divisor class.

theorem Bananas.sub_bananaDiagonalNormalize_mem_displayedRelations {g : ℕ} (B : Banana g) (a : Fin (g + 1) → ℤ) (pivot : Fin (g + 1)) : a - bananaDiagonalNormalize a pivot ∈ bananaDisplayedRelations B

theorem Bananas.exists_nonnegative_zero_diagonalNormalize {g : ℕ} (B : Banana g) (a : Fin (g + 1) → ℤ) : ∃ (b : Fin (g + 1) → ℤ), (∃ (pivot : Fin (g + 1)), b pivot = 0) ∧ (∀ (alpha : Fin (g + 1)), 0 ≤ b alpha) ∧ a - b ∈ bananaCoordinateRelations B

Every integer coordinate vector can be made nonnegative with a zero coordinate using only the diagonal relation. This is the first normalization step in the paper's reduction algorithm.

theorem Bananas.exists_nonnegative_zero_mod_displayedRelations {g : ℕ} (B : Banana g) (a : Fin (g + 1) → ℤ) : ∃ (b : Fin (g + 1) → ℤ), (∃ (pivot : Fin (g + 1)), b pivot = 0) ∧ (∀ (alpha : Fin (g + 1)), 0 ≤ b alpha) ∧ a - b ∈ bananaDisplayedRelations B

The same first normalization step, now stated in the exact displayed relation lattice rather than the full kernel.

def Bananas.bananaPairwiseLengthRelation {g : ℕ} (B : Banana g) (alpha beta : Fin (g + 1)) : Fin (g + 1) → ℤ

The displayed relation comparing arbitrary strands alpha and beta. It is the difference of the paper's two generators based at strand zero.

Equations

• Bananas.bananaPairwiseLengthRelation B alpha beta = ↑(B.length alpha) • Bananas.bananaCoordinateBasis alpha - ↑(B.length beta) • Bananas.bananaCoordinateBasis beta

theorem Bananas.bananaPairwiseLengthRelation_eq {g : ℕ} (B : Banana g) (alpha beta : Fin (g + 1)) : bananaPairwiseLengthRelation B alpha beta = bananaStrandLengthRelation B beta - bananaStrandLengthRelation B alpha

theorem Bananas.bananaPairwiseLengthRelation_mem_relations {g : ℕ} (B : Banana g) (alpha beta : Fin (g + 1)) : bananaPairwiseLengthRelation B alpha beta ∈ bananaCoordinateRelations B

theorem Bananas.bananaPairwiseLengthRelation_mem_displayedRelations {g : ℕ} (B : Banana g) (alpha beta : Fin (g + 1)) : bananaPairwiseLengthRelation B alpha beta ∈ bananaDisplayedRelations B

def Bananas.bananaLeftJustifySwap {g : ℕ} (B : Banana g) (p : (gamma : Fin (g + 1)) → Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B gamma) (alpha beta gamma : Fin (g + 1)) : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B gamma

Exchange a zero at beta with a terminal coordinate at alpha. Every output is a valid position because zero and the strand length are both endpoints of PathPosition.

Equations

• Bananas.bananaLeftJustifySwap B p alpha beta gamma = if gamma = alpha then ⟨0, ⋯⟩ else if gamma = beta then ⟨B.length gamma, ⋯⟩ else p gamma

@[simp]

theorem Bananas.bananaLeftJustifySwap_at_full {g : ℕ} (B : Banana g) (p : (gamma : Fin (g + 1)) → Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B gamma) (alpha beta : Fin (g + 1)) : ↑(bananaLeftJustifySwap B p alpha beta alpha) = 0

@[simp]

theorem Bananas.bananaLeftJustifySwap_at_zero {g : ℕ} (B : Banana g) (p : (gamma : Fin (g + 1)) → Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B gamma) (alpha beta : Fin (g + 1)) (h : beta ≠ alpha) : ↑(bananaLeftJustifySwap B p alpha beta beta) = B.length beta

theorem Bananas.bananaLeftJustifySwap_at_other {g : ℕ} (B : Banana g) (p : (gamma : Fin (g + 1)) → Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B gamma) (alpha beta gamma : Fin (g + 1)) (hAlpha : gamma ≠ alpha) (hBeta : gamma ≠ beta) : bananaLeftJustifySwap B p alpha beta gamma = p gamma

theorem Bananas.positionCoordinates_sub_leftJustifySwap {g : ℕ} (B : Banana g) (p : (gamma : Fin (g + 1)) → Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B gamma) (alpha beta : Fin (g + 1)) (hFull : ↑(p alpha) = B.length alpha) (hZero : ↑(p beta) = 0) : bananaPositionCoordinates B p - bananaPositionCoordinates B (bananaLeftJustifySwap B p alpha beta) = bananaPairwiseLengthRelation B alpha beta

A left-justification swap differs from the original coordinate vector by exactly one pairwise length relation.

theorem Bananas.leftJustifySwap_normalization_step {g : ℕ} (B : Banana g) (p : (gamma : Fin (g + 1)) → Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B gamma) (alpha beta : Fin (g + 1)) (_hOrder : beta < alpha) (hFull : ↑(p alpha) = B.length alpha) (hZero : ↑(p beta) = 0) : (∃ (gamma : Fin (g + 1)), ↑(bananaLeftJustifySwap B p alpha beta gamma) = 0) ∧ bananaPositionCoordinates B p - bananaPositionCoordinates B (bananaLeftJustifySwap B p alpha beta) ∈ bananaCoordinateRelations B

The local ``move a terminal coordinate left and a zero right'' operation used in the paper preserves the presented class and retains a zero coordinate. The order hypothesis identifies precisely an out-of-order pair; it is not needed for the lattice identity itself.

theorem Bananas.leftJustifySwap_mod_displayedRelations {g : ℕ} (B : Banana g) (p : (gamma : Fin (g + 1)) → Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B gamma) (alpha beta : Fin (g + 1)) (hFull : ↑(p alpha) = B.length alpha) (hZero : ↑(p beta) = 0) : bananaPositionCoordinates B p - bananaPositionCoordinates B (bananaLeftJustifySwap B p alpha beta) ∈ bananaDisplayedRelations B

The same left-justification move in the exact displayed lattice.

theorem Bananas.isPaperReduced_iff_no_leftJustify_pair {g : ℕ} (B : Banana g) (p : (gamma : Fin (g + 1)) → Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B gamma) : IsPaperReducedPositionCoordinates B p ↔ (∃ (gamma : Fin (g + 1)), ↑(p gamma) = 0) ∧ ¬∃ (alpha : Fin (g + 1)), ∃ beta < alpha, ↑(p alpha) = B.length alpha ∧ ↑(p beta) = 0

The ordering clause in IsPaperReducedPositionCoordinates says exactly that no zero occurs to the left of a terminal coordinate.