Composition of transducer and comparator Turing machines

Open

CookLevin.transducer_comparator_compose

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

comparatorcook-levintransducerturing-machine

Given a transducer Turing machine M1 running in quadratic time that computes encodeFormula (decodeFormula x) from input x, and an equality comparator machine M2 running in linear time, their sequential composition produces a Turing machine M running in c1 * (|x|+1)^2 + c2 * (|x|+1) steps that decides whether encodeFormula (decodeFormula x) = x.

Preamble

import Definitions.Def_CookLevin_Verifier

Formal statement

namespace CookLevin
theorem transducer_comparator_compose
    (c1 : Nat) (M1 : Machine) (k1 G1 : Nat) (hwf1 : TuringMachine k1 G1 M1)
    (htrans : ∀ x w : List Bool,
      (execute M1 (startConfig2 k1 (boolsToSymbols x) (boolsToSymbols w)) (c1 * (x.length + 1) ^ 2)).1 = M1.length ∧
      outputOf k1 (execute M1 (startConfig2 k1 (boolsToSymbols x) (boolsToSymbols w)) (c1 * (x.length + 1) ^ 2))
        (c1 * (x.length + 1) ^ 2 + 2) = encodeFormula (decodeFormula x))
    (c2 : Nat) (M2 : Machine) (k2 G2 : Nat) (hwf2 : TuringMachine k2 G2 M2)
    (hcomp : ∀ x y : List Bool,
      DecidesIn M2 k2 (boolsToSymbols x) (boolsToSymbols y)
        (c2 * (x.length + 1))
        (decide (y = x))) :
    ∃ (M : Machine) (k G : 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))
          (decide (encodeFormula (decodeFormula x) = x)) := by sorry
end CookLevin

Source

https://github.com/Rizvonium/cook_levin_lean_v1

View graph