Product of odd signs over vertices equals product over outgoing flags

Helpers

Step 1: oddSignAt as a Finset product

Step 2: product over vertices, then swap and collapse

Step 3: incoming to subtype, then reindex

theorem RS.prod_oddSignAt {α : Type} {W : Fragment α} {F : EdgeSubset W} {ℓ : ℕ} {κ : F.TransitionSystem} (o : κ.Orientation) (φ : F.OddColouring ℓ) : ∏ v : W.Vertex, F.oddSignAt o φ v = ∏ f : ↥F.flags, if o.isOut ↑f = true then oddPartnerSign ℓ (↑φ f) else 1

Main theorem: the product over vertices of the Definition-5 odd signs is the product of partner signs over the outgoing participating flags.