A Free Group of Rotations of Rank 2

TL;DR

This paper formalizes a free group of rank 2 generated by 3D rotations, providing a method to generate and verify these rotations as part of the proof of the Banach-Tarski Theorem.

Contribution

It introduces a novel formalization linking reduced words to 3D rotations and demonstrates how to generate and verify these rotations within a rigorous framework.

Findings

Established a one-to-one correspondence between reduced words and 3D rotations

Developed a method to generate 3D rotation matrices from reduced words

Proved that all generated matrices are valid rotations

Abstract

One of the key steps in the proof of the Banach-Tarski Theorem is the introduction of a free group of rotations. First, a free group of reduced words is generated where each element of the set is represented as an ACL2 list. Then we demonstrate that there is a one-to-one relation between the set of reduced words and a set of 3D rotations. In this paper we present a way to generate this set of reduced words and we prove group properties for this set. Then, we show a way to generate a set of 3D matrices using the set of reduced words. Finally we show a formalization of 3D rotations and prove that every element of the 3D matrices set is a rotation.