Cook–Levin machines: append fixed bits on a chosen work tape
ProvedCookLevin.machine_append_fixed_bitscomplexitycook-levinloopsturing-machines
For any fixed bit string and any selected work tape, a well-formed Turing machine appends that string to the tape in exactly its length many steps. The tape initially holds a standard binary output with its head immediately after the output. The final entire tape is the standard encoding of the concatenation, the head advances by the word length, and all other tape contents and heads are preserved. The construction requires no additional tapes.
Preamble
import Definitions.Def_CookLevin_Complexity open CookLevin set_option autoImplicit false
Formal statement
theorem CookLevin.machine_append_fixed_bits {j k G : Nat} (hk : 2 ≤ k)
(hj : 0 < j) (hG : 4 ≤ G) (bits : List Bool) :
∃ R : Machine, TuringMachine k G R ∧
∀ (left right : List Tape) (output : List Bool),
left.length = j →
Transforms R (left ++ (contents (boolsToSymbols output), 1 + output.length) :: right)
bits.length
(left ++ (contents (boolsToSymbols (output ++ bits)), 1 + output.length + bits.length) :: right) := by sorrySource
A single alphabet-safe bit-writing command preserves spectators. Induction on the fixed word uses the accepted sequential-composition theorem.