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.
翻译：证明Banach-Tarski Theorem理论的关键步骤之一是引入一个自由轮换组合。 首先,当集的每个元素都以 ACL2 列表的形式表示时,将产生一个自由的减号组合。 然后,我们证明减号组合和3D 轮值组合之间有一对一的关系。 在本文中,我们提出了一个生成这组减号组合的方法,并证明这组组合的属性。 然后,我们展示了一个利用减号组合生成一套3D矩阵的方法。 最后,我们展示了3D轮值的正规化,并证明3D矩阵组合的每一个元素都是轮换的。
相关内容
微信扫码咨询专知VIP会员