Cook–Levin machines: guarded loop composition and runtime

Proved

CookLevin.machine_guarded_loop_preserves_turing_and_time

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

complexitycook-levinloopsturing-machines

A well-formed multitape Turing machine body can be repeated under a guard on its scanned symbols without extra tapes. For any trace of n body transformations each bounded by T, with the guard true before each iteration and false at the final tapes, the constructed machine halts within n*(T+2)+1 steps and produces exactly the final tapes. Guard and return states preserve all contents and head positions; the body is relocated using its first halting time.

Preamble

import Definitions.Def_CookLevin_Complexity
open CookLevin
set_option autoImplicit false

Formal statement

theorem CookLevin.machine_guarded_loop_preserves_turing_and_time {k G : Nat}
    (guard : List Symbol → Bool) (body : Machine) (hbody : TuringMachine k G body) :
    ∃ R : Machine, TuringMachine k G R ∧
      ∀ (n T : Nat) (tapes : Nat → List Tape),
        (∀ i, i < n → guard (CookLevin.read (tapes i)) = true) →
        guard (CookLevin.read (tapes n)) = false →
        (∀ i, i < n → Transforms body (tapes i) T (tapes (i + 1))) →
        Transforms R (tapes 0) (n * (T + 2) + 1) (tapes n) := by sorry

Source

Direct small-step simulation of relocated machine blocks and stationary guard and return commands.

View graph