I am building on top of this question on MathOverflow.
The conclusion was that feasibility is decidable. Can one give a direct proof without using heavy machinery like Tarski's theorem?
I do not quite understand decidability/undecidability or Tarski's theorem well. However, my intuition tells me that since the sets in question are compact and the functions in question are continuous, some direct proof should be possible for feasibility questions of this kind. Or is what is happening here much deeper than mere compactness and continuity? (Imprecise statement -- reminds me that when sinusoidal functions are included in a theory, decidability vanishes).
Part of the reason why I ask this question is for understanding. The other is that what happens if exponential function is included in the optimization problem? Decidability of the theory of $(R;+,-, \times, <, =, \exp,0,1)$ requires Schanuel's conjecture; however if we pose an optimization problem with the exponential function on compact sets, can one prove decidability of feasibility directly without Schanuel's conjecture?