Executable checked cyclic-difference compiler

The input is the original list CSP and a supplied ordered numerical rotation certificate. Original variable names and certificate entries remain binary. Edge variables are dense actual occurrence positions. Every enumeration is funded by actual constraint/scope/occurrence lists. Static accepted-tuple and cyclic-difference tables depend only on the fixed language, with no uniform language-preprocessing claim. In particular, no solver or recognizer is a parameter.

Black constraints use the ordered cyclic-difference tables. White scopes are the complete orbits of B⁻¹ A⁻¹, enumerated by bounded scans in increasing edge-position order; their parity does not depend on the starting point or direction. Long white scopes use a width-three parity chain. Auxiliary blocks are consecutive and start immediately after the original occurrence positions. Nullaries have no edge variables: true nullaries are omitted, and false nullaries are rejected by the static relation-nonemptiness test. All malformed guards reject to two incompatible pins.

This is a numerical supplied-certificate implementation of the forward direction in [DK15], Section 3, Lemma 5/Corollary 4/Theorem 2, printed pp. 439–440. It asserts no geometric embedding construction, bare recognition, reverse reduction or solver. The bounded scans, parity-chain expansion and binary encoding implementation are original.

Main definitions

• Cslib.Complexity.CSP.CyclicCompiler.compile: total compiler on original raw typed inputs.

def Cslib.Complexity.CSP.CyclicCompiler.sourceRows {Rel : Type} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (r : Rel) : List (List Bool)

The fixed accepted source truth table, including the exact declared arity.

def Cslib.Complexity.CSP.CyclicCompiler.nonemptySymbol {Rel : Type} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (r : Rel) : Bool

Whether the canonical fixed relation has an accepted tuple. Empty symbols are rejected only when they actually occur in the instance.

def Cslib.Complexity.CSP.CyclicCompiler.argumentTable {Rel : Type} (F : Logic.PL.CSP Rel ℕ) : List ℕ

Constraint-side cyclic successor table, indexed by actual edge positions.

def Cslib.Complexity.CSP.CyclicCompiler.whiteTable {Rel : Type} (F : Logic.PL.CSP Rel ℕ) (cert : Graph.RotationCertificate) : List ℕ

White face successor B⁻¹ A⁻¹: invert the supplied variable rotation by scanning its actual list, then invert the actual cyclic argument successor list. Missing entries are total.

def Cslib.Complexity.CSP.CyclicCompiler.whiteScope {Rel : Type} (F : Logic.PL.CSP Rel ℕ) (cert : Graph.RotationCertificate) (edge : ℕ) : List ℕ

Complete boundary of one candidate white orbit, in increasing edge-position order. Repeated source vertices remain separate positions; parity is invariant under this enumeration.

def Cslib.Complexity.CSP.CyclicCompiler.whiteScopes {Rel : Type} (F : Logic.PL.CSP Rel ℕ) (cert : Graph.RotationCertificate) : List (List ℕ)

Keep exactly the least position of each white orbit, including singleton orbits.

def Cslib.Complexity.CSP.CyclicCompiler.blackScope {Rel : Type} (F : Logic.PL.CSP Rel ℕ) (index : ℕ) (scope : List ℕ) : List ℕ

Original cyclic scope order, with every argument replaced by its dense edge position.

def Cslib.Complexity.CSP.CyclicCompiler.blackConstraints {Rel : Type} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (F : Logic.PL.CSP Rel ℕ) : Logic.PL.CSP Logic.PL.CSP.Table ℕ

One static difference table per positive actual constraint position. True nullaries are handled by the outer nonemptiness guard and contribute no black dart orbit.

def Cslib.Complexity.CSP.CyclicCompiler.auxiliaryPrefix (scopes : List (List ℕ)) (index : ℕ) : ℕ

Fresh block prefix length. Only actual white boundary lists fund the allocated names.

def Cslib.Complexity.CSP.CyclicCompiler.whiteConstraints (edges : ℕ) (scopes : List (List ℕ)) : Logic.PL.CSP Logic.PL.CSP.Table ℕ

Each white face gets exactly its own consecutive auxiliary block.

def Cslib.Complexity.CSP.CyclicCompiler.body {Rel : Type} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (F : Logic.PL.CSP Rel ℕ) (cert : Graph.RotationCertificate) : Logic.PL.CSP Logic.PL.CSP.Table ℕ

Output body after the input guards. No interpretation of a quotient or choice is executed.

def Cslib.Complexity.CSP.CyclicCompiler.compile {Rel : Type} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (input : Logic.PL.CSP Rel ℕ × Graph.RotationCertificate) : Logic.PL.CSP Logic.PL.CSP.Table ℕ

Actual total compiler. Bad arity, invalid rotations and occurring empty relations reject honestly to an unsatisfiable edge instance whose two relations are even delta-matroids.

theorem Cslib.Complexity.CSP.CyclicCompiler.nonemptySymbol_eq_true_iff {Rel : Type} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (r : Rel) : nonemptySymbol arity sem r = true ↔ (Logic.PL.CSP.booleanRelation arity sem r).Nonempty

The static nonemptiness test is exactly nonemptiness of the canonical relation.

theorem Cslib.Complexity.CSP.CyclicCompiler.whiteScope_bounds {Rel : Type} (F : Logic.PL.CSP Rel ℕ) (cert : Graph.RotationCertificate) (edge : ℕ) : (whiteScope F cert edge).Nodup ∧ (whiteScope F cert edge).length ≤ F.occurrences.length ∧ ∀ j ∈ whiteScope F cert edge, j < F.occurrences.length

Every listed white boundary is distinct and bounded by the actual occurrence count, including for malformed certificates.

theorem Cslib.Complexity.CSP.CyclicCompiler.length_whiteScopes_le {Rel : Type} (F : Logic.PL.CSP Rel ℕ) (cert : Graph.RotationCertificate) : (whiteScopes F cert).length ≤ F.occurrences.length

No raw boundary scan emits more candidate white faces than original edges.