Cook–Levin machine model: tape padding with unchanged runtime

Proved

CookLevin.machine_tape_padding_preserves_turing_and_time

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

complexity-theorycook-levinturing-machines

Any well-formed k-tape machine can run on k+n tapes by reading its original first k tapes and writing back the symbols on the remaining tapes without moving their heads. The explicit padded command list preserves the alphabet and input-tape restrictions. Every bounded transformation of the original tapes remains valid with the same runtime bound, while all extra tape contents and head positions remain unchanged. This provides tape-count alignment for later composition; it does not relocate the designated output tape or establish general string concatenation.

Preamble

import Definitions.Def_CookLevin_Basic
open CookLevin
set_option autoImplicit false

Formal statement

theorem CookLevin.machine_tape_padding_preserves_turing_and_time
    {k G : Nat} (M : Machine) (hM : TuringMachine k G M) (n : Nat) :
    let padded : Machine := M.map (fun cmd gs =>
      ((cmd (gs.take k)).1,
        (cmd (gs.take k)).2 ++ (gs.drop k).map (fun g => (g, Direction.Stay))))
    TuringMachine (k + n) G padded ∧
      ∀ (tps finalTps extra : List Tape) (T : Nat),
        tps.length = k → extra.length = n →
        Transforms M tps T finalTps →
        Transforms padded (tps ++ extra) T (finalTps ++ extra) := by sorry

Source

Direct simulation of the existing CookLevin Basic machine semantics, developed for the polynomial-time reduction milestone.

View graph