Input-to-output copy correctness

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 |x| + 2 steps with output x; the exported theorem records m + 2 as an upper bound.

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 within the linear bound m + 2.