CNF evaluation decided in product time by multi-tape Turing machine

Open

CookLevin.satisfiesB_machine_product

by Mazecto · Sep 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

cnf-evaluationproduct-timesatisfiesbturing-machineverifier

There exists a multi-tape Turing machine $M$ with tape count $k$ and alphabet size $G$ that evaluates whether truth assignment $w$ satisfies CNF formula $x$ within product time:

V(x, w) = \mathrm{satisfiesB}(\mathrm{decodeAssignment}(w), \mathrm{decodeFormula}(x))

within at most $c_1 (|x| + 1)(|w| + 1)$ steps for a constant $c_1 \in \mathbb{N}$ .

The formula $\varphi = \mathrm{decodeFormula}(x)$ contains at most $|x|$ literals across all its clauses. For each literal of the form $v_n$ or $\neg v_n$ , $M$ scans the certificate tape 1 up to position $n$ to inspect the truth value assigned by $w$ , requiring at most $|w| + 1$ tape head shifts per literal. The total execution time is therefore bounded by $c_1 (|x| + 1)(|w| + 1)$ steps.

Preamble

import Definitions.Def_CookLevin_Verifier

Formal statement

namespace CookLevin
theorem satisfiesB_machine_product :
    ∃ (M : Machine) (k G : Nat) (c1 : Nat),
      TuringMachine k G M ∧
      ∀ x w : List Bool,
        DecidesIn M k (boolsToSymbols x) (boolsToSymbols w)
          (c1 * (x.length + 1) * (w.length + 1))
          (satisfiesB (decodeAssignment w) (decodeFormula x)) := by sorry
end CookLevin

Source

https://github.com/Rizvonium/cook_levin_lean_v1/blob/main/CookLevinLean/Verifier.lean#L54

View graph