Thank you for calling this problem to my attention.
I computed $K$ en route to AWS (though this year's
topics
are a rather different flavor of number theory...).
After some simplification (gp's $\rm polredabs$), it turns out that
the field $K$ is generated by a root of
$$
f(x) = x^{17} - 2x^{16} + 8x^{13} + 16x^{12} - 16x^{11} + 64x^9 - 32x^8 - 80x^7
$$
$$
\qquad\qquad\qquad {} + 32x^6 + 40x^5 + 80x^4 + 16x^3 - 128x^2 - 2x + 68.
$$
gp quickly confirms:
p = Pol([1,-2,0,0,8,16,-16,0,64,-32,-80,32,40,80,16,-128,-2,68])
poldegree(p)
F = nfinit(p);
factor(F.disc)
returns
[2 79]
So the field has discriminant $2^{79}$.
Let $F = {\bf Q}(\zeta_{64}^{\phantom{0}} - \zeta_{64}^{-1})$,
with $F/\bf Q$ cyclic of degree $16$ of $\bf Q$.
It was known that $K$ is contained in
an unramified cyclic extension $L/F$ of degree $17$.
Hence $L(\zeta_{17})$ is a Kummer extension of $F_{17} := F(\zeta_{17})$.
Now $F_{17}$ is a $({\bf Z} / 16 {\bf Z})^2$ extension of $\bf Q$.
Fortunately it was not necessary to work in the unit group
of this degree $256$ field: the Kummer extension is
$F_{17}(u^{1/17})$ with $u \in F_{17}^* / (F_{17}^*)^{17}$
in an eigenspace for the action of ${\rm Gal}(F_{17}/{\bf Q})$,
which makes it fixed by some index-$16$ subgroup of this Galois group.
Thus $u$ could be found in one of the cyclic degree-$16$ extension of $\bf Q$
intermediate between $\bf Q$ and $F_{17}$, and eventually a generator of $K$
turned up whose minimal polynomial, though large, was tractable enough for
gp's number-field routines to do the rest.
I remember working this out 25 years ago. The main idea is to view both rings as quotient rings of completions: $\mathcal O_K/\mathfrak p^e \cong \widehat{\mathcal O_{\mathfrak p}}/\widehat{\mathfrak p}^e$ and $k[t]/(t^e) \cong k[[t]]/(t^e)$. Then the structure of the ring of integers of local fields, in characteristic $0$ and characteristic $p$, will help us solve the problem.
For a nonzero prime ideal $\mathfrak p$ in $\mathcal O_K$ lying over $p$ and $m \geq 1$, the quotient ring $\mathcal O_K/\mathfrak p^m$ is unchanged up to isomorphism if we replace $\mathcal O_K$ by its localization at $\mathfrak p$ or by its completion at $\mathfrak p$ (and the modulus also changes to the ideal it generates in the localization or completion). Also, the ramification index $e = e(\mathfrak p|p)$ and residue field degree $f = f(\mathfrak p|p)$ are unchanged by localizing or completing at $\mathfrak p$.
Let $A = \widehat{\mathcal O_{\mathfrak p}}$ be the completion of $\mathcal O_K$ at $\mathfrak p$, so in $A$ we can write $p = \pi^e u$ for some uniformizer $\pi$ and $u \in A^\times$. Then
$\mathcal O_K/\mathfrak p^e \cong A/(\pi^e) = A/(p)$. (In this step it's important that the exponent $e$ is the ramification index of $\mathfrak p$ over $p$.) The ring $A$ is the ring of integers of the completion $K_\mathfrak p$. Even though $\mathcal O_K$ need not be monogenic, completions are monogenic: the ring of integers of every finite extension of $\mathbf Q_p$ has a power basis over $\mathbf Z_p$, so $A = \mathbf Z_p[\alpha]$ for some $\alpha \in A$. That there is a power basis over $\mathbf Z_p$ is the key fact you were missing.
Let $\alpha$ have minimal polynomial $F(x)$ in $\mathbf Z_p[x]$, so $F(x)$ is irreducible over $\mathbf Z_p$ and
$A \cong \mathbf Z_p[x]/(F(x))$ as rings. Viewing both sides as $\mathbf Z_p$-modules and computing their $\mathbf Z_p$-ranks shows $[K_\mathfrak p:\mathbf Q_p] = \deg F$, so
$$
\deg F = e(\mathfrak p|p)f(\mathfrak p|p) = ef.
$$
Using $F(x)$,
$$
\mathcal O_K/\mathfrak p^e \cong A/(p) = \mathbf Z_p[\alpha]/(p) \cong \mathbf Z_p[x]/(p,F(x)) \cong \mathbf F_p[x]/(\overline{F}(x)).
$$
The mod $p$ reduction $\overline{F}(x)$ in $\mathbf F_p[x]$ has a factorization into monic irreducibles. All monic irreducible factors of $\overline{F}(x)$ are the same, because if that were not the case then we could write $F(x) \equiv G(x)H(x) \bmod p$ for nonconstant monic $G(x)$ and $H(x)$ where $\gcd(G \bmod p,H \bmod p) = 1$ in $\mathbf F_p[x]$, and then by Hensel's lemma (the one about lifting relatively prime factorizations, not just about lifting a simple root) we'd get a factorization of $F(x)$ in $\mathbf Z_p[x]$ into nonconstant monic factors, which contradicts the irreducibility of $F(x)$ over $\mathbf Z_p$. So in $\mathbf F_p[x]$ we must have $\overline{F}(x) = Q(x)^d$ for some monic irreducible $Q(x)$ in $\mathbf F_p[x]$ and $d \geq 1$. That means
$$
\mathcal O_K/\mathfrak p^e \cong A/(p) \cong \mathbf F_p[x]/(Q(x)^d)
$$
as rings.
We will now show
$$
d = e = e(\mathfrak p|p), \ \ \deg Q = f = f(\mathfrak p|p).
$$
Let $k = \mathcal O_K/\mathfrak p$, which is the residue field of $\mathcal O_K$ at $\mathfrak p$, so $\dim_{\mathbf F_p}(k) = f$ by definition. Residue fields are unchanged up to isomorphism by completion, so $k \cong A/(\pi)$. The local ring $A/(p) = A/(\pi^e)$ has maximal ideal $(\pi)/(\pi^e)$ and residue field $A/(\pi)$, while the local ring $\mathbf F_p[x]/(Q(x)^d)$ has maximal ideal $(Q(x))/(Q(x)^d)$ and residue field $\mathbf F_p[x]/(Q(x))$. Isomorphic local rings have isomorphic residue fields, so $k \cong \mathbf F_p[x]/(Q(x))$. Computing $\mathbf F_p$-dimensions of both sides,
$$
f = \deg Q.
$$
Returning to $F$, which is monic and reduces mod $p$ to $Q(x)^d$, we can now say
$$
\deg F = \deg \overline{F} = d\deg Q = d f
$$
and we already saw $\deg F = ef$, so
$$
d = e.
$$
Thus
$$
\mathcal O_K/\mathfrak p^e \cong A/(p) \cong \mathbf F_p[x]/(Q(x)^e), \ \ \deg Q = f.
$$
The last step is to show $\mathbf F_p[x]/(Q(x)^e) \cong k[t]/(t^e)$ as rings, so
$$
\mathcal O_K/\mathfrak p^e \cong A/(p) \cong \mathbf F_p[x]/(Q^e) \cong k[t]/(t^e).
$$
In fact we'll show
$$
\mathbf F_p[x]/(Q(x)^m) \cong k[t]/(t^m)
$$
for all $m \geq 1$. We need $m = e$ only to identify these rings with $\mathcal O_K/\mathfrak p^e$, but the rings are isomorphic to each other for all $m \geq 1$. (Note $\mathcal O_K/\mathfrak p^m$ has characteristic $p$ if and only if $\mathfrak p^m \mid p\mathcal O_K$, forcing $m \leq e$, but the rings $\mathbf F_p[x]/(Q(x)^m)$ and $k[t]/(t^m)$ have characteristic $p$ for all $m \geq 1$, so there's nothing unusual about them winding up as isomorphic to each other for all $m$.) I will describe two methods, the first one being more concrete.
Method 1: The elements of $k[t]/(t^m)$ are uniquely expressible as
$$
c_0 + c_1t + \cdots + c_{m-1}t^{m-1} \bmod t^m
$$
with $c_j \in k$. Inside $\mathbf F_p[x]/(Q^m)$, the elements are uniquely expressible as
$$
a_0(x) + a_1(x)Q(x) + \cdots + a_{m-1}(x)Q(x)^{m-1}
$$
with $a_j(x) = 0$ or $\deg(a_j(x)) < \deg Q$. But this way of writing the elements of $\mathbf F_p[x]/(Q^m)$ is terrible in order to set up a ring isomorphism with $k[t]/(t^m)$ since those base $Q$ digits $a_j(x)$ are not multiplicatively closed (in contrast to the $c_j$ in $k$). What we need to do is find a copy of the field $k$ of order $p^f$ inside $\mathbf F_p[x]/(Q^m)$.
The polynomial $t^{p^f} - t$ splits completely over the field $\mathbf F_p[x]/(Q)$, so for each $m \geq 1$ the $Q$-adic Hensel's lemma tells us we can lift each of those roots mod $Q$ uniquely to a root of $t^{p^f}-t$ in $\mathbf F_p[x]/(Q^m)$. Set
$$
k_m := \{b(x) \bmod Q^m : b(x)^{p^f} \equiv b(x) \bmod Q^m\},
$$
which is the roots of $t^{p^f}-t$ in $\mathbf F_p[x]/(Q^m)$. This set is closed under addition and multiplication and each nonzero element is invertible: if $b(x) \not\equiv 0 \bmod Q^m$ then $b(x) \not\equiv 0 \bmod Q$ (the only lift of $0 \bmod Q$ as a root is $0 \bmod Q^m$), so $\gcd(b(x),Q^m) = 1$. So $k_m$ is a field of order $p^f$ inside $\mathbf F_p[x]/(Q^m)$ and in fact it's the only such field inside $\mathbf F_p[x]/(Q^m)$ thanks to the unique lifting of roots of $t^{p^f}-t$ from modulus $Q$ to modulus $Q^m$.
Since $k_m$ inside $\mathbf F_p[x]/(Q^m)$ is a set of representatives for $\mathbf F_p[x]/(Q)$, we can write every element of $\mathbf F_p[x]/(Q^m)$ uniquely as
$$
b_0(x) + b_1(x)Q(x) + \cdots + b_{m-1}(x)Q(x)^{m-1} \mod Q(x)^m
$$
where $b_j(x) \bmod Q(x)^m \in k_m$. This way of writing
the elements of $\mathbf F_p[x]/(Q^m)$ looks just like the usual way of writing the elements of $k[t]/(t^m)$ and it shows $k_m[Q \bmod Q^m]$ fills up $\mathbf F_p[x]/(Q^m)$
Since $k$ and $k_m$ are fields of equal size $p^f$ there is a field isomorphism $\varphi_m \colon k \to k_m$ (in fact there are $m$ isomorphisms, but that doesn't matter). Extend $\varphi_m$ to a ring homomorphism $k[t] \to \mathbf F_p[x]/(Q^m)$ by mapping $t$ to $Q \bmod Q^m$:
$$
\sum_{i} c_it^i \mapsto \sum_i \varphi_m(c_i)Q^i \bmod Q^m.
$$
This is surjective since $\mathbf F_p[x]/(Q^m)$ is generated as a ring by $k_m$ and $Q \bmod Q^m$. Since $t^m \mapsto Q^m \bmod Q^m = 0$, we get an induced surjective ring homomorphism $k[t]/(t^m) \to \mathbf F_p[x]/(Q^m)$. Both have order $p^{fm}$, so this is a ring isomorphism.
Method 2: Since $Q$ is irreducible in $\mathbf F_p[x]$, the ring $\mathbf F_p[x]/(Q^m)$ is unchanged up to isomorphism if we replace $\mathbf F_p[x]$ with its $Q$-adic completion $\mathbf F_p[x]_Q$:
$$
\mathbf F_p[x]/(Q^m) \cong \mathbf F_p[x]_Q/(Q^m)
$$
as rings.
The residue field of $\mathbf F_p[x]_Q$ is isomorphic to $\mathbf F_p[x]/(Q)$, which is isomorphic to $k$. The completion $\mathbf F_p[x]_Q$ is the ring of integers of the $Q$-adic field completion $\mathbf F_p(x)_Q$, and the structure of local fields of positive characteristic says they are all isomorphic to the formal Laurent series field over the residue field. Thus $\mathbf F_p(x)_Q \cong k((t))$ as valued fields, so their rings of integers are isomorphic: $\mathbf F_p[x]_Q \cong k[[t]]$. The isomorphism identifies powers of the maximal ideal on both sides,
and the maximal ideal of $\mathbf F_p[x]_Q$ is $(Q)$ since $Q$ is a uniformizer in the $Q$-adic completion. Thus
$$
\mathbf F_p[x]_Q/(Q^m) \cong k[[t]]/(t^m)
$$
for each $m \geq 1$. Both sides simplify to quotient rings of $\mathbf F_p[x]$ and $k[t]$, just as $\mathbf Z_p/(p^m) \cong \mathbf Z/(p^m)$:
$$
\mathbf F_p[x]/(Q^m) \cong k[t]/(t^m).
$$
Here is an illustration of Method 1.
Example. Let $Q(x) = x^2 - 2$ in $\mathbf F_5[x]$. Then
$\mathbf F_5[x]/(Q^3) \cong \mathbf F_{25}[t]/(t^3)$. To write down an explicit ring isomorphism we need a copy of $\mathbf F_{25}$ in $\mathbf F_5[x]/(Q^3)$. We can view $\mathbf F_{25}$ as $\mathbf F_5(\alpha)$ where $\alpha^2 = 2$. One root of $t^2 - 2$ in $\mathbf F_5[x]/(x^2-2)$ is $x \bmod x^2-2$, and the unique lifting of this to a root of $t^2 - 2$ in $\mathbf F_5[x]/(Q^3)$ is
$$
r = x + xQ + 4xQ^2 = x + x(x^2-2) + 4x(x^2-2)^2 \bmod Q^3
$$
by an explicit search.
Therefore the copy of $\mathbf F_{25}$ inside $\mathbf F_5[x]/(Q^3)$ is $\mathbf F = \mathbf F_5 + \mathbf F_5r$ and
$$
\mathbf F_5[x]/(Q^3) = \mathbf F + \mathbf F Q + \mathbf F Q^2 \bmod Q^3.
$$
The right side naturally looks like $\mathbf F_{25}[t]/(t^3)$ and we get an isomorphism $\mathbf F_{25}[t]/(t^3) \to \mathbf F_5[x]/(Q^3)$ once we decide on an isomorphism between $\mathbf F_{25}$ and $\mathbf F$.
Best Answer
Lemma. Let $K$ be any number field, and $p$ a prime unramified in $K$. Then $X^n-p$ is irreducible over $K$.
Proof. It suffices to show that the field $L = K(\sqrt[n\ \ ]{p})$ has degree $n$ over $K$. Let $\mathfrak q \subseteq \mathcal O_L$ be a prime above $p$, and let $\mathfrak p = \mathcal O_K \cap \mathfrak q$ be its image in $\operatorname{Spec} \mathcal O_K$. Since $\mathcal O_L$ contains $\mathbf Z[\sqrt[n\ \ ]{p}]$, we have $e_{\mathfrak q/p} \geq n$. But $K$ is unramified above $p$, so $e_{\mathfrak p/p} = 1$. We conclude that $e_{\mathfrak q/\mathfrak p} = n$, so $[L:K] \geq n$. The reverse inequality is clear. $\square$