Formula well-formedness decided in two-phase quadratic plus linear time by Turing machine

Open

CookLevin.isFormulaStringB_machine_composed

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

compositionisformulastringbquadratic-timeturing-machineverifier

There exists a multi-tape Turing machine $M$ with tape count $k$ and alphabet size $G$ that decides whether an input string $x$ is a valid binary encoding of a CNF formula within a two-phase running time:

V(x, w) = \mathrm{isFormulaStringB}(x)

within at most $c_1 (|x| + 1)^2 + c_2 (|x| + 1)$ steps for constants $c_1, c_2 \in \mathbb{N}$ .

The decision procedure operates in two successive phases:

Transduction Phase: The machine decodes $x$ into a CNF formula and re-encodes it onto a dedicated work tape, taking $c_1 (|x| + 1)^2$ steps.
Comparison Phase: The machine traverses tape 0 (holding $x$ ) and the work tape simultaneously, checking character-by-character equality and writing the final decision bit to the verdict tape in $c_2 (|x| + 1)$ steps.

Preamble

import Definitions.Def_CookLevin_Verifier

Formal statement

namespace CookLevin
theorem isFormulaStringB_machine_composed :
    ∃ (M : Machine) (k G : Nat) (c1 c2 : Nat),
      TuringMachine k G M ∧
      ∀ x w : List Bool,
        DecidesIn M k (boolsToSymbols x) (boolsToSymbols w)
          (c1 * (x.length + 1) ^ 2 + c2 * (x.length + 1))
          (isFormulaStringB x) := by sorry
end CookLevin

Source

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

View graph