Per-edge factoring of the out-sign product

The subtype product of odd-partner signs over outgoing participating flags equals the edge-indexed product: each participating edge contributes the sign of its (pairing-constant) colour exactly once, and non-participating edges contribute 1 on both sides.

theorem RS.prod_out_sign_eq_prod_edges (W : ClosedFragment) (F : EdgeSubset W) {ℓ : ℕ} {κ : F.TransitionSystem} (o : κ.Orientation) (φ : F.OddColouring ℓ) : (∏ f : ↥F.flags, if o.isOut ↑f = true then oddPartnerSign ℓ (↑φ f) else 1) = ∏ i : Fin (edgeCount W), if h : (starFlagEnum W).symm (Fin.castAdd (edgeCount W) i) ∈ F.flags then oddPartnerSign ℓ (↑φ ⟨(starFlagEnum W).symm (Fin.castAdd (edgeCount W) i), h⟩) else 1

Each participating edge has exactly one outgoing flag; the subtype product of odd-partner signs equals the edge-indexed product.