Arithmetic count for the corrected cross-one-off block

This file proves the pure finite-row count left open by crossOneOff_corrected_inversion_lower_bound_of_finiteRows.

def Bananas.crossOneOffHighIndex (n i : ℕ) : ℕ

Positions congruent to -1 modulo n, indexed from zero.

Equations

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

def Bananas.crossOneOffLowIndex (n i : ℕ) : ℕ

Positive multiples of n, indexed from zero.

Equations

• Bananas.crossOneOffLowIndex n i = (i + 1) * n

def Bananas.crossOneOffMiddleIndex (n t : ℕ) : ℕ

Interior-residue positions in the block, starting at position 2. The shift by t+1 omits the unavailable position 1.

Equations

• Bananas.crossOneOffMiddleIndex n t = t + 2 + 2 * ((t + 1) / (n - 2))

theorem Bananas.crossOneOffMiddleIndex_strictMono {n : ℕ} (_hn : 2 < n) : StrictMono (crossOneOffMiddleIndex n)

theorem Bananas.crossOneOffHighIndex_data {g n F i : ℕ} (hn : 2 < n) (hF : F = g / (n - 1)) (hi : i < F) : 2 ≤ crossOneOffHighIndex n i ∧ crossOneOffHighIndex n i ≤ crossOneOffCutoff g n ∧ crossOneOffRow g n (crossOneOffHighIndex n i) = g + i + 1

theorem Bananas.crossOneOffLowIndex_data {g n F i : ℕ} (hn : 2 < n) (hF : F = g / (n - 1)) (hi : i < F) : 2 ≤ crossOneOffLowIndex n i ∧ crossOneOffLowIndex n i ≤ crossOneOffCutoff g n ∧ crossOneOffRow g n (crossOneOffLowIndex n i) = i + 2

theorem Bananas.crossOneOffMiddleIndex_data {g n F H t : ℕ} (_hg : 2 ≤ g) (hn : 2 < n) (hF : F = g / (n - 1)) (hH : H = g - F - 1) (ht : t < H) : 2 ≤ crossOneOffMiddleIndex n t ∧ crossOneOffMiddleIndex n t ≤ crossOneOffCutoff g n ∧ crossOneOffRow g n (crossOneOffMiddleIndex n t) = g - t ∧ F + 2 ≤ g - t