Formalization of Gyrovector Spaces as Models of Hyperbolic Geometry and Special Relativity

In this paper, we present an Isabelle/HOL formalization of noncommutative and nonassociative algebraic structures known as gyrogroups and gyrovector spaces. These concepts were introduced by Abraham A. Ungar and have deep connections to hyperbolic geometry and special relativity. Gyrovector spaces can be used to define models of hyperbolic geometry. Unlike other models, gyrovector spaces offer the advantage that all definitions exhibit remarkable syntactical similarities to standard Euclidean and Cartesian geometry (e.g., points on the line between a and b satisfy the parametric equation \[ a \oplus t \otimes (\ominus a \oplus b), \quad \text{for } t \in \mathbb{R}, \] while the hyperbolic Pythagorean theorem is expressed as \[ a^2 \oplus b^2 = c^2, \] where \( \otimes \), \( \oplus \), and \( \ominus \) represent gyro operations). We begin by formally defining gyrogroups and gyrovector spaces and proving their numerous properties. Next, we formalize Möbius and Einstein models of these abstract structures (formulated in the two-dimensional, complex plane), and then demonstrate that these are equivalent to the Poincaré and Klein-Beltrami models, satisfying Tarski’s geometry axioms for hyperbolic geometry.