Do all subtraction-free identities tropicalize?

It suffices to show that whenever $F$ is a function $\mathbb R_{\geq 0}^k\to\mathbb R_{\geq 0}$ defined using $\times,/,+,1$, and $f,g$ is the corresponding tropicalization $\mathbb R^k\to\mathbb R$, for all real $x_1,\dots,x_k$ we have $$F(\exp(-\beta x_1),\dots,\exp(-\beta x_k))^{1/\beta}\to \exp(-f(x_1,\dots,x_k)).$$ as $\beta\to+\infty$.

This follows by structural induction on the formula defining $f$, using the following lemma.

Lemma: Let $F$ be one of the operations $\times,/,+$, let $f$ be the corresponding tropical operation, and let $G_1$ and $G_2$ be functions $\mathbb R_{> 0}\to\mathbb R_{> 0}$ such that $G_1(\beta)^{1/\beta}$ tends to some limit $e^{-x_1}$ as $\beta\to\infty$, and likewise $G_2(\beta)^{1/\beta}\to e^{-x_2}$. Then $$F(G_1(\beta),G_2(\beta))^{1/\beta}\to \exp(- f(x_1,x_2)).$$ as $\beta\to+\infty$.

Proof: The operations $\times$ and $/$ are easy - the only non-trivial step is $$(G_1(\beta)+G_2(\beta))^{1/\beta}\to e^{-\beta \min(x_1,x_2)}.$$

Yes. Replace $x$ with $e^{-Na}$, $y$ with $e^{-Nb}$, etc. Then take the log, then divide by $N$. One gets a new identity where $\times$ is replaced by $+$, $/$ by $-$, $1$ by $0$, and $u+v$ by $-\ln (e^{-N u} + e^{-N v}) / N= \min(u,v) - \ln\left( 1+ e^{-N |u-v|}\right)/N = \min(u,v) + O(1/N)$. Then take the limit as $N$ goes to $\infty$. You now have a tropcal identity.

This fits with the idea of tropical geometry as the limit of classical algebraic geometry as variables get very large.