Lemma 3.1: Kendall's tau of an arbitrary signed shuffle #
S records the horizontal and vertical tilings, with widths allowed to be
zero. π specifies their relative order. A true sign means +1 and a false
sign means -1. The paper's pair sum is written with the indices renamed
j < i; because π is injective, its sign is +1 exactly when π j < π i.
theorem
Papers.OrendayLaresRockel2026TauFootruleBeta.shuffle_tau
{n : ℕ}
(S : Verification.PositiveShuffle n)
(ε : Fin n → Bool)
(π : Equiv.Perm (Fin n))
(hx : ∀ (i j : Fin n), i < j → (S.strip i).x + (S.strip i).width ≤ (S.strip j).x)
(hy : ∀ (i j : Fin n), π i < π j → (S.strip i).y + (S.strip i).width ≤ (S.strip j).y)
: