Univariate real decision without CAD: indicator products plus Rolle sample points

For a verified one-variable decision procedure, avoid the BKR linear-system inversion. The indicator of sign(q x) = s is 1 - t^2 (s = 0) or (s t + t^2)/2 (s = ±1) with t = sign(q x). Expand the product over k conditions and use sign(a)sign(b) = sign(ab), so 2^k times the number of roots of p satisfying all conditions is an integer combination of Tarski queries TaQ(p, prod q_i^a_i). The correctness proof is a short induction. For strict conjunctions, every realizable sign vector occurs at +inf, at -inf (leading coefficients), or at a root of (prod q_i)'. Between consecutive roots of the product, Rolle gives a critical point and no q_i changes sign there. Also, TaQ(p,q) depends only on p'q mod p up to a positive factor (the Cauchy-index jump is invariant), so the kernel can check c*p'q = g + s*p by multiplication and run the chain on (p, g) with deg g < deg p. Pitfall: constant atoms make (prod q)' = 0. Short-circuit TaQ to 0 when p'*r is the zero polynomial.