The sign product of a flip sequence

The port signs of a sequence of chain flips, at the evolving colours: the closed form is a per-label product of the initial sign to the instance count times a triangular-number sign, so a sequence in which every label occurs evenly contributes exactly (−1)^length.

noncomputable def RS.flipColours {α : Type} {ℓ : ℕ} (f : α → Fin (2 * ℓ)) (p : α × α) : α → Fin (2 * ℓ)

The colour relabel of one flip.

Equations

• RS.flipColours f p a = if a = p.1 ∨ a = p.2 then RS.oddPartner ℓ (f a) else f a

noncomputable def RS.flipSignProd {α : Type} {ℓ : ℕ} (f : α → Fin (2 * ℓ)) : List (α × α) → ℤ

The accumulated port-sign product of a flip sequence, at the evolving colours.

Equations

• RS.flipSignProd f [] = 1
• RS.flipSignProd f (p :: L) = RS.oddPartnerSign ℓ (f p.1) * RS.oddPartnerSign ℓ (f p.2) * RS.flipSignProd (RS.flipColours f p) L

def RS.flipLabels {α : Type} (L : List (α × α)) : List α

The label instances of a flip sequence.

Equations

• RS.flipLabels L = List.flatMap (fun (p : α × α) => [p.1, p.2]) L

theorem RS.flipLabels_nil {α : Type} : flipLabels [] = []

No flips list no labels.

theorem RS.flipLabels_cons {α : Type} (p : α × α) (L : List (α × α)) : flipLabels (p :: L) = p.1 :: p.2 :: flipLabels L

One more flip lists its two labels first.

noncomputable def RS.oddCountLabels {α : Type} (L : List (α × α)) : Finset α

The labels with odd instance count.

Equations

• RS.oddCountLabels L = {a ∈ (RS.flipLabels L).toFinset | List.count a (RS.flipLabels L) % 2 = 1}

theorem RS.mem_oddCountLabels {α : Type} {L : List (α × α)} {a : α} : a ∈ oddCountLabels L ↔ List.count a (flipLabels L) % 2 = 1

A label counts as odd exactly when it occurs an odd number of times — the labels the fold has actually moved.