Cook–Levin machines: concatenate bank outputs onto the last tape
ProvedCookLevin.machine_concatenate_bank_outputscomplexity-theorycook-levinturing-machines
For every pair of saved-bank sizes a,b and alphabet G >= 4, a fixed well-formed (a+b+4)-tape machine concatenates terminated outputs xs and ys onto its last physical tape in |xs|+|ys|+3 steps. Initial physical order is input, a saved tapes, first source at head zero, second source at head zero, b saved tapes, then a fresh blank destination. The final last tape is exactly contents(boolsToSymbols(xs++ys)), including the start marker and blank tail. Both source contents, input, and saved banks are preserved, with only the source and destination heads advancing. This matches the bank boundary created by the independent-computation construction after all-head reset.
Preamble
import Definitions.Def_CookLevin_Cost open CookLevin set_option autoImplicit false
Formal statement
theorem CookLevin.machine_concatenate_bank_outputs {a b G : Nat} (hG : 4 ≤ G) :
∃ R : Machine, TuringMachine (a + b + 4) G R ∧
∀ (xs ys : List Bool) (input : Tape) (f g : Nat → Symbol)
(left right : List Tape), left.length = a → right.length = b →
(∀ j, (hj : j < xs.length) → f (1 + j) = boolSym (xs[j])) →
(¬ (f (1 + xs.length) = zeroSymbol ∨ f (1 + xs.length) = oneSymbol)) →
(∀ j, (hj : j < ys.length) → g (1 + j) = boolSym (ys[j])) →
(¬ (g (1 + ys.length) = zeroSymbol ∨ g (1 + ys.length) = oneSymbol)) →
Transforms R (input :: (left ++ (f, 0) :: (g, 0) :: (right ++ [(contents [], 0)])))
(xs.length + ys.length + 3)
(input :: (left ++ (f, 1 + xs.length) :: (g, 1 + ys.length) ::
(right ++ [(contents (boolsToSymbols (xs ++ ys)), 1 + xs.length + ys.length)]))) := by sorrySource
Direct machine construction from CookLevin Basic/Cost: prepare three heads, copy the first prefix, then run a tape-permuted second copier. Composed using the accepted machine_sequence_preserves_turing_and_time theorem.