Icosahedral Axis Normalizer Decomposition

Abstract

The three finite projective axis classes explicitly biject with the complete 6/10/15 cyclic-axis decomposition and have normalizer orders 10/6/4.

Theorem 1.1 (The finite axis decomposition has the stated normalizers).

$$\begin{array}{r}\mathrm{union}(\mathrm{union}(P_5,P_3),P_2)=\mathrm{univ}\left(FiniteProjectivePlane\right)\wedge \mathrm{Disjoint}\left(P_5,P_3\right)\wedge \mathrm{Disjoint}\left(P_5,P_2\right)\wedge \mathrm{Disjoint}\left(P_3,P_2\right)\wedge \\ \mathrm{Bijective}(fivefoldProjectiveAxisMap:P_5\to A_5)\wedge \mathrm{Bijective}(threefoldProjectiveAxisMap:P_3\to A_3)\wedge \mathrm{Bijective}(twofoldProjectiveAxisMap:P_2\to A_2)\wedge \\ \forall p:P_5,\mathrm{axisFixesProjectivePoint}\left(\mathrm{fivefoldProjectiveAxisMap}\left(p\right),p\right)\wedge \forall p:P_3,\mathrm{axisFixesProjectivePoint}\left(\mathrm{threefoldProjectiveAxisMap}\left(p\right),p\right)\wedge \forall p:P_2,\mathrm{axisFixesProjectivePoint}\left(\mathrm{twofoldProjectiveAxisMap}\left(p\right),p\right)\wedge \\ \mathrm{card}(P_5)=6\wedge \mathrm{card}(P_3)=10\wedge \mathrm{card}(P_2)=15\wedge \\ \mathrm{card}(P_5)=\mathrm{card}(A_5)\wedge \mathrm{card}(P_3)=\mathrm{card}(A_3)\wedge \mathrm{card}(P_2)=\mathrm{card}(A_2)\wedge \\ \mathrm{card}(A_5)=6\wedge \mathrm{card}(A_3)=10\wedge \mathrm{card}(A_2)=15\wedge \\ \forall g,h:A_5,\mathrm{axesAreConjugate}\left(5,g,h\right)\wedge \\ \forall g,h:A_3,\mathrm{axesAreConjugate}\left(3,g,h\right)\wedge \\ \forall g,h:A_2,\mathrm{axesAreConjugate}\left(2,g,h\right)\wedge \\ \forall g:A_5,\mathrm{card}(\mathrm{cyclicAxisNormalizer}\left(5,g\right))=10\wedge \\ \forall g:A_3,\mathrm{card}(\mathrm{cyclicAxisNormalizer}\left(3,g\right))=6\wedge \\ \forall g:A_2,\mathrm{card}(\mathrm{cyclicAxisNormalizer}\left(2,g\right))=4\wedge \\ \forall g:A_2,\mathrm{cyclicAxisNormalizer}\left(2,g\right)=\mathrm{elementCentralizer}\left(g\right).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Arith/IcosahedralAxisNormalizerDecomposition.finite_icosahedral_axis_decomposition_with_normalizers (✓ std3). ∎

Source. Repository-derived.

Commentary.

The projective classes and cyclic-axis families are the canonical objects from the finite axis decomposition. The statement publishes their partition together with three structural maps to the unique cyclic axes that fix the corresponding projective directions. Their bijectivity, cardinalities, normalizer orders, and the twofold normalizer-centralizer identification are published in the same statement.

References

• Truth anchor: D5/S3/Arith/IcosahedralAxisNormalizerDecomposition.finite_icosahedral_axis_decomposition_with_normalizers
• Dependency: D5/S3/Arith/IcosahedralAxisDecomposition