The immediate one-off inversion bound

This formalizes the unnamed proposition immediately following Lemma 4.23. The selected positive-residue rows form a strictly decreasing subsequence of length (n-2) * floor(g/(n-1)), hence contribute the corresponding binomial number of distinct k-inversions.

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

Increasing enumeration of the positive residues in blocks of width n: two residue classes (0 and n-1) are skipped per block.

Equations

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

theorem Bananas.oneOffPositiveIndex_strictMono {n : ℕ} (_hn : 2 < n) : StrictMono (oneOffPositiveIndex n)

noncomputable def Bananas.indexedPairEmbedding (index : ℕ → ℕ) (length : ℕ) : Sym2 (Fin length) → ℤ × ℤ

Encode an unordered pair by the indexed smaller position and the index after the larger position.

Equations

• Bananas.indexedPairEmbedding index length = Sym2.lift ⟨fun (a b : Fin length) => (↑(index (min ↑a ↑b)), ↑(index (max ↑a ↑b + 1))), ⋯⟩

theorem Bananas.indexedPairEmbedding_injective {index : ℕ → ℕ} (hIndex : Function.Injective index) (length : ℕ) : Function.Injective (indexedPairEmbedding index length)

theorem Bananas.indexed_decreasing_inversion_lower_bound {length value k : ℕ} {index : ℕ → ℕ} {tau : ℤ → ℤ} (hIndex : StrictMono index) (hValue : length ≤ value) (hFirst : ∀ i < length, index i < k) (hBlock : ∀ i ≤ length, tau ↑(index i) = ↑(value - i)) (hfinite : (kInversions k tau).Finite) : (length + 1).choose 2 ≤ kInversionCount k tau

A decreasing sequence sampled at arbitrary strictly increasing natural indices contributes all of its pairwise inversions. The bound on possible first coordinates is stated only for i < length; the last sampled point can occur only as a second coordinate.

theorem Bananas.oneOff_inversion_lower_bound {g k : ℕ} (B : Banana g) (alpha : Fin (g + 1)) (tau : ℤ → ℤ) (hg : 2 ≤ g) (hk : 0 < k) (hLength : 1 < B.length alpha) (hTau : IsTransmissionPermutation (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (leftEndpoint B) (strandVertex B alpha ⟨B.length alpha - 1, ⋯⟩)) (g • oneChip (rightEndpoint B)) tau) (hAffine : IsKAffine k tau) (hfinite : (kInversions k tau).Finite) : ((B.length alpha - 2) * (g / (B.length alpha - 1))).choose 2 ≤ kInversionCount k tau

The corrected form of the immediate inversion lower bound following Lemma 4.23.