Cook–Levin machines: blank-suffix emission from zero-positioned heads

Proved

CookLevin.machine_blank_suffix_emitter_from_zero

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

complexitycook-levinloopsturing-machines

For each fixed symbol bound, one machine emits the complete blank-suffix formula with its three work heads initially at zero. The literal counter is canonical. The width tape only needs a terminated unary prefix; its remaining contents are unrestricted. Runtime is at most 3a_initial + width(4a_final+16symbols+16)+6. Input and spectator tapes are preserved. The program is independent of tableau width and tape index.

Preamble

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

Formal statement

theorem CookLevin.machine_blank_suffix_emitter_from_zero {k G : Nat} (hk : 4 ≤ k) (hG : 4 ≤ G)
    (symbols : Nat) :
    ∃ R : Machine, TuringMachine k G R ∧
      ∀ (sh : Shape) (j : Nat) (input : Tape) (fuel : Nat → Symbol) (saved : List Tape),
        sh.G = symbols → saved.length + 4 = k →
        (∀ i, i < sh.T → fuel (1 + i) = oneSymbol) →
        fuel (1 + sh.T) ≠ oneSymbol →
        let a₀ := literalN (.Neg (sh.cellVar 0 j 0 blankSymbol))
        let aₙ := literalN (.Neg (sh.cellVar 0 j sh.T blankSymbol))
        let output := encodeFormula (blankSuffixClauses sh j)
        Transforms R
          (input :: (contents (boolsToSymbols (List.replicate a₀ true)), 0) ::
            (contents [], 0) :: (fuel, 0) :: saved)
          (3 * a₀ + sh.T * (4 * aₙ + 16 * symbols + 16) + 6)
          (input :: (contents (boolsToSymbols (List.replicate aₙ true)), 1 + aₙ) ::
            (contents (boolsToSymbols output), 1 + output.length) ::
            (fuel, 1 + sh.T) :: saved) := by sorry

Source

Seek the literal counter terminator, advance output and width heads, repeat the actual clause body, and write the final formula terminator.

View graph