Lubin's formal-group conjecture for commuting power series

Let $K$ be a finite extension of $\mathbf{Q}_p$, with ring of integers $\mathcal{O}_K$ and maximal ideal $\mathfrak{m}_K$. Let $P,U\in T\cdot\mathcal{O}_K[[T]]$ satisfy

$$P\circ U=U\circ P,$$

with $P'(0)\in\mathfrak{m}_K$, $U'(0)\in\mathcal{O}_K^\times$ not a root of unity, and $P(T)\not\equiv 0\pmod{\mathfrak{m}_K}$. A formal group means a formal group law over the indicated ring, and $P_S$ and $U_S$ denote endomorphisms of such a formal group $S$. Lubin's conjecture. There exists a finite extension $E/K$, a formal group $S$ defined over $\mathcal{O}_E$, endomorphisms $P_S$ and $U_S$ of $S$, and a power series $h(T)\in T\mathcal{O}_E[[T]]$ such that

$$P\circ h=h\circ P_S,\qquad U\circ h=h\circ U_S.$$

The conjecture formalizes the expectation that an invertible power series commuting with a noninvertible one arises from a formal group in the background. Several cases were previously known, and the paper proves the conjecture in a new case; the general assertion stated here is not presented as fully resolved.