Solution (source code)

= Solution

For $a\in k$ and each $n$, choose a lift $x_n\in\mathcal O_K$ of the unique $p^n$th root $a^{p^{-n}}$, which exists because $k$ is a <perfect field>. Define
$$
[a]=\lim_{n\to\infty}x_n^{p^n}.
$$
Changing $x_n$ by an element of the maximal ideal changes its $p^n$th power by an element whose valuation tends to infinity, so the limit exists and is independent of all choices. In characteristic $p$, the <Frobenius endomorphism> satisfies $(x+y)^{p^n}=x^{p^n}+y^{p^n}$, making $[\mathord\cdot]$ a ring homomorphism lifting the identity on $k$. If $s:k\to\mathcal O_K$ is any other such section, then
$$
s(a)=s(a^{p^{-n}})^{p^n}
$$
for every $n$, and the same limiting construction forces $s(a)=[a]$. This proves uniqueness of the <Teichmuller lift>.

Choose a <uniformizer> $t$. Repeatedly subtracting the lift of the residue and dividing by $t$ gives every $x\in\mathcal O_K$ a unique convergent <Teichmuller expansion>
$$
x=\sum_{j\geq0}[a_j]t^j.
$$
Because the lift is a ring map, this identifies $\mathcal O_K$ with $k[[t]]$ and its fraction field with the <Laurent series field> $k((t))$. This is the <equal-characteristic complete discretely valued field> classification.

If $K$ is locally compact, its compact valuation ring has only finitely many disjoint residue-class balls. Thus $k$ is finite, as also follows from the <local compactness criterion for a complete non-Archimedean field>.