The riffle and orientation signs

The canonical index permutation from slot-order to edge-interleaved order has sign (−1)^C(n,2) (the riffle sign), and the permutation from edge-interleaved to oriented order has sign (−1)^s where s is the number of edges whose representative flag is outgoing.

Part 1 helpers: slot-map computations

Part 1 helpers: inversions of interleaved lists

Part 1 helpers: crossings count

Part 1: the riffle sign

theorem RS.sign_listIndexPerm_slot_edge (W : ClosedFragment) (F : EdgeSubset W) : ↑(Equiv.Perm.sign (listIndexPerm (globalSlotList W F) (edgePairList W F) ⋯ ⋯ ⋯ ⋯)) = (-1) ^ {p : Fin (edgeCount W) × Fin (edgeCount W) | p.1 < p.2 ∧ p.1 ∈ edgeIndexSet W F ∧ p.2 ∈ edgeIndexSet W F}.card

The riffle sign: the permutation from slot order to edge-interleaved order has sign (-1)^crossings.

Part 2 helpers: oriented list inversions

Part 2: the orientation sign

theorem RS.sign_listIndexPerm_edge_oriented (W : ClosedFragment) (F : EdgeSubset W) {κ : F.TransitionSystem} (o : κ.Orientation) : ↑(Equiv.Perm.sign (listIndexPerm (edgePairList W F) (orientedPairList W F o) ⋯ ⋯ ⋯ ⋯)) = (-1) ^ {i ∈ edgeIndexSet W F | o.isOut ((starFlagEnum W).symm (Fin.castAdd (edgeCount W) i)) = true}.card

The orientation sign: the permutation from edge-interleaved to oriented order has sign (-1)^s where s is the swap count.

Part 3: swap-count complement

theorem RS.card_out_add_card_in_edges (W : ClosedFragment) (F : EdgeSubset W) {κ : F.TransitionSystem} (o : κ.Orientation) : {i ∈ edgeIndexSet W F | o.isOut ((starFlagEnum W).symm (Fin.castAdd (edgeCount W) i)) = true}.card + inRepCount W F o = (edgeIndexSet W F).card

Every edge's representative is either outgoing or incoming, so the two counts partition the edges.