Our construction of $(X^{an},\Omega)$ works even without the assumption $char\,k=0$ where $k$ is the residue field of $K$. This can be explained from the point of view of factorization theorem (see Section 10.4). It turns out that symplectomorphisms which appear in the infinite product in the RHS of the factorization theorem are infinite series whose coefficients are integer polynomials in the coefficients of the “parent” symplectomorphisms.

For example, let $f_{0}(z)=1+\sum_{n\geq 1}c_{n}z^{n}$ and $f_{\infty}(z)=1+\sum_{n\geq 1}d_{n}z^{n}$ be two power series convergent when $|z|<1$. Let us consider two symplectomorphisms: $F_{0}(\xi,\eta)=(\xi,\eta f_{0}(\xi^{-1}))$ and $F_{\infty}(\xi,\eta)=(\xi f_{\infty}(\eta^{-1}),\eta)$ and decompose $F_{\infty}\circ F_{0}$ into the infinite ordered product $\prod_{\to}(F_{\lambda})$. Here

$$F_{p/q}(\xi,\eta)=(\xi f_{p/q}(\xi^{-p}\eta^{-q})^{q},\eta f_{p/q}(\xi^{-p}\eta^{-q})^{-p})$$

where $f_{p/q}(z)=1+\sum_{n\geq 1}c_{n}^{p/q}z^{n}$. Then one can check that for any coprime $p,q\in{\bf Z}_{>0}$ and any $n\geq 1$ one has

$$c_{n}^{p/q}\in{{\bf Z}}[c_{1},c_{2},\dots,d_{1},d_{2},\dots]\,\,.$$

This implies that our construction works when one replaces $K$ by arbitrary commutative ring $R$ endowed with a complete non-trivial valuation $val:R\to(-\infty,+\infty]$.