2.19. Checked Cyclic-Difference Edge Compilation🔗

Import CslibFrontier.Computability.PolyTime.CSP.CyclicDifference.Size. The actual compiler takes the original CSP and a supplied ordered numerical rotation certificate. The fixed language is self-complementary, and each nonempty relation has an even delta-matroid cyclic-difference image:

open Cslib.BitString Cslib.Logic.PL.CSP Cslib.Complexity
  Cslib.Complexity.CSP Cslib.Complexity.CSP.CyclicCompiler
  Turing.MultiTapeTM in
example {Rel : Type} [Finite Rel] (encRel : Rel ↪ List Bool)
    (arity : Rel → ℕ) (sem : Rel → List Bool → Bool)
    (hself : ∀ r, IsSelfComplementary (booleanRelation arity sem r))
    (hdelta : ∀ r, (booleanRelation arity sem r).Nonempty →
      IsEvenDeltaMatroid
        (cyclicDifferenceRelation (booleanRelation arity sem r))) :
    Turing.MultiTapeTM.ComputableInPolyTime (compile arity sem)
      (encCSPRotationCertificate encRel encNat)
      (encCSP encTable encNat) :=
  (compile_spec encRel arity sem hself hdelta).1

Cslib.Complexity.CSP.CyclicCompiler.compile_correct also guarantees an edge instance with exact widths and even constraints on every raw input. Target SAT is equivalent to source SAT together with the exact-arity and rotation checks. Empty symbols may occur in the language; their constraints, false nullaries and bad guards reject to two incompatible nonempty unary pins. True nullaries are handled internally. No positive-scope assumption is needed.

Long white boundaries expand to width-three parity chains. Output names are dense binary indices, independent of the magnitude of original names:

open Cslib.Logic.PL Cslib.Logic.PL.CSP Cslib.Complexity
  Cslib.Complexity.CSP.CyclicCompiler in
example {Rel : Type} (arity : Rel → ℕ)
    (sem : Rel → List Bool → Bool)
    (input : CSP Rel ℕ × Graph.RotationCertificate) :
    (compile arity sem input).vars.length ≤
      4 * input.1.occurrences.length + 2 :=
  length_vars_compile_le arity sem input

There are at most C+M+2 constraints and names below 2M+1, for actual source constraint/occurrence counts C,M. The input encoding frames the CSP before the binary successor certificate; the output includes all explicit rows, binary arities/names and list/pair framing. Cslib.Complexity.CSP.CyclicCompiler.polyBounded_length_compile bounds the complete encoded output. Fixed-language preprocessing can depend exponentially on fixed arity. Runtime has no input-validity premise.

CslibFrontierTests/CSPCyclicCompiler.lean gives concrete SAT/UNSAT NAE runs, long chains, nullaries, repeated arguments, bad guards and huge binary labels. This proves the supplied numerical-certificate compiler stage, without a bare recognizer, geometric correspondence or full planar dichotomy. The edge solver is below.