Cook–Levin machine model: separate work bank with unchanged runtime
ProvedCookLevin.machine_separate_work_bankcomplexity-theorycook-levinturing-machines
Every well-formed k-tape machine can run on k+n tapes with an arbitrary saved bank of n tapes placed between the shared input and its own work tapes. The new machine keeps the input at index zero, uses the same alphabet, and preserves every bounded transformation with the same step budget. The saved tapes retain both their contents and their head positions. The active work tapes appear in reversed index order before and after simulation; this explicit layout permits independent computations to occupy separate banks without moving the saved data.
Preamble
import Definitions.Def_CookLevin_Basic open CookLevin set_option autoImplicit false
Formal statement
theorem CookLevin.machine_separate_work_bank {k G : Nat} (M : Machine)
(hM : TuringMachine k G M) (n : Nat) :
∃ R : Machine, TuringMachine (k + n) G R ∧
∀ (input finalInput : Tape) (work finalWork saved : List Tape) (T : Nat),
work.length + 1 = k → saved.length = n →
Transforms M (input :: work) T (finalInput :: finalWork) →
Transforms R (input :: (saved ++ work.reverse)) T
(finalInput :: (saved ++ finalWork.reverse)) := by sorrySource
Direct tape-permutation simulation of CookLevin Basic, combined with the accepted machine_tape_padding_preserves_turing_and_time theorem. Reversing all work indices after suffix padding places the saved bank before the active work bank.