Cook–Levin machines: blank-suffix clause loop from initialized counters

Proved

CookLevin.machine_blank_suffix_emitter_from_counters

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

complexitycook-levinloopsturing-machines

For each fixed tableau symbol bound, one well-formed Turing machine emits the complete encoded blank-suffix formula from an initialized literal counter and a unary width tape. The same program works for every tableau width and tape index. It preserves the input and spectator tapes and has explicit runtime bounded by width times (4 times the final literal number plus 16 times the symbol bound plus 16), plus 2.

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_counters {k G : Nat} (hk : 4 ≤ k) (hG : 4 ≤ G)
    (symbols : Nat) :
    ∃ R : Machine, TuringMachine k G R ∧
      ∀ (sh : Shape) (j : Nat) (input : Tape) (saved : List Tape),
        sh.G = symbols → saved.length + 4 = k →
        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)), 1 + a₀) ::
            (contents [], 1) :: (contents (List.replicate sh.T oneSymbol), 1) :: saved)
          (sh.T * (4 * aₙ + 16 * symbols + 16) + 2)
          (input :: (contents (boolsToSymbols (List.replicate aₙ true)), 1 + aₙ) ::
            (contents (boolsToSymbols output), 1 + output.length) ::
            (contents (List.replicate sh.T oneSymbol), 1 + sh.T) :: saved) := by sorry

Source

Iterate the uniform clause body with a unary fuel tape, then append the formula terminator. Identify the accumulated stream with the actual blankSuffixClauses encoding.

View graph