论文标题
一组自由旋转等级2
A Free Group of Rotations of Rank 2
论文作者
论文摘要
Banach-Tarski定理证明的关键步骤之一是引入自由旋转。首先，在集合的每个元素表示为ACL2列表的情况下，生成了一组简化的单词。然后，我们证明了一组简化的单词与一组3D旋转之间存在一对一的关系。在本文中，我们提出了一种生成这组简化单词的方法，并证明了该集合的组属性。然后，我们展示了使用一组简化单词来生成一组3D矩阵的方法。最后，我们显示了3D旋转的形式化，并证明3D矩阵集的每个元素都是旋转。
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.
