The Hasse–Arf theorem for mixed-characteristic ramification filtrations

Let $K$ be a complete discretely valued field of mixed characteristic $(0,p)$, and let $\rho:G_K\rightarrow GL(V_\rho)$ be a representation with finite local monodromy. The Artin and Swan conductors are defined by the ramification filtrations, and for $a\geq 0$ the quotients $\mathrm{Fil}^aG_K/\mathrm{Fil}^{a+}G_K$ and $\mathrm{Fil}^a_{\mathrm{log}}G_K/\mathrm{Fil}^{a+}_{\mathrm{log}}G_K$ are the corresponding ramification subquotients. Hasse–Arf theorem. (1) $\mathrm{Art}(\rho)$ and $\mathrm{Swan}(\rho)$ are non-negative integers, and (2) the subquotients

$$\mathrm{Fil}^aG_K/\mathrm{Fil}^{a+}G_K\quad\text{and}\quad\mathrm{Fil}^a_{\mathrm{log}}G_K/\mathrm{Fil}^{a+}_{\mathrm{log}}G_K$$

are abelian groups killed by $p$. This extends the integrality and structural conclusions of the Hasse–Arf theorem to the mixed-characteristic setting considered here; the supplied text does not state whether the result was subsequently proved, so its database status is left open.