Explicit coordinates for the corrected cross-one-off inversion count

This module reparametrizes the finite rows by x = b - b / n. The preferred row over x is x + x / (n - 1); at multiples of n - 1 there is also the immediately preceding row. This is the combinatorial skeleton behind the count choose (g - 1) 2 + g / (n - 1).

def Bananas.crossOneOffColumnPosition (n x : ℕ) : ℕ

The preferred row with compressed coordinate x.

Equations

• Bananas.crossOneOffColumnPosition n x = x + x / (n - 1)

def Bananas.crossOneOffPredecessorPosition (n x : ℕ) : ℕ

A row strictly before the preferred row over x, chosen so that it is never a multiple of n. At a multiple of n-1 it is the exceptional -1-residue row; otherwise it is the preferred row itself.

Equations

• Bananas.crossOneOffPredecessorPosition n x = if x % (n - 1) = 0 then Bananas.crossOneOffColumnPosition n x - 1 else Bananas.crossOneOffColumnPosition n x

theorem Bananas.crossOneOffColumnPosition_div {n x : ℕ} (hn : 2 ≤ n) : crossOneOffColumnPosition n x / n = x / (n - 1)

theorem Bananas.crossOneOffColumnPosition_mod {n x : ℕ} (hn : 2 ≤ n) : crossOneOffColumnPosition n x % n = x % (n - 1)

theorem Bananas.crossOneOffColumnPosition_decode {n x : ℕ} (hn : 2 ≤ n) : crossOneOffColumnPosition n x - crossOneOffColumnPosition n x / n = x

theorem Bananas.crossOneOffColumnPosition_injective {n : ℕ} (hn : 2 ≤ n) : Function.Injective (crossOneOffColumnPosition n)

theorem Bananas.crossOneOffPredecessorPosition_decode {n x : ℕ} (hn : 2 ≤ n) (hx : 2 ≤ x) : crossOneOffPredecessorPosition n x - crossOneOffPredecessorPosition n x / n = x

theorem Bananas.crossOneOffPredecessorPosition_injective {n : ℕ} (hn : 2 ≤ n) : Set.InjOn (crossOneOffPredecessorPosition n) (Set.Ici 2)

theorem Bananas.crossOneOffColumnPosition_strictMono {n : ℕ} (_hn : 2 ≤ n) : StrictMono (crossOneOffColumnPosition n)

theorem Bananas.crossOneOffPredecessorPosition_lt_column {n x y : ℕ} (hn : 2 ≤ n) (hyx : y < x) : crossOneOffPredecessorPosition n y < crossOneOffColumnPosition n x

theorem Bananas.crossOneOffColumnPosition_le_cutoff {g n x : ℕ} (_hn : 2 ≤ n) (hxg : x ≤ g) : crossOneOffColumnPosition n x ≤ crossOneOffCutoff g n

theorem Bananas.crossOneOffColumnPosition_row {g n x : ℕ} (hn : 2 ≤ n) (hxg : x ≤ g) : crossOneOffRow g n (crossOneOffColumnPosition n x) = if x % (n - 1) = 0 then x / (n - 1) + 1 else g + x / (n - 1) + 2 - x

theorem Bananas.crossOneOffPredecessorPosition_row {g n x : ℕ} (hn : 3 ≤ n) (hx : 2 ≤ x) (hxg : x ≤ g) : crossOneOffRow g n (crossOneOffPredecessorPosition n x) = if x % (n - 1) = 0 then g + x / (n - 1) else g + x / (n - 1) + 2 - x

theorem Bananas.crossOneOff_predecessor_column_mem {g n y x : ℕ} (hn : 3 ≤ n) (hy : 2 ≤ y) (hyx : y < x) (hxg : x ≤ g) : (crossOneOffPredecessorPosition n y, crossOneOffColumnPosition n x) ∈ crossOneOffForcedInversionPairs g n

A predecessor row at compressed coordinate y and a column row at a larger compressed coordinate x form one of the forced inversions.

noncomputable def Bananas.crossOneOffTriangularPair (n g : ℕ) : Sym2 (Fin (g - 2)) → ℕ × ℕ

The triangular family of inversions indexed by unordered pairs in {2, ..., g-1}.

Equations

• One or more equations did not get rendered due to their size.

theorem Bananas.crossOneOffTriangularPair_injective {n g : ℕ} (hn : 2 ≤ n) : Function.Injective (crossOneOffTriangularPair n g)

def Bananas.crossOneOffAdjacentPair (n i : ℕ) : ℕ × ℕ

The additional adjacent high-to-low inversion over the ith complete column.

Equations

• Bananas.crossOneOffAdjacentPair n i = ((i + 1) * n - 1, (i + 1) * n)

theorem Bananas.crossOneOffAdjacentPair_injective {n : ℕ} (hn : 0 < n) : Function.Injective (crossOneOffAdjacentPair n)

@[reducible, inline]

abbrev Bananas.CrossOneOffCountDomain (g F : ℕ) : Type

The two disjoint families used in the corrected count.

Equations

• Bananas.CrossOneOffCountDomain g F = (Sym2 (Fin (g - 2)) ⊕ Fin F)

noncomputable def Bananas.crossOneOffCountPair (n g F : ℕ) : CrossOneOffCountDomain g F → ℕ × ℕ

Send a triangular or adjacent-pair counting index to its corresponding pair of natural numbers.

Equations

• Bananas.crossOneOffCountPair n g F (Sum.inl x_1) = Bananas.crossOneOffTriangularPair n g x_1
• Bananas.crossOneOffCountPair n g F (Sum.inr i) = Bananas.crossOneOffAdjacentPair n ↑i

theorem Bananas.crossOneOffCountPair_injective {n g F : ℕ} (hn : 3 ≤ n) : Function.Injective (crossOneOffCountPair n g F)

theorem Bananas.correctedCrossOneOffForcedCount_le_card_of_three_le {g n : ℕ} (hg : 2 ≤ g) (hn : 3 ≤ n) : correctedCrossOneOffForcedCount g n ≤ (crossOneOffForcedInversionPairs g n).card

Corrected finite forced-row count for strand lengths at least three.

theorem Bananas.correctedCrossOneOffForcedCount_le_card {g n : ℕ} (hg : 2 ≤ g) (hn : 2 ≤ n) : correctedCrossOneOffForcedCount g n ≤ (crossOneOffForcedInversionPairs g n).card

Pure arithmetic certificate requested by the corrected Corollary 4.31, valid for every strand length at least two.