I'm trying to find a way to numerically ensure that two constructible numbers are equal (this would be done by a computer).
The idea is to find a polynomial $p(x)$ that contains both numbers as roots (I already have a method to do so), then use following Lemma to obtain a minimal distance $d$ between two roots of $p(x)$, so it would be sufficient to check if the distance between them is less than $d$ to conclude that they are equal.
Lemma (Mahler, 1964). If $p(x)=a_0\prod_{i=1}^{n}(x-\alpha_i)\in\mathbb Z[x]$ is separable and $n\geq 2$, then, for any distinct roots $\alpha_i$ and $\alpha_j$, $$ |\alpha_i-\alpha_j|> \sqrt{3}n^{-(n+2)/2}|D(p)|^{1/2}M(p)^{-(n-1)}, $$ where $D(p)=a_0^{2n-2}\displaystyle\prod_{1\leq i<j\leq n}(\alpha_i-\alpha_j)^2$ and $M(p)=|a_0|\prod_{i=1}^n\max\{1,|\alpha_i|\}$.
The first thing I noticed really fast is that $p(x)$ need not to be separable if we have the care to compute the product of $D(p)$ with different roots only.
The second thing is that, when we open the definitions of $D(p)$ and $M(p)$, the term $a_0$ disappears (which is good for computational purposes). Consequently, $p(x)$ need only to be at $\mathbb Q[x]$.
So actually, for any polynomial $\displaystyle p(x)=\prod_{i=1}^n(x-\alpha_i)\in\mathbb Q[x]$ and any distinct roots $\alpha_k$ and $\alpha_l$, we have $$ |\alpha_k-\alpha_l|> \sqrt{3}n^{-(n+2)/2}\left(\displaystyle\prod_{1\leq i<j\leq n\\ \ \ \ \alpha_i\neq\alpha_j}|\alpha_i-\alpha_j|\right)\left(\prod_{i=1}^n\max\{1,|\alpha_i|\}\right)^{-(n-1)}, $$
My question: Is there a more powerful result concerning the minimal distance between roots of rational polynomials?
