Turing machine conjunction composition with explicit linear overhead

Proved

CookLevin.turingMachine_and_compose_overhead

by junyihjy · Sep 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

compositioncooklevincorrectedturingmachine

Let $M_1, M_2$ be well-formed Turing machines deciding predicates $V_1, V_2$ in times $T_1(n), T_2(n)$ . Then there exist a constant $C$ and a well-formed machine $M$ deciding the conjunction $V_1 \\land V_2$ in time

T_1(n) + T_2(n) + C\\cdot(T_1(n) + T_2(n) + n + 1).

The exact bound $T_1(n)+T_2(n)$ is unachievable in general: the composed machine must copy the input to a pristine tape bank for $M_2$ (since $M_1$ may clobber its tapes), reposition heads after each phase (cost proportional to the distance traveled), and combine the verdicts. This is the corrected, true form of the exact-bound composition claim $CookLevin.turingMachine\\_and\\_compose$ , which is false as stated.

Formal statement

import Definitions.Def_CookLevin_Cost
namespace CookLevin
theorem turingMachine_and_compose_overhead
    (M1 M2 : Machine) (k1 k2 G1 G2 : Nat)
    (hwf1 : TuringMachine k1 G1 M1) (hwf2 : TuringMachine k2 G2 M2)
    (V1 V2 : List Bool → List Bool → Bool)
    (T1 T2 : Nat → Nat)
    (hdec1 : ∀ x w : List Bool, DecidesIn M1 k1 (boolsToSymbols x) (boolsToSymbols w) (T1 (x.length + w.length)) (V1 x w))
    (hdec2 : ∀ x w : List Bool, DecidesIn M2 k2 (boolsToSymbols x) (boolsToSymbols w) (T2 (x.length + w.length)) (V2 x w)) :
    ∃ (C : Nat) (M : Machine) (k G : Nat),
      TuringMachine k G M ∧
      ∀ x w : List Bool,
        DecidesIn M k (boolsToSymbols x) (boolsToSymbols w)
          (T1 (x.length + w.length) + T2 (x.length + w.length) +
            C * (T1 (x.length + w.length) + T2 (x.length + w.length) + (x.length + w.length) + 1))
          (V1 x w && V2 x w) := by sorry
end CookLevin

View graph