Streaming lookup of the simulated input symbol

After linear argument reordering, inputSymbol_stream_inO streams the unary-encoded list once, retaining a binary countdown. The selected symbol is emitted directly; it is never retained across later rounds. With encoded input length N and binary position length b, lookup takes O((N + 1) * (b + 1)²) time and linear workspace. The square comes from the existing binary predecessor certificate.

The public theorem supplies a plain machine certificate. Its implementation uses the streaming fold backend and includes the linear cost of moving the position before the list in the encoding.

theorem Turing.MultiTapeTM.Universal.length_inputSymbol_le (x : List ℕ) (p : ℕ) : ((encOption encUnary) (inputSymbol x p)).length ≤ ((encList encUnary) x).length + 1

A lookup returns at most one input symbol, with one additional bit for the option tag.

theorem Turing.MultiTapeTM.Universal.inputSymbol_stream_inO : ComputableInO (fun (q : List ℕ × ℕ) => inputSymbol q.1 q.2) (encPair (encList encUnary) encNat) (encOption encUnary) (fun (q : List ℕ × ℕ) => (((encList encUnary) q.1).length + 1) * ((encNat q.2).length + 1) ^ 2) fun (q : List ℕ × ℕ) => ((encPair (encList encUnary) encNat) q).length

After linear argument reordering, the simulated input symbol can be found by streaming the encoded list once, with a binary countdown. Time is linear in encoded list length times the square of the binary position length; workspace is linear in the complete encoded input. The returned certificate contains an actual multitape machine, including the cost of reordering the arguments for the streaming pass.