Semantic correctness of the actual difference compiler

The source predicate keeps well-formedness, the supplied checked ordered numerical rotation, and original CSP satisfiability. Vertex spins are obtained from the reviewed numerical lifting theorem on the actual polygon graph. Nullaries are handled internally without changing source indices, and no translation, geometric realization, solver or inverse-table oracle is supplied.

theorem Cslib.Complexity.CSP.CyclicCompiler.eval_blackConstraints_iff {Rel : Type} {F : Logic.PL.CSP Rel ℕ} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (σ : ℕ → Bool) : Logic.PL.CSP.eval Logic.PL.CSP.Table.sem σ (blackConstraints arity sem F) = true ↔ ∀ (i : Fin (List.length F)), 0 < F[↑i].2.length → (Logic.PL.CSP.Table.differenceTable arity sem F[↑i].1).sem (List.map σ (blackScope F (↑i) F[↑i].2)) = true

Evaluation of the actual indexed black-constraint list.

def Cslib.Complexity.CSP.CyclicCompiler.spinTuple {Rel : Type} (F : Logic.PL.CSP Rel ℕ) (spin : ℕ → Bool) (i : Fin (List.length F)) : Fin F[↑i].2.length → Bool

Original variable spins read in the actual scope order.

theorem Cslib.Complexity.CSP.CyclicCompiler.gradient_blackScope {Rel : Type} {F : Logic.PL.CSP Rel ℕ} (spin σ : ℕ → Bool) (he : ∀ (o : F.Occurrence), σ (incidenceEdgeIndex o) = (polygonGraph F).edgeGradient spin (polygonDart o false).1) (i : Fin (List.length F)) : List.map σ (blackScope F (↑i) F[↑i].2) = List.ofFn (BitString.cyclicDifference (spinTuple F spin i))

Local gradient tuples are exactly ordered cyclic differences, even with repeated names.

theorem Cslib.Complexity.CSP.CyclicCompiler.sem_nullary_of_nonempty {Rel : Type} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (r : Rel) (hwidth : arity r = 0) (hne : (Logic.PL.CSP.booleanRelation arity sem r).Nonempty) : sem r [] = true

A true canonical nullary relation accepts the empty row. Nonemptiness suffices because there is only one tuple of arity zero.

theorem Cslib.Complexity.CSP.CyclicCompiler.faceEven_of_body {Rel : Type} {F : Logic.PL.CSP Rel ℕ} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (cert : Graph.RotationCertificate) (h : Graph.RotationCertificate.verifyRotation (incidenceGraph F) cert = true) (σ : ℕ → Bool) (hsat : Logic.PL.CSP.eval Logic.PL.CSP.Table.sem σ (body arity sem F cert) = true) : (polygonRotation (Graph.RotationCertificate.decode (incidenceGraph F) cert h)).FaceEven fun (i : Fin (polygonGraph F).edges.length) => σ ↑i

A black-and-expanded-white satisfying assignment is face-even on the actual polygon.

theorem Cslib.Complexity.CSP.CyclicCompiler.ofFn_spinTuple {Rel : Type} {F : Logic.PL.CSP Rel ℕ} (spin : ℕ → Bool) (i : Fin (List.length F)) : List.ofFn (spinTuple F spin i) = List.map (fun (v : ℕ) => spin (List.idxOf v F.distinctVars)) F[↑i].2

Scope tuples agree with the original CSP evaluator after dense spin reconstruction.

theorem Cslib.Complexity.CSP.CyclicCompiler.satisfiable_source_of_body {Rel : Type} {F : Logic.PL.CSP Rel ℕ} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (hself : ∀ (r : Rel), BitString.IsSelfComplementary (Logic.PL.CSP.booleanRelation arity sem r)) (cert : Graph.RotationCertificate) (hwell : Logic.PL.CSP.WellFormed arity F) (hcert : verifyRotationCertificate F cert = true) (hnonempty : ∀ c ∈ F, nonemptySymbol arity sem c.1 = true) (hsat : Logic.PL.CSP.Satisfiable Logic.PL.CSP.Table.sem (body arity sem F cert)) : Logic.PL.CSP.Satisfiable sem F

Accepted expanded output lifts back to the original source under its checked rotation. Empty occurring relations are excluded by the actual compiler guard, including false nullaries.

theorem Cslib.Complexity.CSP.CyclicCompiler.satisfiable_body_of_source {Rel : Type} {F : Logic.PL.CSP Rel ℕ} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (hself : ∀ (r : Rel), BitString.IsSelfComplementary (Logic.PL.CSP.booleanRelation arity sem r)) (cert : Graph.RotationCertificate) (hwell : Logic.PL.CSP.WellFormed arity F) (hcert : verifyRotationCertificate F cert = true) (hsat : Logic.PL.CSP.Satisfiable sem F) : Logic.PL.CSP.Satisfiable Logic.PL.CSP.Table.sem (body arity sem F cert)

Every source solution gives a solution of the actual expanded body. Difference tables are static; white parity follows from telescoping on the actual polygon rotation.

theorem Cslib.Complexity.CSP.CyclicCompiler.nonemptySymbol_of_satisfiable {Rel : Type} {F : Logic.PL.CSP Rel ℕ} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (hwell : Logic.PL.CSP.WellFormed arity F) (hsat : Logic.PL.CSP.Satisfiable sem F) (c : Logic.PL.Constraint Rel ℕ) : c ∈ F → nonemptySymbol arity sem c.1 = true

Satisfying well-formed source instances pass the occurring-relation nonemptiness guard. This includes true nullaries, and does not require every language symbol to be nonempty.

theorem Cslib.Complexity.CSP.CyclicCompiler.satisfiable_compile_iff {Rel : Type} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (hself : ∀ (r : Rel), BitString.IsSelfComplementary (Logic.PL.CSP.booleanRelation arity sem r)) (input : Logic.PL.CSP Rel ℕ × Graph.RotationCertificate) : Logic.PL.CSP.Satisfiable Logic.PL.CSP.Table.sem (compile arity sem input) ↔ Logic.PL.CSP.WellFormed arity input.1 ∧ verifyRotationCertificate input.1 input.2 = true ∧ Logic.PL.CSP.Satisfiable sem input.1

Full guarded semantic correctness on the original CSP and supplied certificate. The only language assumption is simultaneous self-complementarity. All graph translation, nullary, face-lifting and parity-chain obligations are discharged internally.