Cook–Levin machine model: alphabet enlargement preserves computation
ProvedCookLevin.machine_alphabet_enlargement_preserves_computationcomplexity-theorycook-levinturing-machines
Every well-formed k-tape machine over alphabet G can be replaced by a well-formed k-tape machine over any larger alphabet H. The replacement computes every function computed by the original machine with exactly the same step-bound function. It preserves the actual final configurations, halting state, and output-decoder fuel on all standard Boolean inputs; there is no runtime or output-length approximation.
Preamble
import Definitions.Def_CookLevin_Cost open CookLevin set_option autoImplicit false
Formal statement
theorem CookLevin.machine_alphabet_enlargement_preserves_computation {k G H : Nat}
(M : Machine) (hM : TuringMachine k G M) (hGH : G ≤ H) :
∃ R : Machine, TuringMachine k H R ∧
∀ (T : Nat → Nat) (f : List Bool → List Bool),
ComputesInTime M k T f → ComputesInTime R k T f := by sorrySource
A guard preserves the original command on scans inside alphabet G and halts with stationary write-back actions otherwise. Starting from Boolean inputs and blank work tapes, an alphabet invariant ensures that the guard never changes an original execution.