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 <InlineEquation ID="IEq1"> <EquationSource Format="TEX">$ a \oplus t\otimes (\ominus a \oplus b)$</EquationSource> <EquationSource Format="MATHML"><math> <mrow> <mi>a</mi> <mo>⊕</mo> <mi>t</mi> <mo>⊗</mo> <mo stretchy="false">(</mo> <mo>⊖</mo> <mi>a</mi> <mo>⊕</mo> <mi>b</mi> <mo stretchy="false">)</mo> </mrow> </math></EquationSource> </InlineEquation>, for <InlineEquation ID="IEq2"> <EquationSource Format="TEX">$t \in \mathbb {R}$</EquationSource> <EquationSource Format="MATHML"><math> <mrow> <mi>t</mi> <mo>∈</mo> <mi mathvariant="double-struck">R</mi> </mrow> </math></EquationSource> </InlineEquation>, while the hyperbolic Pythagorean theorem is expressed as <InlineEquation ID="IEq3"> <EquationSource Format="TEX">$a^2\oplus b^2 = c^2$</EquationSource> <EquationSource Format="MATHML"><math> <mrow> <msup> <mi>a</mi> <mn>2</mn> </msup> <mo>⊕</mo> <msup> <mi>b</mi> <mn>2</mn> </msup> <mo>=</mo> <msup> <mi>c</mi> <mn>2</mn> </msup> </mrow> </math></EquationSource> </InlineEquation>, where <InlineEquation ID="IEq4"> <EquationSource Format="TEX">$\otimes $</EquationSource> <EquationSource Format="MATHML"><math> <mo>⊗</mo> </math></EquationSource> </InlineEquation>, <InlineEquation ID="IEq5"> <EquationSource Format="TEX">$\oplus $</EquationSource> <EquationSource Format="MATHML"><math> <mo>⊕</mo> </math></EquationSource> </InlineEquation>, and <InlineEquation ID="IEq6"> <EquationSource Format="TEX">$\ominus $</EquationSource> <EquationSource Format="MATHML"><math> <mo>⊖</mo> </math></EquationSource> </InlineEquation> 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.

Formalization of gyrovector spaces as models of hyperbolic geometry and special relativity

期刊论文
发表日期：

2025年4月26日

查看全文

Jelena Marković,
Filip Marić

摘要

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)$ $a \oplus t \otimes (⊖ a \oplus b)$ , for $t \in \mathbb {R}$ $t \in R$ , while the hyperbolic Pythagorean theorem is expressed as $a^2\oplus b^2 = c^2$ $a^{2} \oplus b^{2} = c^{2}$ , where $\otimes $ $\otimes$ , $\oplus $ $\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.