Solution (source code)

= Solution

The compactness and completeness proved above apply again. The finite ring $\mathcal O/t\mathcal O$ has a positive integer characteristic $m$, so $m\in t\mathcal O$ and $|m|<1$. Prime factorization supplies a prime $p$ with $|p|<1$. In characteristic zero the restriction to $\mathbb Q$ is therefore a positive power of the <p-adic absolute value>, by the preceding classification. Completing $\mathbb Q$ embeds the <P-adic number> field $\mathbb Q_p$ into the complete field $K$.

Now $p\mathcal O$ is open, so $\mathcal O/p\mathcal O$ is finite. It is an $\mathbb F_p$-vector space; choose lifts $e_1,\ldots,e_d\in\mathcal O$ of a basis. Successively reducing modulo $p\mathcal O$ gives, for every $x\in\mathcal O$,
$$
x=\sum_{n\geq0}p^n\sum_{j=1}^d a_{j,n}e_j=\sum_{j=1}^d c_j e_j,\qquad a_{j,n}\in\{0,\ldots,p-1\},\quad c_j=\sum_{n\geq0}a_{j,n}p^n\in\mathbb Z_p.
$$
Convergence in $K$ follows from $|p|<1$. Every element of $K$ becomes integral after multiplication by a power of $p$, so $K=\sum_j\mathbb Q_p e_j$. \b[Consequently $\boxed{[K:\mathbb Q_p]<\infty}$: $K$ is a <p-adic field>.] This finite-module proof does not assume discreteness of the original value group in advance.