Cook–Levin machines: polynomial-time unary input-length counter
ProvedCookLevin.polyTime_input_length_unarycook-levinpolynomial-timeturing-machines
The function x ↦ List.replicate x.length true is polynomial-time computable in the actual CookLevin multitape-machine model. The proof constructs a two-tape four-symbol machine with |x|+2 steps and absorbs that runtime into 2*(|x|+1). This provides a length counter for later tableau-width arithmetic; it does not by itself prove clause emission or the Cook–Levin reduction.
Preamble
import Definitions.Def_CookLevin_Complexity open CookLevin set_option autoImplicit false
Formal statement
theorem CookLevin.polyTime_input_length_unary :
IsPolyTimeComputable (fun x => List.replicate x.length true) := by sorrySource
Direct construction in the CookLevin Basic/Cost machine semantics; unary-length specialization is intended for tableau-emitter arithmetic.