The per-vertex sign collapse #
The product of the two per-vertex sorting signs is the key-sortSign of the pair enumeration: both lists are value maps of the two flag enumerations, so the reindexing sign transports between them, and the block enumeration is key-sorted.
theorem
RS.vertex_sign_collapse
{k ℓ : ℕ}
(W : ClosedFragment)
(F : EdgeSubset W)
{κ : F.TransitionSystem}
(o : κ.Orientation)
(ψ : F.EvenColouring k)
(φ : F.OddColouring ℓ)
(v : Fin (ds W).length)
(hnd : (F.oddListAt o φ (blockVertex W v)).Nodup)
:
↑(sortSign (oddListOf (blockRestrict (ds W) (cSorted W (colouringOfFlip W F o ψ φ)) v))) * ↑(sortSign (F.oddListAt o φ (blockVertex W v))) = ↑(sortSign (List.map (fun (f : ↥F.flags) => sortKey W ↑f) (pairFlagList o (blockVertex W v))))
The per-vertex sign collapse: the block and Definition 5 sorting signs multiply to the key-sortSign of the pair enumeration.