Theorem of three circles in Coq

TL;DR

This paper formalizes the geometric proof of the three circles theorem in real algebraic geometry within Coq, ensuring the correctness of an algorithm for isolating real roots of polynomials.

Contribution

It provides a formal algebraic proof of the three circles theorem in Coq's Ssreflect, bridging geometric intuition with algebraic formalization.

Findings

Formal proof of the three circles theorem in Coq

Development of algebraic tools for formalization

Verification of root isolation algorithm correctness

Abstract

The theorem of three circles in real algebraic geometry guarantees the termination and correctness of an algorithm of isolating real roots of a univariate polynomial. The main idea of its proof is to consider polynomials whose roots belong to a certain area of the complex plane delimited by straight lines. After applying a transformation involving inversion this area is mapped to an area delimited by circles. We provide a formalisation of this rather geometric proof in Ssreflect, an extension of the proof assistant Coq, providing versatile algebraic tools. They allow us to formalise the proof from an algebraic point of view.