General sequential composition of multi-tape Turing machines

Disproved

CookLevin.turingMachine_seqCompose_general

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

complexity-theorygeneral-decidersequential-compositionturing-machine

Given two multi-tape Turing machines $M_1$ and $M_2$ with tape counts $k_1, k_2$ and alphabet bounds $G_1, G_2$ , there exists a sequential composition multi-tape Turing machine $M$ with tape count $k$ and alphabet size $G$ satisfying $\mathrm{TuringMachine}(k, G, M)$ that decides the conjunction of their decisions on arbitrary tape symbols:

\forall xs, ws \in \mathrm{List}\,\mathrm{Symbol},\; \forall t_1, t_2 \in \mathbb{N},\; \forall b_1, b_2 \in \mathbb{B},

\mathrm{DecidesIn}(M_1, k_1, xs, ws, t_1, b_1) \to \mathrm{DecidesIn}(M_2, k_2, xs, ws, t_2, b_2) \to \mathrm{DecidesIn}(M, k, xs, ws, t_1 + t_2, b_1 \wedge b_2).

The composed machine $M$ executes $M_1$ on the input tapes for $t_1$ steps. If $M_1$ rejects ( $b_1 = \mathbf{0}$ ), $M$ halts with verdict $\mathbf{0}$ . If $M_1$ accepts ( $b_1 = \mathbf{1}$ ), $M$ transitions to run $M_2$ on the input tapes for $t_2$ steps and copies $M_2$ 's final verdict bit to the verdict tape. The combined execution time is bounded by $t_1 + t_2$ steps.

This generalizes sequential decider composition to arbitrary symbol alphabets and unconstrained time parameters.

Preamble

import Definitions.Def_CookLevin_Cost

Formal statement

namespace CookLevin
theorem turingMachine_seqCompose_general
    (M1 M2 : Machine) (k1 k2 G1 G2 : Nat) :
    ∃ (M : Machine) (k G : Nat),
      TuringMachine k G M ∧
      ∀ (xs ws : List Symbol) (t1 t2 : Nat) (b1 b2 : Bool),
        DecidesIn M1 k1 xs ws t1 b1 →
        DecidesIn M2 k2 xs ws t2 b2 →
        DecidesIn M k xs ws (t1 + t2) (b1 && b2) := by sorry
end CookLevin

Source

https://github.com/Rizvonium/cook_levin_lean_v1/blob/main/CookLevinLean/Basic.lean#L70

View graph