In their arXiv preprint, "Infinite Time Turing Machines" (arXiv:math/9808093v1 [math.LO] 21 Aug 1998) Hamkins and Lewis state the Lost Melody Theorem for ITTM's as follows:

Lost Melody Theorem 4.9 [pg. 28 in the preprint above—my comment]. There is a real, $c$, such that {$c$} is decidable, but $c$ is not writable. Consequently, there is a constant, total function which is not computable, but whose graph is nevertheless decidable: $f(x)= c$.

Consider also the following quote from the Carl, Schlicht, and Welch paper, "Recognizable Sets and Woodin Cardinals: Computations Beyond the Constructible Universe" (pg. 5 in my copy):

A typical phenomenon for infinitary computations is the existence of sets of ordinals which are recognizable, but not computable. Following [HL00][that is, the Hamkins /Lewis paper just referred to—my comment], we call such sets

lost melodies.

Finally, to return to the Hamkins/Lewis paper, consider further their motivation for the Lost Melody Theorem found in the little paragraph directly above the statement of the theorem:

Like the previous theorem, the next identifies a surprising divergence [as in 'not in'?—my comment] from the classical theory [the "classical theory" presumably being ordinary recursion theory—my comment]. The real $c$ in the theorem is like a forgotten melody that you cannot produce on your own but which you can recognize when someone sings it to you.

My motivation for the question hangs both on this metaphor and on the fact two groups of authors seem to claim that such 'lost melodies' are an infinitary phenomenon, yet I would wager that many (including myself) have had times where we could not remember some melody but recognized it when hummed (or sung) back to us (a decidedly finite phenomenon). Indeed, if one assumes that the human brain can be instantiated by a Turing machine (otherwise we would have to accept J.R. Lucas-like arguments as valid), there would have to be an analogue of the Lost Melody Theorem in ordinary recursion theory, wouldn't there (perhaps it would be a type of computational-complexity theorem)?

8more comments