Conjectural tropical analog of Descartes' rule of signs

Let $P(x)=\sum_{k=0}^d a_kx^k$ be a real univariate polynomial, and define the tropical polynomial associated to $P$ by

$$tr^\dagger_P(\xi)=\max_{0\le k\le d}(k\xi+\ln|a_k|-k^2),\qquad \xi\in\mathbb R,$$

where the weights are given by $\lambda_k^\dagger=e^{-k^2}$ for $k=0,1,\dots$. A positive or negative tropical root is understood to be an essential tropical root with the corresponding sign.

Conjectural tropical analog of Descartes' rule of signs. For any real univariate polynomial $P(x)$, the number of its positive (negative) roots does not exceed the number of positive (negative) essential tropical roots of $tr^\dagger_P(\xi)$.

This conjecture proposes a tropical analogue of Descartes' rule of signs for the fixed rapidly decreasing weight sequence $\lambda_k^\dagger=e^{-k^2}$. The preceding results establish sufficient and necessary-type log-concavity conditions for real-to-tropical root preservers, but do not settle this particular sequence.