The inversion count in Section 5

This module isolates the finite combinatorial part of the final proposition in Section 5. Its remaining graph-theoretic input is the identification of the displayed rank-drop sum with the cardinality of the finite fibres below.

def Bananas.sectionFiveRankDropFibre (tau : ℤ → ℤ) (m : ℤ) : Set ℤ

The points counted by the rank-drop summand at m: they lie weakly to the southeast of (m - 1, m) and have transmission value exactly m - 1.

Equations

• Bananas.sectionFiveRankDropFibre tau m = {b : ℤ | m ≤ b ∧ tau b = m - 1}

theorem Bananas.sectionFive_rankDropFibre_sum_le_inversionCount {tau : ℤ → ℤ} {k : ℕ} (hk : 0 < k) (hAffine : IsKAffine k tau) (hInvolutive : ∀ (a b : ℤ), tau b = a ↔ tau a = b) (hFinite : ∀ (m : Fin k), (sectionFiveRankDropFibre tau ↑↑m).Finite) : ∑ m : Fin k, ↑(sectionFiveRankDropFibre tau ↑↑m).ncard ≤ ↑(kInversionCount k tau)

The finite rank-drop fibres inject into normalized affine inversions when the transmission permutation is self-inverse. This is the ``below the diagonal gives an inversion'' step of the paper proof, with the normalization needed by the Lean definition of kInversionCount.

theorem Bananas.sectionFive_rankDropSum_eq_fibre_sum {M : TwiceMarked} {D : CFDiv M.graph} {tau : ℤ → ℤ} {k : ℕ} (hconn : _root_.graphConnected M.graph) (hTau : IsTransmissionPermutation M D tau) : sectionFiveRankDropSum M D k = ↑(∑ m : Fin k, (sectionFiveRankDropFibre tau ↑↑m).ncard)

The Section 5 rank-drop summand is the cardinality of its corresponding transmission fibre. This is the tauChars part of the paper argument.

theorem Bananas.sectionFive_inversion_lower_bound_of_involutive_transmission_connected {M : TwiceMarked} {D : CFDiv M.graph} {tau : ℤ → ℤ} {k : ℕ} (hk : 0 < k) (hconn : _root_.graphConnected M.graph) (hTau : IsTransmissionPermutation M D tau) (hAffine : IsKAffine k tau) (hInvolutive : ∀ (a b : ℤ), tau b = a ↔ tau a = b) : sectionFiveRankDropSum M D k ≤ ↑(kInversionCount k tau)

Corrected, connected form of the final Section 5 proposition. The paper assumes connected graphs throughout; CFGraph does not bundle that condition, so it is explicit here.