Formula round-trip function computed in quadratic time by Turing machine

Open

CookLevin.formulaRoundTrip_unary_transducer

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

computesintimedecodeformulaencodeformulaquadratic-timeturing-machine

There exists a multi-tape Turing machine $M$ with tape count $k$ and alphabet size $G$ that computes the formula round-trip transformation in quadratic time:

f(x) = \mathrm{encodeFormula}(\mathrm{decodeFormula}(x))

satisfying $\mathrm{ComputesInTime}(M, k, n \mapsto c_1 (n+1)^2, f)$ for a constant $c_1 \in \mathbb{N}$ .

Given the binary encoding $x$ on tape 0 with no certificate on tape 1, $M$ parses $x$ into a formula clause structure and serializes it back into binary. Because the parsing and serialization passes each perform linear-time traversals of the string, the whole computation completes in $c_1 (|x| + 1)^2$ steps in the standard cost model.

Preamble

import Definitions.Def_CookLevin_Verifier

Formal statement

namespace CookLevin
theorem formulaRoundTrip_unary_transducer :
    ∃ (M : Machine) (k G c1 : Nat),
      TuringMachine k G M ∧
      ComputesInTime M k (fun n => c1 * (n + 1) ^ 2) (fun x => encodeFormula (decodeFormula x)) := by sorry
end CookLevin

Source

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

View graph