How large are the stabilization times of Ordinal Turing Machines with an oracle for the transfinite initial ordinals? This question is based on the assumption that $V \ne L$ and we have $\omega_1^L < \omega_1$ (here $\omega_1^L$ is equal to the supremum of ordinals accidentally writable by no-oracle Ordinal Turing Machines).
Consider Ordinal Turing Machines (called “$\omega_{\alpha}$-machines”) with an oracle that provides access to all transfinite initial ordinals.
Any $\omega_{\alpha}$-machine is an Ordinal Turing Machine equipped with an extra tape (the oracle tape). We may assume that this tape is read-only.
Let $t(\alpha)$ denote the symbol written on an $\alpha$-th cell of the oracle tape. Then $t(\alpha) = 1$ if and only if $\alpha$ is an initial ordinal.
If $\epsilon > 0$, then the $\epsilon$-stabilization time of a machine is the successor of $\gamma_0$, where $\gamma_0$ is the least ordinal such that the values of all symbols written on all cells of the initial segment of length $\epsilon$ of the output tape never change at any time $\gamma > \gamma_0$. If $\epsilon = 0$, then the $\epsilon$-stabilization time of a machine is the successor of $\gamma_0$, where $\gamma_0$ is the least ordinal such that the values of all symbols written on all cells (i.e. cells indexed by any element of the class of all ordinals) of the entire output tape never change at any time $\gamma > \gamma_0$. If a machine halts, then $\gamma_0$ is not greater than the halting time. If an ordinal $\gamma_0$ does not exist, then the corresponding $\epsilon$-stabilization time is $0$.
Let $F_{\epsilon}(i)$ denote the $\epsilon$-stabilization time of an $i$-th $\omega_{\alpha}$-machine, assuming that all computations start with no ordinal parameters (i.e. empty input).
Assuming that we have fixed a particular way to encode a countable ordinal by an infinite binary sequence of length $\omega_0=\omega$, the ordinal $\tau_0$ is defined as the supremum of ordinals eventually writable by $\omega_{\alpha}$-machines with empty input on the initial segment of length $\omega_0=\omega$ of the output tape. The reasoning behind this definition of $\tau_0$ is that there may be $\omega_{\alpha}$-machines whose initial output segments of length $\omega$ stabilize at a time $\ge \omega_1$ (i.e. $F_{\omega}(i) \ge \omega_1$), yet all other output segments are irrelevant: they stabilize at an arbitrarily large time or even diverge. That is, I suppose that there may exist a machine $M_n$ such that, for example, $F_0(n) = 0$, yet $F_{\omega}(n) \ge \omega_1$. In this case, if the eventually stable content on the initial $\omega$-segment of the output tape encodes an ordinal, this countable ordinal is eventually writable by $M_n$.
The ordinal $\tau_1$ is defined as follows: $$\tau_1 = \sup \{F_0(i) : i \in \mathbb{N}\}.$$
Is it possible to estimate how large are $\tau_0$ and $\tau_1$ (at least, give a “reasonably accurate” estimate for the lower/upper bounds)? In particular, is $\tau_0$ larger than the least ordinal $\delta$ such that $L_{\delta} \prec_{\Sigma_3} L_{\omega_1}$ (the latter is mentioned in this comment and this answer on Mathoverflow)?
 A: For ordinal Turing machines with an oracle $S⊂Ord$,
- the set/class of output locations that are written at some point is $Σ^{L[S]}_{1,S}$ (i.e. $Σ_1$ in $L[S]$ with a predicate for $S$) and can be arbitrary such,
- the set/class of output locations that are eventually 1 is $Σ^{L[S]}_{2,S}$ and can be arbitrary such,
- any set in $L[S]$ (but no set not in $L[S]$) can be 'accidentally' written at some point.
The supremum of eventually writable (as subsets of $ω$) ordinals $τ_0$ is the least ordinal that is not $Δ^{L[S]}_{2,S}$ definable.  The supremum of stabilization times $τ_1$ is the supremum of $Δ^{L[S]}_{2,S}$ definable ordinals (possibly uncountable).  Similarly, the supremum of writable (as subsets of $ω$) ordinals is the least ordinal not $Δ^{L[S]}_{1,S}$ definable, and the supremum of halting times is the supremum of $Δ^{L[S]}_{1,S}$ definable ordinals.
Your question corresponds to $S=\mathrm{Card}$ (cardinals).  I actually considered $S=\mathrm{Card}$ in the question Cardinal Register Machines, but it is worth it to elaborate it further.
Case 1:  There is no sharp for a proper class of measurable cardinals.  Then:
- $K^{L[\mathrm{Card}]}$ is an iterate of the core model $K$.  ($K^{L[\mathrm{Card}]}$ does not have a sharp since otherwise enough cardinals will be indiscernible to generate a proper of class of measurables $K^{L[\mathrm{Card}]}$.)
- If $V=K$ (which holds if $V=L$), then for sets below the least measurable cardinal (or arbitrarily if there are none), $Δ^{L[\mathrm{Card}]}_{1,\mathrm{Card}}=Δ_2$ and $Δ^{L[\mathrm{Card}]}_{2,\mathrm{Card}}=Δ_3$.  I think the only difference between $K$ and $L[\mathrm{Card}]$ (if $V=K$) is that every measurable cardinal $κ$ (and its measure) in $K$ is converted into a Prikry sequence $κ,κ^{+},κ^{++},...$ for $κ^{+ω}$.
- Non-absoluteness:  There is an ordinal Turing machine $M$ such that if $V$ is a (set) generic extension of $K$ (not sure if this condition is needed), then for every set of ordinals $s$, there is a generic extension $V[G]$ such that in $V[G]$ (and using $\mathrm{Card}^{V[G]}$), $M$ outputs $s$ and halts.  (For example, $M$ can check which cardinal successors are computed correctly for the least $L_α[\mathrm{Card}]$ that correctly computes enough cardinals.)  I think such $M$ (if it works for all such $s$ and $V$) cannot halt if the above sharp exists:  In every case, $\mathrm{Card}$ should in a sense give indiscernibles (and thus be unavailable for coding) until $L[\mathrm{Card}∩α]$ contains all reals in $K$, and if the sharp exists, $M$ should be stuck in the pre-decoding phase.
Case 2:  There is a sharp for a proper class of measurable cardinals.  Then, $K^{L[\mathrm{Card}]}$ is an iterate of the minimal inner model $K'$ with a proper class of measurable cardinals.  Writable (as subsets of $ω$) countable ordinals are exactly $Δ_2^{K'}∩ω_1^{K'}$, and eventually writable — $Δ_3^{K'}∩ω_1^{K'}$.  Note that these are $Δ^1_3$ (in $V$) and independent of forcing.  As an aside, with stronger large cardinal axioms, more structure becomes forcing-independent; for example, see my questions Complexity of L[cf] and Inner models with all sets generic.
