Cook–Levin machines: seek the end of a unary counter

Proved

CookLevin.machine_seek_unary_end

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

complexitycook-levinloopsturing-machines

A single well-formed machine moves a selected head from cell zero to the first non-one symbol after a unary prefix of length n, in at most 3*n+2 steps. It preserves all tape contents and every other head. The selected index is arbitrary, and the contents beyond the terminator are unrestricted.

Preamble

import Definitions.Def_CookLevin_Tableau
import Definitions.Def_CookLevin_Complexity
open CookLevin
set_option autoImplicit false

Formal statement

theorem CookLevin.machine_seek_unary_end {k G : Nat} (hk : 2 ≤ k) (hG : 4 ≤ G) (j : Nat) :
    ∃ R : Machine, TuringMachine k G R ∧
      ∀ (n : Nat) (f : Nat → Symbol) (left right : List Tape),
        left.length = j →
        (∀ i, i < n → f (1 + i) = oneSymbol) →
        f (1 + n) ≠ oneSymbol →
        Transforms R (left ++ (f, 0) :: right) (3 * n + 2)
          (left ++ (f, 1 + n) :: right) := by sorry

Source

Advance the chosen head once, then use unary repetition with an empty body.

View graph