Finite-row inversion counting for the corrected both-off block

The corrected rows of Lemma 4.30 extend to crossOneOffCutoff g n. To count their ordinary inversions as distinct affine inversions one must additionally know that this cutoff is at most the affine period. This file makes that finite-row injection precise and then specializes it to the corrected cross-one-off row function.

def Bananas.finiteRowInversionPairs (lo hi : ℕ) (row : ℕ → ℕ) : Finset (ℕ × ℕ)

Ordered pairs of rows in [lo, hi] on which a finite row function is strictly decreasing.

Equations

• Bananas.finiteRowInversionPairs lo hi row = {ij ∈ (Finset.Icc lo hi).product (Finset.Icc lo hi) | ij.1 < ij.2 ∧ row ij.1 > row ij.2}

def Bananas.finiteRowPairCast : ℕ × ℕ → ℤ × ℤ

Cast a natural-number row pair to the integer pair used by kInversions.

Equations

• Bananas.finiteRowPairCast ij = (↑ij.1, ↑ij.2)

theorem Bananas.finiteRowPairCast_injective : Function.Injective finiteRowPairCast

theorem Bananas.finiteRowInversionPairs_card_le_kInversionCount {lo hi k : ℕ} {row : ℕ → ℕ} {tau : ℤ → ℤ} (hRows : ∀ (b : ℕ), lo ≤ b → b ≤ hi → tau ↑b = ↑(row b)) (hSeparate : hi ≤ k) (hfinite : (kInversions k tau).Finite) : (finiteRowInversionPairs lo hi row).card ≤ kInversionCount k tau

Every inversion visible in a finite row block injects into the normalized k-inversion set when the final row is at most the period. Equality hi = k is allowed: the first coordinate of every inversion is strictly smaller than its second coordinate.

def Bananas.crossOneOffForcedInversionPairs (g n : ℕ) : Finset (ℕ × ℕ)

The finite set of all ordinary inversions forced by the corrected common block 2 ≤ b ≤ crossOneOffCutoff g n.

Equations

• Bananas.crossOneOffForcedInversionPairs g n = Bananas.finiteRowInversionPairs 2 (Bananas.crossOneOffCutoff g n) (Bananas.crossOneOffRow g n)

theorem Bananas.crossOneOff_forcedInversionPairs_card_le {g k : ℕ} (B : Banana g) (alpha beta : Fin (g + 1)) (tau : ℤ → ℤ) (hg : 2 ≤ g) (hab : alpha ≠ beta) (hAlpha : 1 < B.length alpha) (hBeta : 1 < B.length beta) (hLong : CrossOneOffLongEnough g (B.length alpha) (B.length beta)) (hTau : IsTransmissionPermutation (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B alpha ⟨1, ⋯⟩) (strandVertex B beta ⟨B.length beta - 1, ⋯⟩)) (g • oneChip (rightEndpoint B)) tau) (hSeparate : crossOneOffCutoff g (B.length beta) ≤ k) (hfinite : (kInversions k tau).Finite) : (crossOneOffForcedInversionPairs g (B.length beta)).card ≤ kInversionCount k tau

Under the missing period-separation hypothesis from Corollary 4.31, every forced finite-row inversion is a distinct normalized affine inversion.

def Bananas.correctedCrossOneOffForcedCount (g n : ℕ) : ℕ

The corrected numerical target from Corollary 4.31. Its n = 2 branch accounts for the corrected block beginning at row 2; for n ≥ 3 the target is choose (g-1) 2 + floor(g/(n-1)).

Equations

• Bananas.correctedCrossOneOffForcedCount g n = if n = 2 then g.choose 2 else (g - 1).choose 2 + g / (n - 1)

theorem Bananas.crossOneOff_corrected_inversion_lower_bound_of_finiteRows {g k : ℕ} (B : Banana g) (alpha beta : Fin (g + 1)) (tau : ℤ → ℤ) (hg : 2 ≤ g) (hab : alpha ≠ beta) (hAlpha : 1 < B.length alpha) (hBeta : 1 < B.length beta) (hLong : CrossOneOffLongEnough g (B.length alpha) (B.length beta)) (hTau : IsTransmissionPermutation (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B alpha ⟨1, ⋯⟩) (strandVertex B beta ⟨B.length beta - 1, ⋯⟩)) (g • oneChip (rightEndpoint B)) tau) (hSeparate : crossOneOffCutoff g (B.length beta) ≤ k) (hfinite : (kInversions k tau).Finite) (hSharp : correctedCrossOneOffForcedCount g (B.length beta) ≤ (crossOneOffForcedInversionPairs g (B.length beta)).card) : correctedCrossOneOffForcedCount g (B.length beta) ≤ kInversionCount k tau

A sharp finite-row block certificate implies the corrected Corollary 4.31 lower bound, provided the cutoff lies in one affine period. The remaining pure arithmetic task is to construct hSharp for crossOneOffRow.