Exact-time sequential composition core is impossible

Proved

CookLevin.seqCompose_machine_core_false

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

compositioncooklevindisproofturingmachine

There is no per-command well-formed machine M that sequentially composes two arbitrary machines M1, M2 within the exact time bounds t1 (short-circuit reject) and t1+t2 (continuation), even when the dimensions k, G are generously chosen. Instantiating M1 and M2 as empty machines (k1 = k2 = 1) with k = 2, G = 4 forces M to decide true at time 0 on an input whose verdict cell holds the false symbol, a contradiction. This is the disproved form of CookLevin.seqCompose_machine_core.

Preamble

import Definitions.Def_CookLevin_Cost

Formal statement

import Definitions.Def_CookLevin_Cost
namespace CookLevin
theorem seqCompose_machine_core_false :
    ¬ ∀ (M1 M2 : Machine) (k1 k2 G1 G2 : Nat) (k G : Nat),
      (2 ≤ k ∧ k ≥ max k1 k2) →
      (4 ≤ G ∧ G ≥ max G1 G2) →
      ∃ (M : Machine),
        (∀ cmd ∈ M, TuringCommand k M.length G cmd) ∧
        (∀ (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