Does quantifier elimination (by cylindrical decomposition) work for systems of polynomial equations and inequalities where some or all of the variables are complex numbers of unit modulus, rather than being real numbers? If it works in principle - has it been implemented?
Addendum: of course it works in principle, but can it be made to work in practice, i.e., without doubling the number of variables? (Cylindrical decomposition has doubly exponential complexity on the number of variables.)