[step:Set up the reduction $\mathbb{K} \leq_m \operatorname{Fin}$ via a timed halting gate]
To show $\operatorname{Fin} \notin \Pi_1$, we construct a reduction $\mathbb{K} \leq_m \operatorname{Fin}$. (Rice's theorem only gives $\mathbb{W} \setminus \mathbb{K} \leq_m \operatorname{Fin}$, which is in the wrong direction for $\Pi_1$-ness.) The construction inverts the pattern: instead of making $W_{h(w)}$ all-or-nothing, we make $W_{h(w)}$ finite-or-infinite, with finite when $w \in \mathbb{K}$ and infinite when $w \notin \mathbb{K}$.
We use the timed simulation function of [Computability of the Configuration Function](/theorems/1818): for each register machine $M$ of arity $1$ there is a total computable function
\begin{align*}
t_{M} : \mathbb{W}^2 &\to \mathbb{W}, \\
(v, u) &\mapsto \begin{cases} a & \text{if $M$ on input $v$ halts in at most $\#u$ steps}, \\ \varepsilon & \text{otherwise}, \end{cases}
\end{align*}
where $\#u$ is the shortlex index of $u$ (see [Shortlex Is Order-Isomorphic to $\mathbb{N}$](/theorems/1815)). For $w \in \mathbb{W}$, write $t_{w, 1}(v, u) := t_{M_w}(v, u)$ where $M_w$ is the register machine with code $w$. The assignment $w \mapsto t_{w, 1}$ is uniformly total computable: there is a single total computable $t : \mathbb{W}^3 \to \mathbb{W}$ with $t(w, v, u) = t_{w, 1}(v, u)$, by [Computability of the Configuration Function](/theorems/1818) combined with the uniform coding of register machines.
Define
\begin{align*}
g : \mathbb{W}^2 &\rightharpoonup \mathbb{W}, \\
(v, w) &\mapsto \begin{cases} \uparrow & \text{if } t(w, w, v) = a, \\ \varepsilon & \text{if } t(w, w, v) = \varepsilon. \end{cases}
\end{align*}
[claim:$g$ is computable]
A register machine $M_g$ witnessing $g$ runs on input $(v, w)$ as follows:
(a) Invoke the total computable $t : \mathbb{W}^3 \to \mathbb{W}$ on $(w, w, v)$: build the triple by pairing and copy primitives (total computable, L2 of Step 4 of the proof of [Recursive Implies Computable](/theorems/1817)), then run the register machine for $t$.
(b) Case-distinguish on the output (total computable primitive, L2): if the output is $\varepsilon$, halt with $\varepsilon$ in register $0$; if the output is $a$, enter an immediate infinite loop.
This matches the definition of $g$. Formally, $g = \mathrm{cd} \circ t \circ \sigma$, where $\sigma : \mathbb{W}^2 \to \mathbb{W}^3$, $(v, w) \mapsto (w, w, v)$ is total computable (pairing and copy primitives) and $\mathrm{cd} : \mathbb{W} \rightharpoonup \mathbb{W}$ sends $\varepsilon \mapsto \varepsilon$ and $a \mapsto \uparrow$ (computable by L2). Composition preserves computability of partial functions (L1).
[/claim]
[/step]