Cook–Levin machines: append a unary counter and restore its head

Proved

CookLevin.machine_append_unary_restore_source

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

complexitycook-levinloopsturing-machines

A three-state multitape Turing machine appends a unary source counter of length n to an existing binary output prefix in 2*n+3 steps. The source head begins and ends on the terminator at cell 1+n; the source contents, input tape, and every spectator tape remain unchanged. The resulting destination is exactly the standard encoding of the original output followed by n ones, including its marker and blank tail. The source has a non-one at zero, n ones from cell one, and a non-one terminator; symbols beyond that terminator are unrestricted.

Preamble

import Definitions.Def_CookLevin_Complexity
open CookLevin
set_option autoImplicit false

Formal statement

theorem CookLevin.machine_append_unary_restore_source {k G : Nat} (hk : 3 ≤ k) (hG : 4 ≤ G) :
    ∃ R : Machine, TuringMachine k G R ∧
      ∀ (n : Nat) (bits : List Bool) (input : Tape) (f : Nat → Symbol) (saved : List Tape),
        saved.length + 3 = k →
        f 0 ≠ oneSymbol →
        (∀ i, i < n → f (1 + i) = oneSymbol) →
        f (1 + n) ≠ oneSymbol →
        Transforms R
          (input :: (f, 1 + n) :: (contents (boolsToSymbols bits), 1 + bits.length) :: saved)
          (2 * n + 3)
          (input :: (f, 1 + n) ::
            (contents (boolsToSymbols (bits ++ List.replicate n true)), 1 + bits.length + n) :: saved) := by sorry

Source

A three-state machine steps left from the source terminator, copies ones while scanning backward, then scans forward to restore the source head.

View graph