Lubin's formal-group conjecture for commuting p-adic power series

Let $\mathfrak{f}$ and $\mathfrak{u}$ be a non-invertible and a non-torsion invertible series, respectively, defined over the ring of integers $\mathcal{O}$ of a finite extension of $\mathbf{Q}_p$. Suppose that the roots of $\mathfrak{f}$ and all of its iterates are simple, and that $\mathfrak{f}'(0)$ is a uniformizer in $\mathcal{O}$. Lubin's conjecture. If

$$\mathfrak{f}\circ \mathfrak{u}=\mathfrak{u}\circ \mathfrak{f},$$

then there is a formal group law $F/\mathcal{O}$ such that

$$\mathfrak{f},\mathfrak{u}\in\operatorname{End}_{\mathcal{O}}(F).$$

The conjecture seeks to make precise Lubin's philosophy that a formal group should underlie commuting non-invertible and non-torsion invertible power series. The preliminary assertion that the formal group associated to an invertible series is defined over $\mathbf{Z}_p$ is false, with counterexamples known over finite extensions; the stated integrality criterion remains unresolved in the supplied source.