Cook–Levin machines: canonicalize a computed bit output

Proved

CookLevin.machine_copy_bits_from_zero

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

complexitycook-levinloopsturing-machines

One well-formed machine copies an arbitrary terminated bit prefix into a fresh canonical output tape. Both heads start at zero and finish at one plus the bit length. Runtime is at most bit length plus three. The source contents, input tape, and spectator tapes are preserved; no assumption is made about source contents beyond the terminator.

Preamble

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

Formal statement

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

Source

Advance the two work-tape heads and apply the accepted prefix copier. Its pointwise output guarantees determine the entire canonical tape.

View graph