Cook–Levin machines: linear-time mapping of input bits

Proved

CookLevin.computesInTime_map_bits

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

cook-levinpolynomial-timeturing-machines

For every Boolean map h, a fixed well-formed two-tape machine over four symbols computes x.map h within |x|+2 steps. One initial step skips the markers, each input bit is read and its mapped bit written in one step, and a non-bit input terminator halts the machine. The proof checks the whole destination tape and final decoding while preserving input contents.

Preamble

import Definitions.Def_CookLevin_Complexity
open CookLevin
set_option autoImplicit false

Formal statement

theorem CookLevin.computesInTime_map_bits (h : Bool → Bool) :
    ∃ M : Machine, TuringMachine 2 4 M ∧
      ComputesInTime M 2 (fun n => n + 2) (fun x => x.map h) := by sorry

Source

Direct construction in the CookLevin Basic/Cost machine semantics; unary-length specialization is intended for tableau-emitter arithmetic.

View graph