Cook–Levin machines: reset all heads with linear runtime overhead
ProvedCookLevin.machine_all_heads_reset_linear_overheadcomplexity-theorycook-levinturing-machines
For every well-formed k-tape machine M there is a well-formed (k+1)-tape machine R over the same alphabet. For any initial tapes of length k with all heads at zero, whenever M halts within T with finalTps, R starts on those tapes plus a fresh blank clock and halts within 2*T+1 with exactly the original final tape contents, all heads reset to zero, and the blank clock restored at zero. No marker condition is required on any original tape, and their final cell-zero symbols may have been overwritten.
Preamble
import Definitions.Def_CookLevin_Cost open CookLevin set_option autoImplicit false
Formal statement
theorem CookLevin.machine_all_heads_reset_linear_overhead {k G : Nat} (M : Machine)
(hM : TuringMachine k G M) :
∃ R : Machine, TuringMachine (k + 1) G R ∧
∀ (tps finalTps : List Tape) (T : Nat),
tps.length = k →
(∀ tp ∈ tps, tp.2 = 0) →
Transforms M tps T finalTps →
Transforms R (tps ++ [(contents [], 0)]) (2 * T + 1)
(finalTps.map (fun tp => (tp.1, 0)) ++ [(contents [], 0)]) := by sorrySource
Direct clock simulation and bounded rewind proofs from CookLevin Basic/Cost, composed with the accepted machine_sequence_preserves_turing_and_time theorem. Developed for polynomial-time output concatenation in the SAT reduction.