A well-founded measure for banana-coordinate reduction

The prose reduction in Proposition 2.14 alternates two operations: transfer one strand length from an over-length coordinate to a zero coordinate, then (if that consumed the last zero) subtract the new positive minimum from every coordinate. The lexicographic termination measure is

(sum (a_alpha / n_alpha), number of zero coordinates).

This module proves the strict-decrease facts behind that measure. They are kept on natural-valued nonnegative coordinates; the separate quotient certificate module translates a terminal vector into the displayed integer relation lattice.

def Bananas.bananaQuotientWeight {g : ℕ} (B : Banana g) (a : Fin (g + 1) → ℕ) : ℕ

Sum of the integral strand-length quotients of a nonnegative coordinate vector.

Equations

• Bananas.bananaQuotientWeight B a = ∑ alpha : Fin (g + 1), a alpha / B.length alpha

def Bananas.bananaZeroSet {g : ℕ} (a : Fin (g + 1) → ℕ) : Finset (Fin (g + 1))

Coordinates currently equal to zero.

Equations

• Bananas.bananaZeroSet a = {alpha : Fin (g + 1) | a alpha = 0}

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

Move one full strand length from coordinate alpha to the zero coordinate beta.

Equations

• Bananas.bananaLengthTransfer B a alpha beta gamma = if gamma = alpha then a gamma - B.length gamma else if gamma = beta then B.length gamma else a gamma

@[simp]

theorem Bananas.bananaLengthTransfer_apply_alpha {g : ℕ} (B : Banana g) (a : Fin (g + 1) → ℕ) (alpha beta : Fin (g + 1)) : bananaLengthTransfer B a alpha beta alpha = a alpha - B.length alpha

@[simp]

theorem Bananas.bananaLengthTransfer_apply_beta {g : ℕ} (B : Banana g) (a : Fin (g + 1) → ℕ) (alpha beta : Fin (g + 1)) (hNe : alpha ≠ beta) : bananaLengthTransfer B a alpha beta beta = B.length beta

theorem Bananas.bananaLengthTransfer_apply_other {g : ℕ} (B : Banana g) (a : Fin (g + 1) → ℕ) (alpha beta gamma : Fin (g + 1)) (hAlpha : gamma ≠ alpha) (hBeta : gamma ≠ beta) : bananaLengthTransfer B a alpha beta gamma = a gamma

theorem Bananas.bananaQuotientWeight_lengthTransfer {g : ℕ} (B : Banana g) (a : Fin (g + 1) → ℕ) (alpha beta : Fin (g + 1)) (hOver : B.length alpha < a alpha) (hZero : a beta = 0) : bananaQuotientWeight B (bananaLengthTransfer B a alpha beta) = bananaQuotientWeight B a

A length transfer preserves the quotient-weight component of the termination measure.

theorem Bananas.bananaZeroSet_lengthTransfer_ssubset {g : ℕ} (B : Banana g) (a : Fin (g + 1) → ℕ) (alpha beta : Fin (g + 1)) (hOver : B.length alpha < a alpha) (hZero : a beta = 0) : bananaZeroSet (bananaLengthTransfer B a alpha beta) ⊂ bananaZeroSet a

A transfer removes the chosen zero and creates no new zero. Consequently its zero set is a strict subset of the old zero set whenever some other zero remains.

def Bananas.bananaShiftDown {g : ℕ} (a : Fin (g + 1) → ℕ) (m : ℕ) : Fin (g + 1) → ℕ

Subtract a common natural number from all coordinates.

Equations

• Bananas.bananaShiftDown a m alpha = a alpha - m

theorem Bananas.bananaQuotientWeight_shiftDown_lt {g : ℕ} (B : Banana g) (a : Fin (g + 1) → ℕ) (m : ℕ) (beta : Fin (g + 1)) (hmPos : 0 < m) (hmLe : ∀ (alpha : Fin (g + 1)), m ≤ a alpha) (hBeta : a beta = B.length beta) : bananaQuotientWeight B (bananaShiftDown a m) < bananaQuotientWeight B a

If a positive common shift is bounded by every coordinate, then quotient weight cannot increase and strictly drops at any coordinate equal to one full strand length. This is the case used after consuming the unique zero.

def Bananas.bananaReductionMeasure {g : ℕ} (B : Banana g) (a : Fin (g + 1) → ℕ) : ℕ

A single natural number encoding the lexicographic pair (quotient weight, zero count). The block size g+2 is one larger than the number of coordinates, so a drop in quotient weight dominates any change in the zero count.

Equations

• Bananas.bananaReductionMeasure B a = Bananas.bananaQuotientWeight B a * (g + 2) + (Bananas.bananaZeroSet a).card

theorem Bananas.bananaReductionMeasure_lengthTransfer_lt {g : ℕ} (B : Banana g) (a : Fin (g + 1) → ℕ) (alpha beta : Fin (g + 1)) (hOver : B.length alpha < a alpha) (hZero : a beta = 0) : bananaReductionMeasure B (bananaLengthTransfer B a alpha beta) < bananaReductionMeasure B a

If another zero remains, a length transfer strictly decreases the encoded measure through its zero-count component.

theorem Bananas.bananaReductionMeasure_lt_of_quotientWeight_lt {g : ℕ} (B : Banana g) (a b : Fin (g + 1) → ℕ) (hWeight : bananaQuotientWeight B b < bananaQuotientWeight B a) : bananaReductionMeasure B b < bananaReductionMeasure B a

