Formula well-formedness decided in quadratic time by Turing machine

Proved

CookLevin.isFormulaStringB_machine_quad

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

isformulastringbquadratic-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 quadratic time:

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

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

The decision procedure evaluates isFormulaStringB x, which checks whether encodeFormula (decodeFormula x) = x. Decoding $x$ into a CNF formula $\varphi$ and re-encoding $\varphi$ into binary both perform linear-time sweeps over the representation. Comparing the re-encoded list with $x$ takes quadratic time on a standard Turing machine due to tape head repositioning. Because the decision is independent of the witness $w$ , the step count is bounded by $c_0 (|x| + 1)^2 \le c_0 (|x| + |w| + 1)^2$ .

Preamble

import Definitions.Def_CookLevin_Verifier

Formal statement

namespace CookLevin
theorem isFormulaStringB_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)
          (isFormulaStringB x) := by sorry
end CookLevin

Source

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

View graph