Counting a collision of crossing affine inversions

This file isolates the combinatorial counting step in the proof of paper Proposition 6.1. Two distinct inversions crossing the origin which represent the same affine inversion class force at least 2 * k - 1 distinct affine inversion classes.

def Bananas.normalizeInversionFirst (k : ℕ) (p : ℤ × ℤ) : ℤ × ℤ

Normalize an ordinary inversion by translating its first coordinate into the fundamental interval [0, k).

Equations

• Bananas.normalizeInversionFirst k p = (p.1 % ↑k, p.2 - p.1 / ↑k * ↑k)

theorem Bananas.kInversionCount_ge_two_mul_sub_one_of_crossing_collision {k : ℕ} {tau : ℤ → ℤ} (hk : 0 < k) (hAffine : IsKAffine k tau) {a b a' b' : ℤ} (haNeg : a < 0) (hbNonneg : 0 ≤ b) (haPos : 0 < tau a) (hbNonpos : tau b ≤ 0) (ha'Neg : a' < 0) (hb'Nonneg : 0 ≤ b') (ha'Pos : 0 < tau a') (hb'Nonpos : tau b' ≤ 0) (hDistinct : (a, b) ≠ (a', b')) (hSame : normalizeInversionFirst k (a, b) = normalizeInversionFirst k (a', b')) : 2 * k - 1 ≤ kInversionCount k tau

Two distinct crossing inversions with the same normalized first-coordinate representative force at least 2 * k - 1 affine inversion classes. This is the counting kernel of paper Proposition 6.1.