The refined same-strand one-off inversion count

This proves paper Proposition 4.25. If n is the length of the marked strand and f = floor(g/(n-1)), the paper's auxiliary quantity h is actually g-f. Consequently its displayed lower bound simplifies to

choose g 2 + f.

The proof uses the paper's compressed coordinate x = b - floor(b/n). There is one preferred row over every 1 <= x <= g, and an additional row immediately before it whenever (n-1) | x. Every ordered pair of compressed coordinates gives an inversion, as does each additional adjacent pair.

def Bananas.oneOffRow (g n b : ℕ) : ℕ

The three rows in Lemma 4.23, written as one finite row function.

Equations

• Bananas.oneOffRow g n b = if b % n = 0 then b / n else if b % n = n - 1 then g + b / n + 1 else g + 2 * (b / n) + 1 - b

theorem Bananas.transmission_oneOff_block {g : ℕ} (B : Banana g) (alpha : Fin (g + 1)) (b : ℕ) (tau : ℤ → ℤ) (hg : 2 ≤ g) (hLength : 1 < B.length alpha) (_hbLo : 1 ≤ b) (hbHi : b ≤ crossOneOffCutoff g (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) : tau ↑b = ↑(oneOffRow g (B.length alpha) b)

Lemma 4.23, uniformly over its full integral cutoff interval.

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

The finite set of ordinary inversions visible in Lemma 4.23's block.

Equations

• Bananas.oneOffForcedInversionPairs g n = Bananas.finiteRowInversionPairs 1 (Bananas.crossOneOffCutoff g n) (Bananas.oneOffRow g n)

theorem Bananas.oneOff_forcedInversionPairs_card_le {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) : (oneOffForcedInversionPairs g (B.length alpha)).card ≤ kInversionCount k tau

Every forced finite-row inversion is a normalized affine inversion. Lemma 4.23's period conclusion supplies the required separation.

Compressed-row arithmetic

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

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

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

The predecessor coordinate has the same compressed coordinate, including the boundary value x=1 needed by Proposition 4.25.

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

theorem Bananas.oneOff_predecessor_column_mem {g n y x : ℕ} (hg : 2 ≤ g) (hn : 2 ≤ n) (hy : 1 ≤ y) (hyx : y < x) (hxg : x ≤ g) : (crossOneOffPredecessorPosition n y, crossOneOffColumnPosition n x) ∈ oneOffForcedInversionPairs g n

A predecessor row over y and the preferred row over x > y form an inversion in the one-off block.

The finite count

noncomputable def Bananas.oneOffTriangularPair (n g : ℕ) : Sym2 (Fin (g - 1)) → ℕ × ℕ

The inversion indexed by an unordered pair of distinct compressed coordinates in {1, ..., g}.

Equations

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

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

@[reducible, inline]

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

Counting indices consisting of unordered pairs on the first part and individual adjacent-pair indices on the second.

Equations

• Bananas.OneOffRefinedCountDomain g F = (Sym2 (Fin (g - 1)) ⊕ Fin F)

noncomputable def Bananas.oneOffRefinedCountPair (n g F : ℕ) : OneOffRefinedCountDomain g F → ℕ × ℕ

Realize the triangular and adjacent-pair parts of the refined counting domain as pairs of natural numbers.

Equations

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

theorem Bananas.oneOffRefinedCountPair_injective {n g F : ℕ} (hn : 2 ≤ n) : Function.Injective (oneOffRefinedCountPair n g F)

theorem Bananas.oneOff_refinedCount_le_card {g n : ℕ} (hg : 2 ≤ g) (hn : 2 ≤ n) : g.choose 2 + g / (n - 1) ≤ (oneOffForcedInversionPairs g n).card

The pure finite-row count in Proposition 4.25.

theorem Bananas.oneOff_refined_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) : g.choose 2 + g / (B.length alpha - 1) ≤ kInversionCount k tau

Proposition 4.25 in its simplified numerical form.

theorem Bananas.oneOff_not_kGeneral_of_four_le_genus {g k : ℕ} (B : Banana g) (alpha : Fin (g + 1)) (hg : 4 ≤ g) (hLength : 1 < B.length alpha) : ¬KGeneralTransmission (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (leftEndpoint B) (strandVertex B alpha ⟨B.length alpha - 1, ⋯⟩)) k

The refined one-off count is already larger than the genus from genus four onward, so this entire same-strand one-off family is never k-general in that range.

theorem Bananas.oneOff_refined_inversion_lower_bound_ledger {g k : ℕ} (B : Banana g) (alpha : Fin (g + 1)) (hg : 2 ≤ g) (hLength : 1 < B.length alpha) (hSub : AllSubmodular (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (leftEndpoint B) (strandVertex B alpha ⟨B.length alpha - 1, ⋯⟩))) (hTO : IsTorsionOrder (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (leftEndpoint B) (strandVertex B alpha ⟨B.length alpha - 1, ⋯⟩)) k) : ∃ (tau : ℤ → ℤ), IsTransmissionPermutation (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (leftEndpoint B) (strandVertex B alpha ⟨B.length alpha - 1, ⋯⟩)) (g • oneChip (rightEndpoint B)) tau ∧ IsKAffine k tau ∧ g.choose 2 + g / (B.length alpha - 1) ≤ kInversionCount k tau

TeX label: prop-oneOffNotGeneral (Proposition 4.25), simplified equivalent form.

For the same-strand one-off marking (leftEndpoint, v_{α,nα-1}), write f = floor(g / (nα - 1)). The paper's auxiliary quantity is h = g - f, so its displayed four-family count is exactly choose(g,2) + f. This statement gives the paper's maximum-inversion conclusion as a concrete divisor/transmission witness.