Descartes' Rule of Signs

In this work, we formally proved Descartes Rule of Signs, which relates the number of positive real roots of a polynomial with the number of sign changes in its coefficient list. Our proof follows the simple inductive proof given by Arthan [1], which was also used by John Harrison in his HOL Light formalisation. We proved most of the lemmas for arbitrary linearly-ordered integrity domains (e.g. integers, rationals, reals); the main result, however, requires the intermediate value theorem and was therefore only proven for real polynomials. Contents 1 Sign changes and Descartes’ Rule of Signs 1

• Type: Journal
• Year: 2015
• Where: AFP
• Authors: Manuel Eberl
• Keywords: AFP 2015, Formal Methods