Input-to-output copy correctness

Exact simulation proof for TM.copyInputToOutputTM. Starting from the initial configuration on x, the machine skips the two left-end markers, copies one Boolean symbol per step, and halts at the first input blank after exactly |x| + 2 steps with output x.

The public theorem is stated in Complexitylib.Models.TuringMachine.Subroutines.CopyOutput.

Copy loop

Initial-configuration correctness

theorem Complexity.TM.copyInputToOutputTM_computesInTime_internal (n : ℕ) : copyInputToOutputTM.ComputesInTime id fun (m : ℕ) => m + 2

Internal implementation theorem: the copy machine computes identity in the exact linear bound m + 2.