Cook–Levin machine model: reset input with linear runtime overhead
ProvedCookLevin.machine_input_reset_linear_overheadcomplexity-theorycook-levinturing-machines
For every well-formed k-tape machine M there is a well-formed machine R on the same tapes and alphabet that performs M and then returns the input head to cell zero. For any Boolean input and any initial work tapes of the correct count, if M halts within T steps with final tapes, R halts within 2*T+1 steps with the original input restored at head zero and exactly the same final work tapes and work-tape head positions. The proof derives input preservation and the input head displacement bound from the actual machine semantics; neither is assumed as an extra premise.
Preamble
import Definitions.Def_CookLevin_Cost open CookLevin set_option autoImplicit false
Formal statement
theorem CookLevin.machine_input_reset_linear_overhead {k G : Nat} (M : Machine)
(hM : TuringMachine k G M) :
∃ R : Machine, TuringMachine k G R ∧
∀ (x : List Bool) (work finalTps : List Tape) (T : Nat),
work.length + 1 = k →
Transforms M ((contents (boolsToSymbols x), 0) :: work) T finalTps →
Transforms R ((contents (boolsToSymbols x), 0) :: work) (2 * T + 1)
((contents (boolsToSymbols x), 0) :: finalTps.tail) := by sorrySource
The CookLevin Basic and Cost semantics plus the accepted machine_sequence_preserves_turing_and_time theorem. A one-command rewind scans left to the unique start marker on the preserved bit-input tape.