Polynomial-time emitter for acceptance clauses
ProvedCookLevin.acceptClauseEmitter_polyTimeclause-generationcook-levinpolynomial-timeturing-machine
For fixed tableau parameters, the encoded acceptance clauses of the Cook-Levin tableau can be emitted by a multi-tape Turing machine in time polynomial in the input length.
This isolates one concrete structural clause family from the nine-family aggregate and can be reused in modular tableau assembly.
Formal statement
import Definitions.Def_CookLevin_Reduction
open CookLevin
theorem CookLevin.acceptClauseEmitter_polyTime
(k G Q cw dw ct dt : Nat) :
IsPolyTimeComputable (fun x =>
encodeFormula (acceptClauses ⟨k, G, Q, tabWidth cw dw ct dt x⟩)) := by sorrySource
Decomposition of CookLevin.structuralClauseEmitters_polyTime: https://prove2.me/theorems/ea203338-20bc-4754-986a-bf8cb7ef70f8