Inversions and the sorting sign

The calculus of the sorting sign (inversions and sortSign are defined in RS/Definitions.lean): the sign is antisymmetric under adjacent transpositions of distinct elements, which is the combinatorial engine of the alternating evaluation of mixed vertex functionals.

theorem RS.sortSign_sq {α : Type} [LinearOrder α] (l : List α) : ↑(sortSign l) * ↑(sortSign l) = 1

Sorting signs square to one over ℂ.

theorem RS.inversions_map_orderEmbedding {α β : Type} [LinearOrder α] [LinearOrder β] (e : α ↪o β) (l : List α) : inversions (List.map (⇑e) l) = inversions l

Increasing embeddings preserve inversion counts.

theorem RS.sortSign_map_orderEmbedding {α β : Type} [LinearOrder α] [LinearOrder β] (e : α ↪o β) (l : List α) : sortSign (List.map (⇑e) l) = sortSign l

Increasing embeddings preserve the sorting sign.

theorem RS.inversions_eq_zero_of_sorted {α : Type} [LinearOrder α] (l : List α) : List.Pairwise (fun (x1 x2 : α) => x1 ≤ x2) l → inversions l = 0

Sorted lists have no inversions.

theorem RS.sortSign_eq_one_of_sorted {α : Type} [LinearOrder α] (l : List α) (h : List.Pairwise (fun (x1 x2 : α) => x1 ≤ x2) l) : sortSign l = 1

Sorted lists have sorting sign one.

theorem RS.filter_length_of_perm {α : Type} (p : α → Bool) {l₁ l₂ : List α} (h : l₁.Perm l₂) : (List.filter p l₁).length = (List.filter p l₂).length

Inversion counts are invariant under permuting the tail past a fixed head-filter: permuted lists have equal filter lengths.

theorem RS.sortSign_swap_adjacent {α : Type} [LinearOrder α] (l₁ l₂ : List α) {a b : α} (hab : a ≠ b) : sortSign (l₁ ++ b :: a :: l₂) = -sortSign (l₁ ++ a :: b :: l₂)

Swapping two distinct adjacent elements flips the sorting sign.

theorem RS.sortSign_pair_block_swap {α : Type} [LinearOrder α] (l₁ l₂ : List α) {p₁ p₂ q₁ q₂ : α} (hp₁q₁ : p₁ ≠ q₁) (hp₁q₂ : p₁ ≠ q₂) (hp₂q₁ : p₂ ≠ q₁) (hp₂q₂ : p₂ ≠ q₂) : sortSign (l₁ ++ q₁ :: q₂ :: p₁ :: p₂ :: l₂) = sortSign (l₁ ++ p₁ :: p₂ :: q₁ :: q₂ :: l₂)

Moving a two-element block past another two-element block preserves the sorting sign: four adjacent transpositions, an even number of sign flips.