Cook–Levin machines: unary-controlled repetition and runtime
ProvedCookLevin.machine_repeat_unary_preserves_turing_and_timecomplexitycook-levinloopsturing-machines
A well-formed multitape Turing-machine body can be repeated once per symbol of a terminated unary prefix on any chosen tape. The body preserves that source tape and its head; the loop advances its head one cell after each iteration. The source can start at any cell and has arbitrary contents outside the unary prefix. For n body executions bounded by T each, the full loop halts within n*(T+3)+1 steps, preserving the source contents and producing the exact final spectator tapes specified by the body trace. No extra tapes are introduced.
Preamble
import Definitions.Def_CookLevin_Complexity open CookLevin set_option autoImplicit false
Formal statement
theorem CookLevin.machine_repeat_unary_preserves_turing_and_time {k G : Nat}
(j : Nat) (body : Machine) (hbody : TuringMachine k G body) :
∃ R : Machine, TuringMachine k G R ∧
∀ (n T p : Nat) (g : Nat → Symbol) (left right : Nat → List Tape),
(∀ i, i ≤ n → (left i).length = j) →
(∀ i, i < n → g (p + i) = oneSymbol) →
g (p + n) ≠ oneSymbol →
(∀ i, i < n → Transforms body
(left i ++ (g, p + i) :: right i) T
(left (i + 1) ++ (g, p + i) :: right (i + 1))) →
Transforms R (left 0 ++ (g, p) :: right 0) (n * (T + 3) + 1)
(left n ++ (g, p + n) :: right n) := by sorrySource
A write-back command advances only the selected tape head. Accepted sequential and guarded-loop constructors then realize unary-controlled repetition.