[step:Prove L3 — closure under minimisation]
Let $f : \mathbb{W}^{n + 1} \rightharpoonup \mathbb{W}$ be computable with witness machine $M_f$. The function $\mu f : \mathbb{W}^n \rightharpoonup \mathbb{W}$ is defined by
\begin{align*}
(\mu f)(w) &= \min\{v \in \mathbb{W} : f(w, v) = \varepsilon \text{ and } f(w, v') \downarrow \text{ for all } v' < v\},
\end{align*}
where $<$ is the shortlex order on $\mathbb{W}$ and "min" refers to the shortlex-minimum, which exists whenever the set is non-empty because $(\mathbb{W}, <)$ is well-ordered (see [Shortlex Order and Computable Successor](/theorems/1815)). If the set is empty (either because $f(w, v)$ is undefined at some $v$ before any $\varepsilon$ is found, or because no $\varepsilon$ value is ever produced), then $(\mu f)(w)$ is undefined.
We construct a machine $M_{\mu f}$ using a scratch register $k$ that enumerates $\mathbb{W}$ in shortlex order, starting at $\varepsilon$ and using the computable successor $s : \mathbb{W} \to \mathbb{W}$ whose computability is established in [Shortlex Order and Computable Successor](/theorems/1815).
*Register layout.* Input registers $0, \ldots, n - 1$ hold $w_1, \ldots, w_n$; we use scratch registers $R_1, \ldots, R_n$ to save a master copy, scratch register $k$ for the candidate, and we call $M_f$ and $M_s$ as sub-routines with their working registers disjoint from these (achievable by renaming register indices in $M_f$ and $M_s$).
*Phase 0: save inputs.* Copy $w_1, \ldots, w_n$ from registers $0, \ldots, n-1$ into $R_1, \ldots, R_n$. Initialise $k := \varepsilon$ (erase $k$).
*Phase 1: main loop.* Each iteration:
(1a) Restore $w_1, \ldots, w_n$ from $R_1, \ldots, R_n$ into the first $n$ input registers of $M_f$, and copy $k$ into the $(n+1)$-th input register. Run $M_f$. If $M_f$ diverges, $M_{\mu f}$ diverges (correct: for $(\mu f)(w)$ to be defined, $f(w, v')$ must be defined for every $v' \le $ the minimising $v$; divergence at the current $k$ means $f(w, k)$ is undefined, so either $k$ is not bounded above by the minimiser, or no minimiser exists). If $M_f$ halts, examine its output.
(1b) If the output of $M_f$ is $\varepsilon$, copy $k$ into register $0$ and halt. By the loop invariant below, $k$ at this point is the shortlex-least $v$ with $f(w, v) = \varepsilon$, i.e. $(\mu f)(w) = k$.
(1c) If the output is non-empty, replace $k$ by $s(k)$ using the computable successor $M_s$ (established in [Shortlex Order and Computable Successor](/theorems/1815)): copy $k$ into $M_s$'s input register, run $M_s$, copy its output back into $k$. Return to (1a).
The test "output is $\varepsilon$" in (1b) vs. "non-empty" in (1c) is the standard read-result case distinction on $M_f$'s output register: read the last letter once; if the read returns $\varepsilon$ the register was empty (halt), otherwise it returned some $a \in \Sigma$ (proceed; first write $a$ back to restore the output register before moving on, though actually in our context the output register of $M_f$ is going to be overwritten next iteration anyway, so we may just discard).
[claim:The loop in Phase 1 maintains the invariant "at the start of the iteration, $k$ is the shortlex-least word $v$ such that $f(w, v) \downarrow$ and $f(w, v)$ has not yet been observed to be $\varepsilon$, and for every $v' < k$ we have $f(w, v') \ne \varepsilon$ (and $f(w, v') \downarrow$)"]
The initial iteration starts with $k = \varepsilon$, the shortlex-minimum, and no previous values of $f$ have been queried, so the invariant holds vacuously (the set $\{v' : v' < \varepsilon\}$ is empty).
If the invariant holds at the start of an iteration, step (1a) evaluates $f(w, k)$. Three outcomes:
- $f(w, k)$ diverges: by the invariant, $f(w, v') \downarrow$ and $f(w, v') \ne \varepsilon$ for all $v' < k$. Since $f$ fails to be defined at $k$, the minimisation definition requires $(\mu f)(w)$ to be undefined (there is no $v$ with $f(w, v) = \varepsilon$ and $f$ defined on all smaller inputs, because at $k$ itself $f$ is undefined and $k$ is not greater than any such putative $v$ — more precisely, for $(\mu f)(w) = v$ we'd need $f(w, k) \downarrow$ either with $k = v$ where $f$ value is $\varepsilon$, or $k < v$ where $f$ value is arbitrary defined — but here $f$ is undefined at $k$, so neither works). $M_{\mu f}$ correctly diverges.
- $f(w, k) = \varepsilon$: by the invariant, for every $v' < k$ we have $f(w, v') \downarrow$ and $f(w, v') \ne \varepsilon$. So $k$ is the shortlex-least $v$ with $f(w, v) = \varepsilon$ and $f(w, v') \downarrow$ for all $v' < v$. Hence $k = (\mu f)(w)$, and step (1b) emits it.
- $f(w, k)$ is defined and non-empty: the invariant is updated to "$k' := s(k)$" in step (1c). Note $s(k)$ is the shortlex-successor of $k$, so words strictly less than $s(k)$ are precisely words $\le k$. For each such $v' \le k$ the invariant previously required $f(w, v') \downarrow$ and $f(w, v') \ne \varepsilon$ (for $v' < k$ by the old invariant, and for $v' = k$ by the current iteration's computation). So the invariant rewrites to $k'$ correctly.
By induction on the iteration index, the invariant is maintained.
[/claim]
[claim:If $(\mu f)(w) = v_0$, the loop exits at iteration where $k = v_0$, after finitely many iterations; if $(\mu f)(w)$ is undefined, the loop does not emit a value (it either diverges at some iteration or never terminates)]
*If $(\mu f)(w) = v_0$.* By definition $f(w, v') \downarrow$ for every $v' \le v_0$ and $f(w, v_0) = \varepsilon$. The loop enumerates $k = \varepsilon, s(\varepsilon), s(s(\varepsilon)), \ldots$, and by [Shortlex Order and Computable Successor](/theorems/1815) iterated application of $s$ starting from $\varepsilon$ visits every element of $\mathbb{W}$ in shortlex order, and in particular visits $v_0$ after finitely many iterations (precisely $\#(v_0)$ iterations, where $\#$ is the order isomorphism $\mathbb{W} \to \mathbb{N}$). At the iteration where $k = v_0$, step (1a) returns $\varepsilon$ and step (1b) halts with output $v_0$.
*If $(\mu f)(w)$ is undefined.* Two cases: either there is a shortlex-least $v^\dagger$ at which $f(w, v^\dagger) \uparrow$, in which case the loop enumerates up to $k = v^\dagger$ (after $\#(v^\dagger)$ iterations) and diverges in step (1a); or $f(w, v) \downarrow$ and is non-empty for every $v$, in which case the loop runs forever without emitting. Either way $M_{\mu f}$ does not halt, matching the undefinedness of $(\mu f)(w)$.
[/claim]
Hence $\mu f \in \mathcal{C}$.
[/step]