The core and grand parities

The two parity counts the extraction's sign bookkeeping rests on: the parity of the core slots' pairing and the parity of the whole slot list.

theorem RS.core_parity (W : ClosedFragment) (F : EdgeSubset W) {κ : F.TransitionSystem} (o : κ.Orientation) : (-1) ^ patternOddInv 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 * (-1) ^ inRepCount W F o) * ∏ v : Fin (ds W).length, ↑(sortSign (List.map (fun (f : ↥F.flags) => sortKey W ↑f) (pairFlagList o (blockVertex W v)))) = (-1) ^ κ.circuitCount

The core parity identity: the pattern, crossing and representative signs against the pair-enumeration key signs compose to the circuit and outgoing signs.

theorem RS.grand_parity {k ℓ : ℕ} (W : ClosedFragment) (F : EdgeSubset W) {κ : F.TransitionSystem} (o : κ.Orientation) (ψ : F.EvenColouring k) (φ : F.OddColouring ℓ) (hnd : ∀ (v : Fin (ds W).length), (F.oddListAt o φ (blockVertex W v)).Nodup) : (-1) ^ patternOddInv 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 * (-1) ^ inRepCount W F o) * ∏ v : Fin (ds W).length, ↑(sortSign (oddListOf (blockRestrict (ds W) (cSorted W (colouringOfFlip W F o ψ φ)) v))) * ↑(sortSign (F.oddListAt o φ (blockVertex W v))) = (-1) ^ κ.circuitCount

The grand parity identity: the pattern, crossing, representative and per-vertex sorting signs compose to the circuit sign.