Sequential composition with exact time bound is impossible

Proved

CookLevin.seqCompose_machine_split_false

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

compositioncooklevindisproofturingmachine

There is no well-formed Turing machine M that sequentially composes two arbitrary machines M1, M2 within the exact sum of their running times while short-circuiting on rejection. Instantiating M1 and M2 as empty machines (k1 = k2 = 1) forces contradictory requirements on M's verdict cell, so the claimed machine cannot exist. This is the corrected, disproved form of CookLevin.seqCompose_machine_split.

Formal statement

import Definitions.Def_CookLevin_Cost
namespace CookLevin
theorem seqCompose_machine_split_false :
    ¬ ∀ (M1 M2 : Machine) (k1 k2 G1 G2 : Nat),
      ∃ (M : Machine) (k G : Nat),
        TuringMachine k G M ∧
        (∀ (xs ws : List Symbol) (t1 : Nat),
          DecidesIn M1 k1 xs ws t1 false →
          DecidesIn M k xs ws t1 false) ∧
        (∀ (xs ws : List Symbol) (t1 t2 : Nat) (b2 : Bool),
          DecidesIn M1 k1 xs ws t1 true →
          DecidesIn M2 k2 xs ws t2 b2 →
          DecidesIn M k xs ws (t1 + t2) b2) := by sorry
end CookLevin

View graph