CNF evaluation decided in quadratic time by Turing machine

Open

CookLevin.satisfiesB_machine_quad

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

quadratic-timesatisfiesbturing-machineverifier

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

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

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

The evaluation parses $x$ into a clause list and $w$ into variable assignments. For each clause in the formula, the machine checks whether at least one literal evaluates to true under the assignment by seeking the corresponding bit in $w$ . Since the total number of literals is bounded by $|x|$ and each lookup in $w$ takes $O(|w|)$ head movements, the total execution time is bounded by $O(|x| \cdot |w|) \subseteq O((|x| + |w| + 1)^2)$ .

Preamble

import Definitions.Def_CookLevin_Verifier

Formal statement

namespace CookLevin
theorem satisfiesB_machine_quad :
    ∃ (M : Machine) (k G : Nat) (c0 : Nat),
      TuringMachine k G M ∧
      ∀ x w : List Bool,
        DecidesIn M k (boolsToSymbols x) (boolsToSymbols w)
          (c0 * (x.length + w.length + 1) ^ 2)
          (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