Finite left-justification of banana position coordinates

After the terminating length-reduction pass, coordinates are valid strand positions and at least one is zero. This module formalizes the paper's final sorting pass: terminal coordinates move left of zero coordinates. The sum of the reverse indices of all zeros is a strictly decreasing natural measure.

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

A decreasing measure for the paper's final left-justification pass.

Equations

• Bananas.bananaLeftJustifyMeasure B p = ∑ alpha : Fin (g + 1), if ↑(p alpha) = 0 then g + 1 - ↑alpha else 0

theorem Bananas.bananaLeftJustifyMeasure_swap_lt {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) : bananaLeftJustifyMeasure B (bananaLeftJustifySwap B p alpha beta) < bananaLeftJustifyMeasure B p

def Bananas.bananaLeftJustifyDecreases {g : ℕ} (B : Banana g) (next current : (alpha : Fin (g + 1)) → Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B alpha) : Prop

The strict decrease relation for the measure controlling left justification of strand positions.

Equations

• Bananas.bananaLeftJustifyDecreases B next current = (Bananas.bananaLeftJustifyMeasure B next < Bananas.bananaLeftJustifyMeasure B current)

theorem Bananas.bananaLeftJustifyDecreases_wellFounded {g : ℕ} (B : Banana g) : WellFounded (bananaLeftJustifyDecreases B)

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

The finite left-justification pass terminates and produces the paper's ordering convention, without leaving the displayed relation class.

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

Full existence of the paper's preferred representative modulo the exact displayed diagonal and strand-length lattice.