Only admissibles start gaps in clockable ordinals This is a question about ITTM model introduced by Hamkins et al. In this paper it is proven that no admissible ordinal is clockable, so it either starts or lies within a gap in clockable ordinals. I seek for reference concerning sort of opposite result - that if an ordinal starts such gap, then it's necessarily admissible.
P.D.Welch claims here to have proof of this fact, however he doesn't give one.
I'm asking for either a reference to full proof or at least a sketch of the methods used in obtaining this result.
Thanks for help in advance!
 A: Let me sketch the argument. Philip Welch is also on
MO, and I would encourage him to post further explanation and details.
The main question left open in the original ITTM paper 


*

*Joel David Hamkins and Andy Lewis, Infinite time Turing machines, J. Symbolic Logic 65 (2000), no. 2, 567--604. blog post
was whether every clockable ordinal was writable. This was
answered beautifully by Philip Welch in


*

*P. D. Welch, The length of infinite time Turing machine computations, Bull. London Math. Soc. 32 (2000), no. 2, 129--136.


This result led to his $\lambda,\zeta,\Sigma$ theorem, which
asserts that $$L_\lambda\prec_{\Sigma_1}L_\zeta\prec_{\Sigma_2}
L_\Sigma,$$ where $\lambda$ is the supremum of the writable
ordinals, $\zeta$ is the supremum of the eventually writable
ordinals and $\Sigma$ is the supremum of the accidentally
writable ordinals. What Philip showed was that every infinite
time Turing machine computation (on writable input) repeats its
stage $\zeta$ configuration at time $\Sigma$, and from this it
follows that there are no clockable ordinals above $\lambda$.
This argument is fantastic, because it shows that whenever an
infinite time Turing machine $p$ halts on some input $x$, there is
another infinite time Turing machine that on input $x$ produces a
complete description of the computation history of $p$ on $x$, and in particular it writes an ordinal coding the ordinal halting time of that computation.
A finer analysis of the proof shows a bit more, which is relevant
for your question:
Lemma. (Welch) If an ordinal $\beta$ is clockable, then
$\beta$ is writable in time before the next gap in the clockable
ordinals.
Indeed, I recall that the stronger forms of the lemma show that
$\beta$ is clockable in time $\beta+\omega$, or even right in time
$\beta$, but for this case I'd have to think it through again, or
perhaps Philip can post about it (I don't recall which of Philip's
papers has this argument). It is interesting to note what happens
down low: in time $\omega$, we can write a real coding any
particular ordinal below $\omega_1^{CK}$, which begins the first
gap, and at time $\omega_1^{CK}+\omega$, which is clockable again,
we can write reals coding $\omega_1^{CK}$ and indeed all the
ordinals up to the second admissible ordinal.
Given this lemma, we can now answer your question.
Theorem. (Welch) If $\xi$ begins a gap in the clockable
ordinals, then $\xi$ is admissible.
Proof. Suppose that $\xi$ begins a gap in the clockable ordinals.
In particular, $\xi$ is a limit of clockable ordinals.
Furthermore, each of these ordinals is writable in time before
$\xi$, and so in particular, every ordinal below $\xi$ is writable
in time before $\xi$. Now, suppose $\xi$ were not admissible. Then
$L_\xi$ would have a $\Sigma_1$ definable map $f:\alpha\to\xi$
that was unbounded in $\xi$, for some $\alpha<\xi$, and in fact we
may assume $\alpha=\omega$ here. Thus, $L_\xi$ is the first stage
of the constructibility hierarchy where infinitely many instances
of a certain $\Sigma_1$ fact becomes true. Consider now the
infinitary algorithm that generates all writable reals, checking
if they code an ordinal $\beta$, and if they do generating a real
coding the structure $\langle L_\beta,\in\rangle$ (as in the style
of the literature mentioned above), and checking in this structure
to see how many witnesses there are to the $\Sigma_1$ fact. Since
$\xi$ begins a gap, it has sufficient closure properties that for
any particular $\beta<\xi$, all this can be checked in time less
than $\xi$. Every time we find a larger ordinal $\beta$ than
previously with a new instance of the $\Sigma_1$ fact, then we can
flash a certain master flag. By our assumption on $\xi$, it will
be first at stage $\xi$ that this master flag is on, and so our
algorithm can halt at stage $\xi$. This contradicts the assumption
that $\xi$ was not clockable. QED
A: I'd like to add to Joel's generous and thorough answer. He is right to recall that if $\beta$ is clockable, then $\beta$ is writable in order type at most $\beta$-steps (thus improving the Lemma).  One can argue this directly and it sounds like you have found the paper, but for completeness it is in:
P.D. Welch ``Characteristics of discrete transfinite Turing machine models:
halting times, stabilization times, and Normal Form Theorems'' in Theoretical Computer Science, vol. 410, Jan. 2009, 426-442 doi: 10.1016/j.tcs.2008.09.050,
But actually there is a nice argument, which involves seeing how an ITTM can compute directly codes for levels of the $L$-hierarchy up to $\Sigma$, at the same time as computing the theories of each such level.
Theorem. There is an ITTM program so that for limit $\alpha$ (i) it has at time $\omega^2\cdot\alpha$ on a section of its tape: a set $T_\alpha \subseteq \mathbb{N}$ so that (via some usual goedel coding) the complete $\Sigma_2$-theory of $(L_\alpha, \in)$ is uniformly r.e. in $T_\alpha$.
(ii) at time $\omega^2\cdot\alpha +\omega\cdot2$ on another section of the tape there is a code $E_\alpha$ for $(L_\alpha, \in)$  (meaning that $(\omega, E_\alpha) \cong   (L_\alpha, \in)$).
Because we are below $\Sigma$, (uniformly) recursive in the $\Sigma_2$-theory of $(L_\alpha, \in)$ is a wellorder of order-type $\alpha$. This leads to:
Corollary If a limit $\alpha$ is clockable, then a code for $\alpha$ is writable by time $\alpha + \omega$ 
(just add on the extra steps to write out (a code for) the wellorder).
With some more fiddling around and consideration of cases that ``$+\,\omega$'' can be removed, and also for successor cases... 
The theorem appears in:
S-D Friedman & P.D. Welch Two Observations concerning Infinite Time Turing Machines, in Bonn International Workshop on Ordinal Computability, Ed: I. Dmitriou, J. Hamkins & P. Koepke, 2007, Bonn, 44-48.
http://www.math.uni-bonn.de/ag/logik/events/biwoc/report.pdf
There the theorem is proven for the Jensen $J_\alpha$ hierarchy, but with work it can be done for the $L_\alpha$'s too.
