There's a (fairly basic) fact I want to use in a paper I'm writing; it's not entirely trivial, so I don't feel comfortable just stating the result and moving on, but I don't have a citation for it. Can anyone provide a reference? (I'd be willing to include it if I thought it was new, but it's the sort of thing that at least feels like folklore.) I've put the proof below for those interested.
The result is a kind of $\Sigma^1_1$ bounding claim (although the proof I have doesn't actually use $\Sigma^1_1$ bounding); namely, that from a $\Sigma^1_1$ description of an ordinal relative to some structure, I can pass to a computable description of a possibly longer ordinal relative to that same structure.
Formally, the result is:
Suppose we have
a countable structure (in a finite (or at worst computable) language) $\mathfrak{A}$,
a $\Sigma^1_1$ formula $\varphi(x, X)=\exists Y\psi(x, X, Y)$, and
an ordinal $\alpha$,
such that $\varphi$ defines a copy of $\alpha$ uniformly from any copy of $\mathfrak{A}$; more precisely, such that whenever $A$ is a structure with domain $\omega$ which is isomorphic to $\mathfrak{A}$ (below: $\omega$-copy), $\varphi(x, A)$ defines a well-ordering of $\omega$ of ordertype $\alpha$.
Then there is some $e\in\omega$ and some ordinal $\beta\ge\alpha$ such that for each $\omega$-copy $A$ of $\mathfrak{A}$, $\Phi_e^A\cong\beta$.
EDIT: In fact, from the proof we get a slightly stronger result - that if there is a $\Sigma^1_1$ formula which defines an ordinal when fed any copy of $\mathfrak{A}$, then there is some ordinal uniformly computable from copies of $\mathfrak{A}$ which is greater than any of the ordinals the above formula can produce from any copy of $\mathfrak{A}$. (This is not quite a trivial application of $\Sigma^1_1$-bounding, because of the word "uniformly": $\Sigma^1_1$-bounding does give us that there is an ordinal $\alpha$ which is computable in each copy of $\mathfrak{A}$ and appropriately large, but it does not give a uniform computation of $\alpha$ from arbitrary copies of $\mathfrak{A}$.)
Proof: First, terminology. For $k\in\omega$, a $k$-shuffle is a bijection $f: A\rightarrow B$ for some $A, B\subset\omega$ with $\vert A\vert=\vert B\vert=2k$ and $\{0, ..., k-1\}\subset A\cap B$. The point is that if $\sigma_i$ are $i$-shuffles for $i\in\omega$ and $s_0\subset s_1\subset...$, the map $\bigcup s_i$ is in fact a permutation of $\omega$. This is basically the back-and-forth condition.
Now given an $\omega$-copy $A$ of $\mathfrak{A}$, we build a tree $T_A$ as follows. We'll then convert this into a well-founded tree $S_A$, and let $\beta$ be the Kleene-Brouwer order of that tree. The trees in question are not defined as sets of finite strings of natural numbers; but to take the Kleene-Brouwer order of a tree, we need an appropriate lateral ordering on the nodes, coming from a well-ordering of the "symbols." So fix in the background some appropriate way of viewing the trees below as subsets of $\omega^{<\omega}$.
$T_A$ is defined as follows. A node of length $k$ on $T_A$ is a four-tuple $(s, l, w, n)$ such that:
$s$ is a $k$-shuffle (which builds part of a possibly-different $\omega$-copy $B$ from the $\omega$-copy $A$)
$l$ is a finite linear order with domain $\{0, 1, ..., k-1\}$ (which describes the node's guess as to the ordering of the copy of $\alpha$ built by the copy of $\mathfrak{A}$ our shuffle produces from $A$)
$w\in\omega^k$ (which is a partial witness to the correctness of $l$ above)
$p\in\omega^k$ (which isn't doing anything except to "pad out" the tree, to guarantee that $S_A$ embeds into $S_B$ for any pair of $\omega$-copies $A, B$; I don't think this is necessary but it clears out a possible problem), and
$w$ has not been seen at stage $k$ to fail to be a witness to $l\subset\varphi(-, s(A))$. Note that by the Normal Form Theorem, we may take the matrix $\psi$ of $\varphi$ to be $\Pi^0_1$ so this makes sense; even if it were higher arithmetic, we could still make this work by having our node contain "more data" - specific guesses about the relevant witnesses.
The ordering on $T_A$ is the obvious one. Note that $T_A$ is uniformly computable from $A$.
Now we build a well-founded tree $S_A$ associated to the (very ill-founded) tree $T_A$. Namely, a node on $S_A$ of length $n$ is a sequence of pairs $\langle \sigma_i, \tau_i\rangle_{i<n}$ such that
$\sigma_i=(s_i, l_i, w_i, p_i)$ is a node on $T_A$ with $\sigma_0<\sigma_1<...$, and
$\tau_i$ is a descending sequence in $l_i$ of length $i$.
Note that $S_A$ is again uniformly computable from $A$, and that $S_A$ is wellfounded since any infinite path would represent an infinite descending sequence in the copy of $\alpha$ built from the relevant copy of $A$. Finally, let $\beta_A$ be the ordertype of the Kleene-Brouwer ordering of $S_A$.
Because of the padding coordinate $p$, it's easy to see that $S_A$ embeds into $S_B$ for any two $\omega$-copies $A, B$ of $\mathfrak{A}$; so $\beta_A=\beta_B=\beta$. And the tree of descending sequences in $\alpha$ embeds into $S_A$, so $\beta\ge\alpha$. Since taking Kleene-Brouwer orderings is computable, we're done. $\quad\Box$
It should be clear at this point why I don't want to include the proof - it's a bit lengthy but doesn't really involve anything non-easy.
It's only borderline relevant, but I've added the "descriptive set theory" tag because of the tangential connection to $\Sigma^1_1$ bounding; I could see this result being stated in a descriptive set theory paper on the more model-theoretic side.
