NP completeness over reals

I am studying the BSS model of computation recently (cf. for instance Complexity and Real Computation; Blum, Cucker, Shub, Smale.)

For reals $R$, it is shown that, given a system of polynomials $f_1,\cdots, f_m\in R[x_1, \cdots, x_n]$, the existence of zeros is $NP_R$-complete. However, I am wondering, if those $f$'s are polynomials only have integer coefficients, i.e., $f_1,\cdots, f_m\in Z[x_1, \cdots, x_n]$, is still the problem $NP_R$-hard? (it is obviously in $NP_R$).

I suspect yes, but is there a simple proof?

I think the answer is no, assuming $\mathsf{P}_{\mathbb{R}} \neq \mathsf{NP}_{\mathbb{R}}$ (I believe I give a proof below, but there are enough potentially nitpicky definitional issues here that I'm being cautious about my claims).
Proof that the answer is no assuming $\mathsf{P}_\mathbb{R} \neq \mathsf{NP}_{\mathbb{R}}$: In fact, I believe the following stronger statement holds:
Lemma: For any BSS decision problem $L$ over $\mathbb{R}$, if $L$ poly-time-BSS$_{\mathbb{R}}$ reduces to a problem on integer inputs, then $L \in \mathsf{P}_\mathbb{R}$.
Proof of lemma: Suppose there were a polynomial-time BSS$_{\mathbb{R}}$ reduction from $L$ to a problem on integer inputs, given by a machine $M$. For inputs consisting of $n$ real parameters, unroll the computation of $M$ into an algebraic computation tree. There are only finitely many leaves, and the result at each leaf is a single rational function in the input parameters. In order for a rational function of real inputs to always output an integer value, it must be a constant function, and therefore not depend on the input. However, which constant function is used at each leaf can, of course, depend on the branches. However, since $M$ is a uniform machine, there can be only $O(1)$ output nodes, and thus only $O(1)$ output values. Thus $M$ can be trivially modified to in fact decide $L$ in polynomial time. QED
Now, take $L$ to be real feasibility of real polynomials. If $\mathsf{P}_{\mathbb{R}} \neq \mathsf{NP}_{\mathbb{R}}$, then $L \notin \mathsf{P}_{\mathbb{R}}$, and by the Lemma there is no reduction from $L$ to any problem on integer inputs (in particular, to real feasibility of integer polynomials).
Promise problem issue?: Another potential issue with your question is that real feasibility of integer polynomials may not be in $\mathsf{NP}_{\mathbb{R}}$, but only in its promise version. The issue here is that to verify that an input (such as the coefficient of a polynomial $f_i$) is an integer takes time that depends on the magnitude of $x$, whereas the set of instances (all instances, not just yes-instances) for an $\mathsf{NP}_{\mathbb{R}}$ decision problem should be decidable in $\mathsf{P}_\mathbb{R}$, the latter meaning that it takes polynomial time in the number of parameters, and not their magnitudes. This is, I believe, closely related to the fact that the integers are not first-order definable within the reals. (Essentially the best a BSS$_{\mathbb{R}}$-machine can do to test if an input $x$ is an integer is to compute the integer part of $x$ by computing powers of $2$ and doing "binary search." Once it's computed the integer part of $x$, it just checks whether that is equal to $x$.) So I think the probleam of real feasibility of integer equations is in $\mathsf{PromiseNP}_{\mathbb{R}}$ but probably not in $\mathsf{NP}_{\mathbb{R}}$ (or at least it seems nontrivial to prove that it is in $\mathsf{NP}_{\mathbb{R}}$).