← All papers
Formalizing Rotation Number and Its Properties in Lean
cs.LO
Jul 27, 2021 · v1
TL;DR
Formalizes rotation number for circle homeomorphisms and Ghys's semiconjugacy theorem in Lean.
Abstract
Rotation number is the key numerical invariant of an orientation-preserving circle homeomorphism. This paper describes a formalization in Lean of the definition and basic properties of the translation number of a lift of a circle homeomorphism to the real line, as well as a theorem by E. Ghys providing a necessary and sufficient condition for two actions of a group on the circle by homeomorphisms to be semiconjugate to each other.
Problem
The rotation number is the key numerical invariant of an orientation-preserving circle homeomorphism, but its definition and basic properties had not been formalized in a proof assistant.
Approach
The authors formalize in Lean the definition and basic properties of the translation number of a lift of a circle homeomorphism to the real line. They also formalize a theorem by E. Ghys providing a necessary and sufficient condition for two group actions on the circle by homeomorphisms to be semiconjugate to each other.
Results
The formalization covers the translation number definition, its basic properties, and the Ghys semiconjugacy theorem for circle homeomorphism group actions.