The pattern inversion count

The master sum's global sign at a data colouring depends only on the pattern: the sort-permutation's odd inversions count pairs of participating slots, a pure (W, F) quantity.

noncomputable def RS.patternOddInv (W : ClosedFragment) (F : EdgeSubset W) : ℕ

The pattern inversion count of an edge subset: inverted sort pairs of participating slots.

Equations

• One or more equations did not get rendered due to their size.

theorem RS.oddInversions_colouringOf {k ℓ : ℕ} (W : ClosedFragment) (F : EdgeSubset W) (ψ : F.EvenColouring k) (φ : F.OddColouring ℓ) : oddInversions (sortSplitPerm W) (colouringOf W F ψ φ ∘ ⇑(finCongr ⋯)) = patternOddInv W F

The master sign at a data colouring is the pattern inversion count.