Actual white-successor table and the polygon rotation

All semantic permutations here are derived from the decoded checked incidence rotation. The executed compiler continues to use finite tables and bounded scans, not these proof-only permutations. Nullaries remain indexed original constraint positions and add no darts.

theorem Cslib.Complexity.CSP.CyclicCompiler.getD_argumentTable {Rel : Type} {F : Logic.PL.CSP Rel ℕ} (o : F.Occurrence) : (argumentTable F).getD (incidenceEdgeIndex o) 0 = incidenceEdgeIndex ((argumentPermutation F) o)

Reading the argument table at an actual occurrence gives its actual cyclic successor.

theorem Cslib.Complexity.CSP.CyclicCompiler.argumentTable_nodup {Rel : Type} (F : Logic.PL.CSP Rel ℕ) : (argumentTable F).Nodup

The argument successor table is a permutation of actual occurrence positions.

theorem Cslib.Complexity.CSP.CyclicCompiler.idxOf_argumentTable {Rel : Type} {F : Logic.PL.CSP Rel ℕ} (o : F.Occurrence) : List.idxOf (incidenceEdgeIndex o) (argumentTable F) = incidenceEdgeIndex ((Equiv.symm (argumentPermutation F)) o)

Bounded inverse scan computes the actual previous argument edge, including singleton scopes.

theorem Cslib.Complexity.CSP.CyclicCompiler.idxOf_variable {Rel : Type} {F : Logic.PL.CSP Rel ℕ} (cert : Graph.RotationCertificate) (h : Graph.RotationCertificate.verifyRotation (incidenceGraph F) cert = true) (o : F.Occurrence) : List.idxOf (2 * incidenceEdgeIndex o) cert.successor = 2 * incidenceEdgeIndex ((Equiv.symm (variablePermutation (Graph.RotationCertificate.decode (incidenceGraph F) cert h))) o)

Inverting the supplied successor list at an actual variable end recovers precisely the inverse variable permutation of the decoded rotation; no supplied inverse is trusted.

theorem Cslib.Complexity.CSP.CyclicCompiler.getD_whiteTable {Rel : Type} {F : Logic.PL.CSP Rel ℕ} (cert : Graph.RotationCertificate) (h : Graph.RotationCertificate.verifyRotation (incidenceGraph F) cert = true) (o : F.Occurrence) : (whiteTable F cert).getD (incidenceEdgeIndex o) 0 = incidenceEdgeIndex ((Equiv.symm (argumentPermutation F)) ((Equiv.symm (variablePermutation (Graph.RotationCertificate.decode (incidenceGraph F) cert h))) o))

The executed white table is exactly the polygon's backward-dart face successor.

noncomputable def Cslib.Complexity.CSP.CyclicCompiler.whitePermutation {Rel : Type} {F : Logic.PL.CSP Rel ℕ} (r : (incidenceGraph F).RotationSystem) : Equiv.Perm F.Occurrence

The white permutation is derived from the actual variable and argument rotations.

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

Bounded white scans use precisely one clock unit per actual occurrence, including fixed points of the permutation.

theorem Cslib.Complexity.CSP.CyclicCompiler.sameCycle_white_iff {Rel : Type} {F : Logic.PL.CSP Rel ℕ} (r : (incidenceGraph F).RotationSystem) (o p : F.Occurrence) : (whitePermutation r).SameCycle o p ↔ (polygonRotation r).faceNext.SameCycle (polygonDart o true) (polygonDart p true)

The white orbit scan is the actual face orbit on backward polygon darts.

theorem Cslib.Complexity.CSP.CyclicCompiler.sameCycle_black_iff {Rel : Type} {F : Logic.PL.CSP Rel ℕ} (r : (incidenceGraph F).RotationSystem) (o p : F.Occurrence) : (polygonRotation r).faceNext.SameCycle (polygonDart o false) (polygonDart p false) ↔ o.fst = p.fst

The black orbit is the original indexed constraint position.

theorem Cslib.Complexity.CSP.CyclicCompiler.sameCycle_polygon_side {Rel : Type} {F : Logic.PL.CSP Rel ℕ} (r : (incidenceGraph F).RotationSystem) (d e : (polygonGraph F).Dart) (h : (polygonRotation r).faceNext.SameCycle d e) : d.2 = e.2

A polygon face cannot change its black/white endpoint side.