Polynomial-time instantiation of fixed affine templates

The finite relation alphabet and its local affine systems are fixed independently of the input. Local positions use unary encoding for list lookup. Original variable labels use binary encoding throughout; no array indexed by their numerical values is constructed. Each fixed template lookup, substitution and concatenation has a native multi-tape polynomial-time certificate.

Main results

• Cslib.Complexity.CSP.computableInPolyTime_instantiateAffine: polynomial template compilation.

theorem Cslib.Complexity.CSP.computableInPolyTime_instantiateAffine {Rel : Type} [Finite Rel] (encRel : Rel ↪ List Bool) (template : Rel → Logic.PL.AffineSystem ℕ) : Turing.MultiTapeTM.ComputableInPolyTime (Logic.PL.CSP.instantiateAffine 0 template) (encCSP encRel Turing.MultiTapeTM.encNat) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encBool))

Fixed affine systems can be instantiated in native polynomial time, with unary local positions and binary original variable labels. The bound may depend on the fixed language.