Whenever quotient weight drops, the encoded measure drops as well, regardless of the new zero set.

theorem Bananas.bananaReductionMeasure_shiftDown_lengthTransfer_lt {g : ℕ} (B : Banana g) (a : Fin (g + 1) → ℕ) (alpha beta : Fin (g + 1)) (m : ℕ) (hOver : B.length alpha < a alpha) (hZero : a beta = 0) (hmPos : 0 < m) (hmLe : ∀ (gamma : Fin (g + 1)), m ≤ bananaLengthTransfer B a alpha beta gamma) : bananaReductionMeasure B (bananaShiftDown (bananaLengthTransfer B a alpha beta) m) < bananaReductionMeasure B a

In the unique-zero case, the post-transfer positive-minimum shift strictly decreases the encoded measure through its quotient-weight component.

theorem Bananas.exists_positive_minimum_after_uniqueZero_transfer {g : ℕ} (B : Banana g) (a : Fin (g + 1) → ℕ) (alpha beta : Fin (g + 1)) (hOver : B.length alpha < a alpha) (hZero : a beta = 0) (hUnique : ∀ (gamma : Fin (g + 1)), a gamma = 0 → gamma = beta) : ∃ (m : ℕ), 0 < m ∧ (∀ (gamma : Fin (g + 1)), m ≤ bananaLengthTransfer B a alpha beta gamma) ∧ ∃ (delta : Fin (g + 1)), bananaShiftDown (bananaLengthTransfer B a alpha beta) m delta = 0

If beta is the unique zero, then after transferring a length away from an over-length coordinate every coordinate is positive. Subtracting the finite minimum therefore restores a zero with a positive common shift.

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

Regard nonnegative natural coordinates as integer coordinate vectors.

Equations

• Bananas.bananaNatCoordinates a alpha = ↑(a alpha)

theorem Bananas.natCoordinates_sub_lengthTransfer {g : ℕ} (B : Banana g) (a : Fin (g + 1) → ℕ) (alpha beta : Fin (g + 1)) (hOver : B.length alpha < a alpha) (hZero : a beta = 0) : bananaNatCoordinates a - bananaNatCoordinates (bananaLengthTransfer B a alpha beta) = bananaPairwiseLengthRelation B alpha beta

A transfer is exactly the pairwise displayed strand-length relation.

theorem Bananas.natCoordinates_sub_shiftDown {g : ℕ} (a : Fin (g + 1) → ℕ) (m : ℕ) (hmLe : ∀ (alpha : Fin (g + 1)), m ≤ a alpha) : bananaNatCoordinates a - bananaNatCoordinates (bananaShiftDown a m) = ↑m • bananaDiagonalRelation

theorem Bananas.exists_reductionStep_mod_displayedRelations {g : ℕ} (B : Banana g) (a : Fin (g + 1) → ℕ) (hHasZero : ∃ (beta : Fin (g + 1)), a beta = 0) (alpha : Fin (g + 1)) (hOver : B.length alpha < a alpha) : ∃ (b : Fin (g + 1) → ℕ), (∃ (beta : Fin (g + 1)), b beta = 0) ∧ bananaReductionMeasure B b < bananaReductionMeasure B a ∧ bananaNatCoordinates a - bananaNatCoordinates b ∈ bananaDisplayedRelations B

From any nonnegative vector with a zero and an over-length coordinate, there is a strictly smaller normalized vector in the same displayed-lattice class. This is the complete recursive step for the first two paper-reduced conditions.

def Bananas.bananaReductionDecreases {g : ℕ} (B : Banana g) (next current : Fin (g + 1) → ℕ) : Prop

The strict relation induced by bananaReductionMeasure is well founded; this is the recursion principle needed to iterate the paper's reduction moves.

Equations

• Bananas.bananaReductionDecreases B next current = (Bananas.bananaReductionMeasure B next < Bananas.bananaReductionMeasure B current)

theorem Bananas.bananaReductionDecreases_wellFounded {g : ℕ} (B : Banana g) : WellFounded (bananaReductionDecreases B)

theorem Bananas.exists_bounded_zero_natCoordinates_mod_displayedRelations {g : ℕ} (B : Banana g) (a : Fin (g + 1) → ℕ) (hHasZero : ∃ (beta : Fin (g + 1)), a beta = 0) : ∃ (b : Fin (g + 1) → ℕ), (∃ (beta : Fin (g + 1)), b beta = 0) ∧ (∀ (alpha : Fin (g + 1)), b alpha ≤ B.length alpha) ∧ bananaNatCoordinates a - bananaNatCoordinates b ∈ bananaDisplayedRelations B

Terminating existence for the first two paper-reduced conditions. Every nonnegative coordinate vector having a zero is congruent modulo the displayed lattice to another such vector lying in all closed strand intervals.

theorem Bananas.exists_positionCoordinates_with_zero_mod_displayedRelations {g : ℕ} (B : Banana g) (a : Fin (g + 1) → ℤ) : ∃ (p : (alpha : Fin (g + 1)) → Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B alpha), (∃ (alpha : Fin (g + 1)), ↑(p alpha) = 0) ∧ a - bananaPositionCoordinates B p ∈ bananaDisplayedRelations B

Every integer vector has a representative by valid strand positions with at least one zero coordinate, modulo exactly the displayed relation lattice. This completes conditions (1) and (2) of the paper's reduction convention; the ordering of terminal coordinates versus zeros is the remaining finite left-justification step.