Direct mapping with the complete original input

The existing captured fold retains the original input while appending each callback result. Its prefix bound follows from the list's encoded length and the callback machine's own clock.

theorem Turing.MultiTapeTM.ComputableInPolyTime.mapWithInput {α β γ : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encIn : γ ↪ List Bool} {f : γ → α → β} {list : γ → List α} (hlist : ComputableInPolyTime list encIn (encList encA)) (hf : ComputableInPolyTime (fun (p : γ × α) => f p.1 p.2) (encPair encIn encA) encB) : ComputableInPolyTime (fun (x : γ) => List.map (f x) (list x)) encIn (encList encB)

Map with the complete original input captured uniformly by one joint callback machine. The list certificate fixes its element encoding before the callback is checked.