A Universe of Sorts

Explain by example. Let floating point number $f = 1.4142$ .
Clearly, this has a minpoly of $10000x - 14142 = 0$ with coefficients in $Z[x]$ .
However, we know that the correct minpoly is $x^2 - 2 = 0$ .
What's the difference in these two cases? Well, the correct minpoly has "small" coefficients.
How do we find such a minpoly using LLL?
Key idea: Build vectors (in our case) of the form $b_0 \equiv (1, 0, 0, 1000)$ , $b_1 \equiv (0, 1, 0, 1000f)$ , and $b_2 \equiv (1000f^2)$ . Then LLL, on trying to find a shorter basis for these, will try very hard to make the third component smaller. It will do this by changing the basis vectors to $b'_0 \equiv b_0, b'_1 \equiv b_1$ , and $b'_2 \equiv b_2 - 2b_0 = (-1, 0, 1, 1000(f^2 - 2)$ . Since $f^2 - 2 \sim 0$ , the length of $b'_2$ is much smaller than $b_2$ , granting us a shorter basis!
In general, given some rational number $\theta$ , we build n basis vectors v_i of dimension n+1of the form v_i[i] = 1, v_i[n] = 1000(θ^i), and v_i[-] = 0 otherwise.
LLLing on these vectors v_i will attempt to find an integer relation on the last coefficient, which will be the minpoly.

§ Using LLL to Discover Minimal Polynomial for Floating Point Number