Cook–Levin machines: uniform blank-suffix clause body

Proved

CookLevin.machine_emit_blank_suffix_clause_body

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 a blank-suffix clause for every tableau width, tape index, and position. A unary counter initially holds the negative literal number a. The machine appends the actual encoded clause without the outer formula terminator, increments the counter by 8 times the tableau symbol bound, and preserves the input and all spectator tapes. The bound is 4a+16symbols+13. It uses the identity that the positive next-cell literal number is a+8*symbols+1, so only one counter is needed.

Preamble

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

Formal statement

theorem CookLevin.machine_emit_blank_suffix_clause_body {k G : Nat} (hk : 3 ≤ k) (hG : 4 ≤ G)
    (symbols : Nat) :
    ∃ R : Machine, TuringMachine k G R ∧
      ∀ (sh : Shape) (j p : Nat) (input : Tape) (bits : List Bool) (saved : List Tape),
        sh.G = symbols → saved.length + 3 = k →
        let a := literalN (.Neg (sh.cellVar 0 j p blankSymbol))
        let chunk := (encodeFormula [[Literal.Neg (sh.cellVar 0 j p blankSymbol),
          Literal.Pos (sh.cellVar 0 j (p + 1) blankSymbol)]]).dropLast
        Transforms R
          (input :: (contents (boolsToSymbols (List.replicate a true)), 1 + a) ::
            (contents (boolsToSymbols bits), 1 + bits.length) :: saved)
          (4 * a + 16 * symbols + 13)
          (input :: (contents (boolsToSymbols (List.replicate (a + 8 * symbols) true)), 1 + (a + 8 * symbols)) ::
            (contents (boolsToSymbols (bits ++ chunk)), 1 + (bits ++ chunk).length) :: saved) := by sorry

Source

Compose fixed output writes, two source-restoring unary appends, and a fixed counter increment. Verify the result against the actual clause and formula encodings.

View graph