Constructive Proof to Show that Algebraic Numbers are Algebraically Closed

EDIT2: After reading some papers, I think the question can best be rephrased as "How can the minimal polynomial for a polynomial with algebraic coefficients be calculated. I have seen papers and textbooks that show that algebraic numbers are algrebraically closed, but I haven't seen a constructive proof.

Let $f_n,f_{n-1},...,f_0$ be univariate polynomials with rational coefficients. For each $f_i$, assume that we have successfully isolated a root $\lambda_i$ via Sturm's Theorem as the only root within the range $[\lambda_i^-,\lambda_i^+]$.

Define $g$ as the univariate polynomial:

$$g(x) = \lambda_nx^n + \lambda_{n-1}x^{n-1} + ... + \lambda_0$$

Is it possible to isolate the zeros of $g$? Specifically, is it possible to determine if $g$ has repeated roots?

I asked a somewhat similar question here in which each $\lambda_i$ is represented as an interval whose size can be shrunk arbitrarily (but not shrunk to a single point). Alex Degtyarev correctly pointed out that the problem cannot be solved if the values of $\lambda_i$ are not known exactly.

However, in this instance, the values are known exactly. Unfortunately, I'm missing how the rational coefficients of the $f_i$ can be incorporated in an algorithm to isolate the roots of $g$.

Thanks for any help.

EDIT: Since posting the question, I've read a bit on Galois Theory, and it looks like this problem can be solved, although I'm still trying to figure out exactly how. I've figured out algorithms to find the minimal polynomial for sums and products of algebraic numbers. I still haven't found a algorithm to determine the minimal polynomial for a polynomial with algebraic coefficients although I have found a proof that such a polynomial exists.

• Are you sure this is not related to the recently famous story of interlacing polynomials? – Anirbit Nov 10 '14 at 2:44
• I'm sorry, my background is in computer science, so I'm not up to date with the latest mathematical headlines. I'll google "interlacing polynomials" and see what I can find. – Ashwin Deshpande Nov 10 '14 at 2:46
• Infact interlacing polynomials became big because of CS people! Look at Terence Tao's review of the solution to the Kadison-Singer conjecture. It was proven by Nikhil Srivastava, Daniel Spielman and Adam Marcus. – Anirbit Nov 10 '14 at 2:49
• Can you explain why do you need this? I am curious - since I too think of such stuff these days! – Anirbit Nov 10 '14 at 2:53
• I'm working on an iterated cylindrical algebraic decomposition approach to prove decidability for robotic task and motion planning. Previously, people have only considered 1 round of c.a.d., which means that all polynomial coefficients are rational. In my approach, from the second round of c.a.d. on, the coefficients will be algebraic numbers in general. – Ashwin Deshpande Nov 10 '14 at 2:59

I found a constructive proof. It will be odd to use cylindrical algebraic decomposition (with rational polynomial coefficients) as a sub-algorithm for cylindrical algebraic decomposition (with algebraic polynomial coefficients), but it appears to work.

• There might be some theory in perso.univ-rennes1.fr/marie-francoise.roy/bpr-ed2-posted1.html To my knowledge, quantifier elimination has really nasty complexity. – Per Alexandersson Nov 10 '14 at 9:10
• Thanks for the link. I know the horrible complexity of quantifier elimination all too well. Without getting into the parameteric details, the tentative run-time of my task and motion decidability result looks like $\omega(2^{2^{(2 \uparrow \uparrow k)^{(2 \uparrow \uparrow k)}}})$, but decidability is decidability. – Ashwin Deshpande Nov 10 '14 at 10:13
• I found a great paper outlining an explicit algorithm to solve the problem (link). – Ashwin Deshpande Nov 10 '14 at 10:17

You can have a look at the constructive proof provided by the Mathematical Components libraries, you will find further references in the comments.

http://ssr.msr-inria.inria.fr/doc/mathcomp-1.5/MathComp.algebraics_fundamentals.html

There is also a lot of documentation in Cyril's Cohen PhD thesis.

Best, E