A minimal complex differential equation descends to the series coefficient field

Let $K$ be a field embedded in $\mathbb C$, and let $f\in K[[X]]$. Suppose the image of $f$ in $\mathbb C[[X]]$ has a minimal polynomial differential equation $L$ of order $n$. Then it has a minimal equation of order $n$ with coefficients in $K[X]$. One coefficient of its leading polynomial can moreover be normalized to one.

Choose a nonzero coefficient $c$ in the leading polynomial of $L$, and a $K$-linear functional $\sigma:\mathbb C\to K$ taking $c$ to one. Apply $\sigma$ coefficientwise to all coefficient polynomials of $L$. Every formal coefficient equation is $K$-linear, so the projected operator still annihilates $f$. Its leading polynomial is nonzero by the chosen normalization. Mapping the equation back to $\mathbb C$ gives the same order $n$, and minimality excludes every smaller equation.

The proof does not require $K/\mathbb Q$ to be algebraic, or convergence or arithmetic bounds on $f$. In the E-function application, it justifies working over the actual arithmetic coefficient field rather than assuming that a complex minimal operator already has arithmetic coefficients.