Well-formed sequential composition machine with tape bounds

Disproved

CookLevin.seqCompose_machine_wf

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

sequential-compositiontape-boundsturing-machinewell-formedness

Given two multi-tape Turing machines $M_1$ and $M_2$ with $k_1, k_2$ tapes and alphabet sizes $G_1, G_2$ , there exists a composite multi-tape Turing machine $M$ whose tape count $k$ is at least $\max(k_1, k_2)$ and whose alphabet size $G$ is at least $\max(G_1, G_2)$ , satisfying $\mathrm{TuringMachine}(k, G, M)$ and the two-phase sequential execution specification:

If $M_1$ decides $\mathbf{0}$ within $t_1$ steps, $M$ halts with $\mathbf{0}$ within $t_1$ steps.
If $M_1$ decides $\mathbf{1}$ within $t_1$ steps and $M_2$ decides $b_2$ within $t_2$ steps, $M$ halts with $b_2$ within $t_1 + t_2$ steps.

This makes explicit the structural bounds on tape count and alphabet size for the composed machine.

Preamble

import Definitions.Def_CookLevin_Cost

Formal statement

namespace CookLevin
theorem seqCompose_machine_wf
    (M1 M2 : Machine) (k1 k2 G1 G2 : Nat) :
    ∃ (M : Machine) (k G : Nat),
      TuringMachine k G M ∧
      k ≥ max k1 k2 ∧
      G ≥ max G1 G2 ∧
      (∀ (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

Source

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

View graph