Cook–Levin machines: indexed unary iteration and runtime

Proved

CookLevin.machine_repeat_unary_indexed_preserves_turing_and_time

by Robertboy18 · Sep 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

complexitycook-levinloopsturing-machines

A well-formed multitape Turing-machine body can iterate over a terminated unary source while a separate adjacent tape holds the current index in unary. Before iteration i the index contains exactly i ones, with its head at cell 1+i. The body preserves both counter tapes; a single command advances the source head and extends the index by one. A source prefix of n ones followed by a non-one gives exactly n body iterations, a final unary index n, and runtime at most n*(T+3)+1 when each body run is bounded by T. All other tapes have precisely the final contents and head positions specified by the body trace.

Preamble

import Definitions.Def_CookLevin_Complexity
open CookLevin
set_option autoImplicit false

Formal statement

theorem CookLevin.machine_repeat_unary_indexed_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) :: (contents (List.replicate i oneSymbol), 1 + i) :: right i) T
          (left (i + 1) ++ (g, p + i) ::
            (contents (List.replicate i oneSymbol), 1 + i) :: right (i + 1))) →
        Transforms R (left 0 ++ (g, p) :: (contents [], 1) :: right 0)
          (n * (T + 3) + 1)
          (left n ++ (g, p + n) :: (contents (List.replicate n oneSymbol), 1 + n) :: right n) := by sorry

Source

An alphabet-safe command advances the source and increments an adjacent unary index in one step. Accepted sequential and guarded-loop constructors realize the indexed iteration.

View graph