Cook–Levin machines: copy a terminated bit prefix in linear time

Proved

CookLevin.machine_copy_bit_prefix_linear_time

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

complexity-theorycook-levinturing-machines

For every tape count k >= 3 and alphabet G >= 4, a single well-formed machine copies any terminated bit prefix from tape one to tape two. Starting at arbitrary source and destination heads p and q, a string of n bits is copied in n+1 steps. The source contents, input tape, and all saved tapes remain unchanged. Both active heads advance by n. Destination cell q+j contains the corresponding bit for each j<n, and every destination cell outside [q,q+n) retains its original symbol. The theorem applies to arbitrary initial destination contents and requires only a non-bit terminator on the source.

Preamble

import Definitions.Def_CookLevin_Cost
open CookLevin
set_option autoImplicit false

Formal statement

theorem CookLevin.machine_copy_bit_prefix_linear_time {k G : Nat} (hk : 3 ≤ k) (hG : 4 ≤ G) :
    ∃ R : Machine, TuringMachine k G R ∧
      ∀ (bits : List Bool) (input : Tape) (f g : Nat → Symbol)
        (p q : Nat) (saved : List Tape),
        saved.length + 3 = k →
        (∀ j, (hj : j < bits.length) → f (p + j) = boolSym (bits[j])) →
        (¬ (f (p + bits.length) = zeroSymbol ∨ f (p + bits.length) = oneSymbol)) →
        ∃ out : Nat → Symbol,
          Transforms R (input :: (f, p) :: (g, q) :: saved) (bits.length + 1)
            (input :: (f, p + bits.length) :: (out, q + bits.length) :: saved) ∧
          (∀ j, (hj : j < bits.length) → out (q + j) = boolSym (bits[j])) ∧
          (∀ i, i < q ∨ q + bits.length ≤ i → out i = g i) := by sorry

Source

Direct proof from CookLevin Basic/Cost semantics, developed for output concatenation in the polynomial-time SAT reduction. One running state copies bits and halts on the first non-bit symbol.

View graph