An algebraic certificate for Budan's theorem (Q531342)

Budan's Theorem states that if \(a,b\) are two elements of an ordered field \(K\) with \(a<b\), then the number of sign changes in the sequence \(\left( f(a),f'(a),f''(a),\dots\right)\) is not less than the number of sign changes in \(\left(f(b),f'(b),f''(b),\dots\right)\). In this short paper, the author presents an algebraic certificate for Budan's Theorem. An algebraic certificate is a certain kind of proof of a statement. In particular, it is an algorithm which produces, from an arbitrary data in the premise of the statement, explicit (in)equalities which express the conclusion. The author presents two different algorithms producing an algebraic certificate for Budan's Theorem. The author claims that this is a first step towards reducing the complexity of constructing the real closure of an ordered field.