Cook–Levin machines: acceptance-clause emission from a computable width
ProvedCookLevin.acceptClauseEmitter_of_unary_widtharithmeticcook-levinpolynomial-timeturing-machines
For arbitrary fixed tape count k, alphabet size G, and halting state Q, if a width w(x) is polynomial-time computable in unary, then the exact binary encoding of the two Cook-Levin acceptance clauses at width w(x) is polynomial-time computable. The clauses assert the halting state at time w(x) and the true symbol in cell one of the verdict tape at that time. The proof computes both packed literal indices as natural polynomials in the width, adds unary-number delimiters, and emits the exact clause/formula delimiters. No well-formedness restrictions on k, G, or Q are required for this syntactic emitter.
Preamble
import Definitions.Def_CookLevin_Tableau open CookLevin set_option autoImplicit false
Formal statement
theorem CookLevin.acceptClauseEmitter_of_unary_width (k G Q : Nat) (w : List Bool → Nat)
(hw : IsPolyTimeComputable (fun x => List.replicate (w x) true)) :
IsPolyTimeComputable (fun x => encodeFormula (acceptClauses ⟨k, G, Q, w x⟩)) := by sorrySource
CookLevin Tableau acceptance clauses and Satisfiability encoding, with polynomial evaluation and concatenation machine closures.