Multivariate ultrametric root counting

Let $K$ be a field, complete with respect to a discrete non-archimedian valuation and let $k$ be the residue field. Consider a system $F$ of $n$ polynomial equations in $K\vars$. Our first result is a reformulation of the classical Hensel's Lemma in the language of tropical geometry: we show sufficient conditions (semiregularity at $w$) that guarantee that the first digit map $\delta:(K^\ast)^n\to(k^\ast)^n$ is a one to one correspondence between the solutions of $F$ in $(K^\ast)^n$ with valuation $w$ and the solutions in $(k^\ast)^n$ of the initial form system ${\rm in}_w(F)$. Using this result, we provide an explicit formula for the number of solutions in $(K^\ast)^n$ of a certain class of systems of polynomial equations (called regular), characterized by having finite tropical prevariety, by having initial forms consisting only of binomials, and by being semiregular at any point in the tropical prevariety. Finally, as a consequence of the root counting formula, we obtain the expected number of roots in $(K^\ast)$ of univariate polynomials with given support and random coefficients.