Formalization of a sign determination algorithm in real algebraic geometry

Overview & Synopsis

One of the problems in real algebraic geometry is root counting. Given a polynomial, we want to count the number of roots that satisfies constraints expressed as polynomial inequalities, this is done through a process called "sign determination". A naive way is to compute an exponential number of time consuming quantities, called Tarski Queries. In this paper, we formalize the construction of the adapted matrix part of the "better sign determination" algorithm from "Algorithms in Real Algebraic Geometry" (Basu, Pollack, Roy). We prove in Coq that the matrix has the properties expected from the book: small size but still invertible.