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

Open

CookLevin.formulaRoundTrip_transducer

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

decodeformulaencodeformulaquadratic-timetransducerturing-machine

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

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

on its output tape within quadratic time $c_1 (|x| + 1)^2$ for a constant $c_1 \in \mathbb{N}$ .

The machine reads the input string $x$ on tape 0, parses the clauses and literals into an intermediate tape representation, and serializes the resulting formula back to its canonical binary representation. Because the certificate $w$ on tape 1 is ignored and both decoding and encoding perform sequential traversals of the string representation, the execution completes in $c_1 (|x| + 1)^2$ steps.

Preamble

import Definitions.Def_CookLevin_Verifier

Formal statement

namespace CookLevin
theorem formulaRoundTrip_transducer :
    ∃ (M : Machine) (k G c1 : Nat),
      TuringMachine k G M ∧
      ∀ x w : List Bool,
        (execute M (startConfig2 k (boolsToSymbols x) (boolsToSymbols w)) (c1 * (x.length + 1) ^ 2)).1 = M.length ∧
        outputOf k (execute M (startConfig2 k (boolsToSymbols x) (boolsToSymbols w)) (c1 * (x.length + 1) ^ 2))
          (c1 * (x.length + 1) ^ 2 + 2) = encodeFormula (decodeFormula x) := by sorry
end CookLevin

Source

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

View graph