Email Gateway (Apr 09 2025 at 15:22): Email Gateway (Apr 09 2025 at 15:22):From: Lawrence Paulson <lp15@cam.ac.uk>
I'm happy to announce a substantial new contribution:
Formalization of Gyrovector Spaces as Models of Hyperbolic Geometry and Special Relativity,
by Filip Marić and Jelena Markovic
From the abstract:
“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 .... 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."
https://www.isa-afp.org/entries/GyrovectorSpaces.html
Larry
Last updated: Apr 17 2025 at 20:22 UTC