Concatenation sign factorisation

The global key-sortSign of the concatenated pair enumeration equals the product of the per-block key-sortSigns: key ranges of distinct blocks are disjoint and ordered, so concatenation adds no inversions.

Cross-block key monotonicity

theorem RS.blockSigmaEquiv_lt_of_block_lt {ds : List ℕ} {v₁ v₂ : Fin ds.length} : v₁ < v₂ → ∀ (j₁ : Fin (ds.get v₁)) (j₂ : Fin (ds.get v₂)), (blockSigmaEquiv ds) ⟨v₁, j₁⟩ < (blockSigmaEquiv ds) ⟨v₂, j₂⟩

Keys from an earlier block are strictly less than keys from a later block.

Inversions under ordered append

theorem RS.inversions_append_of_le {α : Type} [LinearOrder α] (l₁ l₂ : List α) : (∀ x ∈ l₁, ∀ y ∈ l₂, x ≤ y) → inversions (l₁ ++ l₂) = inversions l₁ + inversions l₂

Appending two lists whose elements are in order adds no inversions.

theorem RS.sortSign_append_of_le {α : Type} [LinearOrder α] (l₁ l₂ : List α) (h : ∀ x ∈ l₁, ∀ y ∈ l₂, x ≤ y) : sortSign (l₁ ++ l₂) = sortSign l₁ * sortSign l₂

The sortSign is multiplicative under ordered append.

Key membership in blocks

theorem RS.sortKey_mem_block (W : ClosedFragment) (F : EdgeSubset W) {κ : F.TransitionSystem} (o : κ.Orientation) (v : Fin (ds W).length) (f : ↥F.flags) (hf : f ∈ pairFlagList o (blockVertex W v)) : ∃ (j : Fin ((ds W).get v)), sortKey W ↑f = (blockSigmaEquiv (ds W)) ⟨v, j⟩

A pair-flag at block v has its key in that block's sigma range.

Global list properties

theorem RS.globalPairList_nodup (W : ClosedFragment) (F : EdgeSubset W) {κ : F.TransitionSystem} (o : κ.Orientation) : (globalPairList W F o).Nodup

The global pair list is duplicate-free.

theorem RS.mem_globalPairList (W : ClosedFragment) (F : EdgeSubset W) {κ : F.TransitionSystem} (o : κ.Orientation) (x : ↥F.flags) : x ∈ globalPairList W F o

Every participating flag appears in the global pair list.

Main theorem

theorem RS.sortSign_globalPairList (W : ClosedFragment) (F : EdgeSubset W) {κ : F.TransitionSystem} (o : κ.Orientation) : ↑(sortSign (List.map (fun (f : ↥F.flags) => sortKey W ↑f) (globalPairList W F o))) = ∏ v : Fin (ds W).length, ↑(sortSign (List.map (fun (f : ↥F.flags) => sortKey W ↑f) (pairFlagList o (blockVertex W v))))

The global key-sortSign is the product of the per-block key-sortSigns.