Unary input-length transducer — proof internals

This module proves the exact execution contract for TM.unaryLengthTM. Starting from an initial configuration on x, it skips the left-end marker, writes one true bit per input bit, and halts on the first input blank after exactly |x| + 2 transitions.

theorem Complexity.TM.unaryLengthTM_computesInTime_internal (n : ℕ) : unaryLengthTM.ComputesInTime (fun (x : List Bool) => List.replicate x.length true) fun (m : ℕ) => m + 2

Internal implementation theorem: unaryLengthTM emits the unary input length within the linear bound m + 2.