Polynomial-time fixed Boolean CSP syntax checks

The exact-arity guard is native polynomial-time for every fixed finite relation alphabet. The fixed arity table uses unary values; instance variable labels retain their binary encoding. This certificate is shared by satisfiability reductions and primitive-positive replacement.

Main results

• Cslib.Complexity.CSP.computableInPolyTime_validArity: native polynomial-time arity checking.

theorem Cslib.Complexity.CSP.computableInPolyTime_validArity {Rel : Type} [Finite Rel] (encRel : Rel ↪ List Bool) (arity : Rel → ℕ) : Turing.MultiTapeTM.ComputableInPolyTime (Logic.PL.CSP.validArity arity) (encCSP encRel Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encBool

The exact-arity guard is polynomial-time for each fixed finite relation alphabet.