Complete bounded enumeration of white faces

Least-position scans enumerate every white orbit exactly once. The resulting boundary lists partition the actual occurrence positions, even when source variables or constraint records repeat. All uses of choice below are proof-only; the compiler executes the bounded scans.

theorem Cslib.Complexity.CSP.CyclicCompiler.whiteRep_iff {Rel : Type} {F : Logic.PL.CSP Rel ℕ} (cert : Graph.RotationCertificate) (h : Graph.RotationCertificate.verifyRotation (incidenceGraph F) cert = true) (o : F.Occurrence) : Graph.RotationCertificate.faceRepBool F.occurrences.length (whiteTable F cert) (incidenceEdgeIndex o) = true ↔ ∀ (p : F.Occurrence), (whitePermutation (Graph.RotationCertificate.decode (incidenceGraph F) cert h)).SameCycle o p → incidenceEdgeIndex o ≤ incidenceEdgeIndex p

The finite representative test means least original occurrence position in that white orbit.

theorem Cslib.Complexity.CSP.CyclicCompiler.exists_whiteRep {Rel : Type} {F : Logic.PL.CSP Rel ℕ} (cert : Graph.RotationCertificate) (h : Graph.RotationCertificate.verifyRotation (incidenceGraph F) cert = true) (o : F.Occurrence) : ∃ (p : F.Occurrence), (whitePermutation (Graph.RotationCertificate.decode (incidenceGraph F) cert h)).SameCycle o p ∧ Graph.RotationCertificate.faceRepBool F.occurrences.length (whiteTable F cert) (incidenceEdgeIndex p) = true

Every actual occurrence has a least representative in its complete white orbit.

theorem Cslib.Complexity.CSP.CyclicCompiler.whiteRep_unique {Rel : Type} {F : Logic.PL.CSP Rel ℕ} (cert : Graph.RotationCertificate) (h : Graph.RotationCertificate.verifyRotation (incidenceGraph F) cert = true) (o p : F.Occurrence) (ho : Graph.RotationCertificate.faceRepBool F.occurrences.length (whiteTable F cert) (incidenceEdgeIndex o) = true) (hp : Graph.RotationCertificate.faceRepBool F.occurrences.length (whiteTable F cert) (incidenceEdgeIndex p) = true) (hcycle : (whitePermutation (Graph.RotationCertificate.decode (incidenceGraph F) cert h)).SameCycle o p) : o = p

Two accepted representatives in the same orbit have the same original edge position.

theorem Cslib.Complexity.CSP.CyclicCompiler.whiteScope_eq_of_sameCycle {Rel : Type} {F : Logic.PL.CSP Rel ℕ} (cert : Graph.RotationCertificate) (h : Graph.RotationCertificate.verifyRotation (incidenceGraph F) cert = true) (o p : F.Occurrence) (hcycle : (whitePermutation (Graph.RotationCertificate.decode (incidenceGraph F) cert h)).SameCycle o p) : whiteScope F cert (incidenceEdgeIndex o) = whiteScope F cert (incidenceEdgeIndex p)

Changing the representative within a white orbit leaves its complete sorted scope unchanged.

theorem Cslib.Complexity.CSP.CyclicCompiler.mem_flatten_whiteScopes {Rel : Type} {F : Logic.PL.CSP Rel ℕ} (cert : Graph.RotationCertificate) (h : Graph.RotationCertificate.verifyRotation (incidenceGraph F) cert = true) (v : ℕ) : v ∈ (whiteScopes F cert).flatten ↔ v < F.occurrences.length

The actual white lists cover every edge position and introduce no extra boundary name.

theorem Cslib.Complexity.CSP.CyclicCompiler.nodup_flatten_whiteScopes {Rel : Type} {F : Logic.PL.CSP Rel ℕ} (cert : Graph.RotationCertificate) (h : Graph.RotationCertificate.verifyRotation (incidenceGraph F) cert = true) : (whiteScopes F cert).flatten.Nodup

The complete flattened boundary enumeration is duplicate free.

theorem Cslib.Complexity.CSP.CyclicCompiler.count_flatten_whiteScopes {Rel : Type} {F : Logic.PL.CSP Rel ℕ} (cert : Graph.RotationCertificate) (h : Graph.RotationCertificate.verifyRotation (incidenceGraph F) cert = true) (v : ℕ) : List.count v (whiteScopes F cert).flatten = if v < F.occurrences.length then 1 else 0

Each actual edge occurs exactly once on the white side, with no spurious name.