Checked native cyclic-difference compiler specification

For each fixed finite Boolean language, the actual total compiler takes the original CSP and a supplied checked ordered numerical genus-zero rotation. In the self-complementary language branch with nonempty difference relations even delta-matroids, it outputs an explicit-table EDGE CSP over the existing infinite CSP.Table alphabet. Every output is well formed and every constraint is a nonempty even delta-matroid, including rejected raw inputs. Source indices stay binary; all construction loops traverse actual lists. Static language preprocessing may depend exponentially on fixed arity, as in Schaefer's fixed-language convention.

This numerical supplied-certificate stage implements the forward difference construction of [DK15], Section 3, Lemma 5/Corollary 4/Theorem 2, printed pp. 439–440, with the edge convention of [KKR18], v6, Definition 3 (printed p. 0:3). The parity-chain implementation is original. There is no geometric realization claim, bare rotation recognizer, edge solver assumption or full planar dichotomy claim.

Main results

• Cslib.Complexity.CSP.CyclicCompiler.compile_correct: full guarded semantic/edge/evenness result.
• Cslib.Complexity.CSP.CyclicCompiler.compile_spec: combined ordinary native endpoint.

theorem Cslib.Complexity.CSP.CyclicCompiler.count_vars_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) (v : ℕ) : List.count v (body arity sem F cert).vars = if v < F.occurrences.length + auxiliaryPrefix (whiteScopes F cert) (whiteScopes F cert).length then 2 else 0

Dense edge and auxiliary names have exactly two output occurrences. The auxiliary block starts at the original occurrence count and has its actual prefix-sum length.

theorem Cslib.Complexity.CSP.CyclicCompiler.edgeInstance_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) : (body arity sem F cert).EdgeInstance

Actual black and expanded-white scopes meet the positional edge convention. This uses only the checked original rotation, with no positivity or semantic assumption.

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

All-raw edge guarantee of the total compiler, including rejection.

theorem Cslib.Complexity.CSP.CyclicCompiler.body_tables {Rel : Type} {F : Logic.PL.CSP Rel ℕ} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (hdelta : ∀ (r : Rel), (Logic.PL.CSP.booleanRelation arity sem r).Nonempty → BitString.IsEvenDeltaMatroid (BitString.cyclicDifferenceRelation (Logic.PL.CSP.booleanRelation arity sem r))) (cert : Graph.RotationCertificate) (hwell : Logic.PL.CSP.WellFormed arity F) (hne : ∀ c ∈ F, nonemptySymbol arity sem c.1 = true) (constraint : Logic.PL.Constraint Logic.PL.CSP.Table ℕ) (hc : constraint ∈ body arity sem F cert) : constraint.1.arity = constraint.2.length ∧ BitString.IsEvenDeltaMatroid (Logic.PL.CSP.booleanRelation Logic.PL.CSP.Table.arity Logic.PL.CSP.Table.sem constraint.1)

Widths and actual explicit-table relations of the guarded body. Empty symbols need not satisfy the static delta-matroid condition; their occurring constraints are rejected first.

theorem Cslib.Complexity.CSP.CyclicCompiler.compile_tables {Rel : Type} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (hdelta : ∀ (r : Rel), (Logic.PL.CSP.booleanRelation arity sem r).Nonempty → BitString.IsEvenDeltaMatroid (BitString.cyclicDifferenceRelation (Logic.PL.CSP.booleanRelation arity sem r))) (input : Logic.PL.CSP Rel ℕ × Graph.RotationCertificate) (constraint : Logic.PL.Constraint Logic.PL.CSP.Table ℕ) : constraint ∈ compile arity sem input → constraint.1.arity = constraint.2.length ∧ BitString.IsEvenDeltaMatroid (Logic.PL.CSP.booleanRelation Logic.PL.CSP.Table.arity Logic.PL.CSP.Table.sem constraint.1)

Actual even delta-matroid constraints and matching table/scope widths on every raw input.

theorem Cslib.Complexity.CSP.CyclicCompiler.tableWellFormed_compile {Rel : Type} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (hdelta : ∀ (r : Rel), (Logic.PL.CSP.booleanRelation arity sem r).Nonempty → BitString.IsEvenDeltaMatroid (BitString.cyclicDifferenceRelation (Logic.PL.CSP.booleanRelation arity sem r))) (input : Logic.PL.CSP Rel ℕ × Graph.RotationCertificate) (constraint : Logic.PL.Constraint Logic.PL.CSP.Table ℕ) (hc : constraint ∈ compile arity sem input) : constraint.1.wellFormed = true

Every emitted explicit row has the declared width. Together with compile_tables, this also gives exact actual scope widths; no malformed table is used as a rejection shortcut.

theorem Cslib.Complexity.CSP.CyclicCompiler.compile_correct {Rel : Type} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (hself : ∀ (r : Rel), BitString.IsSelfComplementary (Logic.PL.CSP.booleanRelation arity sem r)) (hdelta : ∀ (r : Rel), (Logic.PL.CSP.booleanRelation arity sem r).Nonempty → BitString.IsEvenDeltaMatroid (BitString.cyclicDifferenceRelation (Logic.PL.CSP.booleanRelation arity sem r))) (input : Logic.PL.CSP Rel ℕ × Graph.RotationCertificate) : (compile arity sem input).EdgeInstance ∧ Logic.PL.CSP.WellFormed Logic.PL.CSP.Table.arity (compile arity sem input) ∧ Logic.PL.CSP.EdgeInstance.EvenConstraints 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 ↔ Logic.PL.CSP.Satisfiable Logic.PL.CSP.Table.sem (compile arity sem input))

Full guarded correctness of the actual total compiler on the original CSP/certificate. All translation, graph, lifting, nullary and expansion ingredients are proved internally.

theorem Cslib.Complexity.CSP.CyclicCompiler.compile_spec {Rel : Type} [Finite Rel] (encRel : Rel ↪ List Bool) (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (hself : ∀ (r : Rel), BitString.IsSelfComplementary (Logic.PL.CSP.booleanRelation arity sem r)) (hdelta : ∀ (r : Rel), (Logic.PL.CSP.booleanRelation arity sem r).Nonempty → BitString.IsEvenDeltaMatroid (BitString.cyclicDifferenceRelation (Logic.PL.CSP.booleanRelation arity sem r))) : Turing.MultiTapeTM.ComputableInPolyTime (compile arity sem) (encCSPRotationCertificate encRel Turing.MultiTapeTM.encNat) (encCSP encTable Turing.MultiTapeTM.encNat) ∧ ∀ (input : Logic.PL.CSP Rel ℕ × Graph.RotationCertificate), (compile arity sem input).EdgeInstance ∧ Logic.PL.CSP.WellFormed Logic.PL.CSP.Table.arity (compile arity sem input) ∧ Logic.PL.CSP.EdgeInstance.EvenConstraints 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 ↔ Logic.PL.CSP.Satisfiable Logic.PL.CSP.Table.sem (compile arity sem input))

Combined ordinary native fixed-language endpoint: no correct-translation certificate, solver/recognizer, geometric realization, or input-validity premise is a runtime assumption.