The regroup sign

The extraction enumerates a subset's participating flags three ways: oriented, each edge's representative followed by its pairing partner; matched, each incoming flag followed by its match; and global, the per-vertex pair blocks concatenated. The sign relating them is the regroup sign, and this module computes it in two halves.

• Oriented to matched (sign_listIndexPerm_oriented_matched) conjugates the out-permutation: the index permutation between the two enumerations acts on edge indices exactly as the orientation's out-permutation acts on flags, so the two signs agree.
• Matched to global (sign_listIndexPerm_matched_global) is even: both enumerations list the same incoming flags each followed by its match, so the index permutation moves whole two-element blocks and its sign is a square.

Both run on the flat-map presentations of the three lists and on the index arithmetic of a list of pairs.

Slot extraction from block membership

Slot contradiction helper

Nodup: matched pair list

theorem RS.matchedPairList_nodup' (W : ClosedFragment) (F : EdgeSubset W) {κ : F.TransitionSystem} (o : κ.Orientation) : (matchedPairList W F o).Nodup

The matched pair list has no repeats.

Membership: matched pair list

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

And lists every participating flag — so it is a reordering of them, and its sign is the regroup sign.

Nodup and membership: global pair list

Length equalities

Match subtype and base lists

FlatMap decompositions

Pairing properties

Orientation properties of base elements

Nodup getElem? injection

pairBlowup and sign

Half 1 infrastructure

Half 1: sign of oriented → matched = sign of outPerm

theorem RS.sign_listIndexPerm_oriented_matched (W : ClosedFragment) (F : EdgeSubset W) {κ : F.TransitionSystem} (o : κ.Orientation) : Equiv.Perm.sign (listIndexPerm (orientedPairList W F o) (matchedPairList W F o) ⋯ ⋯ ⋯ ⋯) = Equiv.Perm.sign (κ.outPerm o)

Half 1: the sign of the index permutation from oriented to matched equals the sign of the out-permutation.

Half 2: sign of matched → global = 1

theorem RS.sign_listIndexPerm_matched_global (W : ClosedFragment) (F : EdgeSubset W) {κ : F.TransitionSystem} (o : κ.Orientation) : Equiv.Perm.sign (listIndexPerm (matchedPairList W F o) (globalPairList W F o) ⋯ ⋯ ⋯ ⋯) = 1

Half 2: the sign of the index permutation from matched to global pair list is +1.