The cap pairing at the flipped colouring

Composing the diagonal cap evaluation, the flip's edge signs, the per-edge collapse, and the vertex odd-sign product: the cap pairing at the flipped data colouring is the crossing and representative parities times the Definition 5 odd signs.

theorem RS.betaDiag_colouringOfFlip {k ℓ : ℕ} (W : ClosedFragment) (F : EdgeSubset W) {κ : F.TransitionSystem} (o : κ.Orientation) (ψ : F.EvenColouring k) (φ : F.OddColouring ℓ) : betaDiag (edgeCount W) (colouringOfFlip W F o ψ φ) = (-1) ^ {p : Fin (edgeCount W) × Fin (edgeCount W) | p.1 < p.2 ∧ p.1 ∈ edgeIndexSet W F ∧ p.2 ∈ edgeIndexSet W F}.card * (-1) ^ inRepCount W F o * ∏ v : W.Vertex, ↑(F.oddSignAt o φ v)

The cap pairing at the flipped data colouring.