Parity of the actual compiled black and white scopes

Finite sums retain each indexed edge/dart occurrence. White scopes may be listed in increasing position order because parity is commutative; black scopes retain the original argument order.

theorem Cslib.Complexity.CSP.CyclicCompiler.blackScope_eq_ofFn {Rel : Type} {F : Logic.PL.CSP Rel ℕ} (i : Fin (List.length F)) : blackScope F (↑i) F[↑i].2 = List.ofFn fun (j : Fin F[↑i].2.length) => incidenceEdgeIndex ⟨i, j⟩

Exact original ordered scope after replacing its ports by indexed edge positions.

theorem Cslib.Complexity.CSP.CyclicCompiler.blackScope_bounds {Rel : Type} {F : Logic.PL.CSP Rel ℕ} (i : Fin (List.length F)) : (blackScope F (↑i) F[↑i].2).Nodup ∧ ∀ v ∈ blackScope F (↑i) F[↑i].2, v < F.occurrences.length

Names in a black scope are distinct actual edge positions.

theorem Cslib.Complexity.CSP.CyclicCompiler.faceParity_black {Rel : Type} {F : Logic.PL.CSP Rel ℕ} (r : (incidenceGraph F).RotationSystem) (σ : ℕ → Bool) (o : F.Occurrence) : (polygonRotation r).faceParity (fun (i : Fin (polygonGraph F).edges.length) => σ ↑i) ⟦polygonDart o false⟧ = BitString.wordParity (List.map σ (blackScope F (↑o.fst) F[↑o.fst].2))

Black face parity is exactly parity of its original cyclic scope.

theorem Cslib.Complexity.CSP.CyclicCompiler.faceParity_white {Rel : Type} {F : Logic.PL.CSP Rel ℕ} (cert : Graph.RotationCertificate) (h : Graph.RotationCertificate.verifyRotation (incidenceGraph F) cert = true) (σ : ℕ → Bool) (o : F.Occurrence) : (polygonRotation (Graph.RotationCertificate.decode (incidenceGraph F) cert h)).faceParity (fun (i : Fin (polygonGraph F).edges.length) => σ ↑i) ⟦polygonDart o true⟧ = BitString.wordParity (List.map σ (whiteScope F cert (incidenceEdgeIndex o)))

White face parity is exactly parity of the complete executable boundary scan.