The closed form of the flip-sign product

Each label a with n instances in flipLabels L contributes (oddPartnerSign ℓ (f a))^n * (-1)^(n*(n-1)/2) to the sign product of the flip sequence, so a sequence in which every label occurs evenly contributes exactly (−1)^length. That is the sign bookkeeping the paired step of Proposition 3 runs on.

theorem RS.flipSignProd_nil {α : Type} {ℓ : ℕ} (f : α → Fin (2 * ℓ)) : flipSignProd f [] = 1

The empty flip sequence contributes no sign.

theorem RS.flipSignProd_cons {α : Type} {ℓ : ℕ} (f : α → Fin (2 * ℓ)) (p : α × α) (L : List (α × α)) : flipSignProd f (p :: L) = oddPartnerSign ℓ (f p.1) * oddPartnerSign ℓ (f p.2) * flipSignProd (flipColours f p) L

One more flip contributes its two port signs, at the colours reached so far.

theorem RS.oddPartnerSign_flipColours_of_mem {α : Type} {ℓ : ℕ} (f : α → Fin (2 * ℓ)) (p : α × α) {a : α} (ha : a = p.1 ∨ a = p.2) : oddPartnerSign ℓ (flipColours f p a) = -oddPartnerSign ℓ (f a)

The flipped colour of a participating label has the opposite sign.

theorem RS.flipColours_of_not_mem {α : Type} {ℓ : ℕ} (f : α → Fin (2 * ℓ)) (p : α × α) {a : α} (ha : ¬(a = p.1 ∨ a = p.2)) : flipColours f p a = f a

A non-participating label keeps its colour.

theorem RS.flipLabels_length {α : Type} (L : List (α × α)) : (flipLabels L).length = 2 * L.length

Each flip contributes two label instances.

theorem RS.flipSignProd_formula {α : Type} {ℓ : ℕ} (f : α → Fin (2 * ℓ)) (L : List (α × α)) (hd : ∀ p ∈ L, p.1 ≠ p.2) : flipSignProd f L = ∏ a ∈ (flipLabels L).toFinset, oddPartnerSign ℓ (f a) ^ List.count a (flipLabels L) * (-1) ^ (List.count a (flipLabels L) * (List.count a (flipLabels L) - 1) / 2)

The closed form of the flip-sign product: each label a with n instances in flipLabels L contributes the initial sign to the n-th power times the triangular-number sign.

theorem RS.flipSignProd_of_even {α : Type} {ℓ : ℕ} (f : α → Fin (2 * ℓ)) (L : List (α × α)) (hd : ∀ p ∈ L, p.1 ≠ p.2) (heven : ∀ (a : α), List.count a (flipLabels L) % 2 = 0) : flipSignProd f L = (-1) ^ L.length

The even corollary: a flip sequence in which every label occurs an even number of times has sign product (−1)^length.