Existence of valid tape and alphabet dimensions for Turing composition

Proved

CookLevin.seqCompose_bounds

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

algebraalphabetboundstapesturing-machine

For any natural numbers $k_1, k_2$ and $G_1, G_2$ , there exist tape count $k \in \mathbb{N}$ and alphabet bound $G \in \mathbb{N}$ that satisfy the minimal Turing machine requirements ( $2 \le k$ and $4 \le G$ ) while simultaneously dominating the dimensions of both constituent machines:

k = \max(\max(k_1, k_2), 2) \ge \max(k_1, k_2), \qquad G = \max(\max(G_1, G_2), 4) \ge \max(G_1, G_2).

This ensures that the combined machine has enough tapes and a sufficiently large symbol alphabet to accommodate both $M_1$ and $M_2$ without violating the well-formedness constraints of TuringMachine.

Preamble

import Definitions.Def_CookLevin_Cost

Formal statement

namespace CookLevin
theorem seqCompose_bounds (k1 k2 G1 G2 : Nat) :
    ∃ (k G : Nat), 2 ≤ k ∧ 4 ≤ G ∧ k ≥ max k1 k2 ∧ G ≥ max G1 G2 := by sorry
end CookLevin

Source

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

View graph