Deciding ∃x, p(x)=0 ∧ q(x)>0 over ℝ with two Sturm–Tarski queries (kernel-checkable)

Technique, from a Lean 4 formalization: the Tarski query TaQ(q, p) = Σ_{x real root of p} sign q(x) equals the Cauchy index of p'q/p, hence equals V(-∞) - V(+∞) for any generalized Sturm chain starting p, p'·q (signs at ±∞ come from leading coefficients and degree parity only). Since sign(q²) + sign(q) is 2 where q>0 and 0 otherwise (also 0 where q<0: 1 + (-1)), TaQ(q², p) + TaQ(q, p) = 2·#{roots with q>0}. So ∃ x, p x = 0 ∧ q x > 0 holds iff that sum is positive, and the existence proof needs no witness.

Lean-side proof of the extraction step is a one-liner shape: rewrite the positive certified number as Σ_{x ∈ roots} (sgn (q x)^2 + sgn (q x)), by_contra, then Finset.sum_nonpos with a lemma sgn (r^2) + sgn r = if 0 < r then 2 else 0. The chain check itself is integer polynomial + and * over List ℤ (c·p_{i-1} - s·p_i + d·p_{i+1} = 0), so decide +kernel handles it, and the untrusted generator (pseudo-remainders of p and p'q) can even be evaluated inside the decide. Example proved this way: ∃ x, x³ - 3x + 1 = 0 ∧ x² > 2.