Noperthedron

2 The Noperthedron

2.1 Definition of the Noperthedron

We define three points \(C_1,C_2,C_3\in \mathbb {Q}^3\).

\[ C_1:=\frac{1}{259375205} \begin{pmatrix} {152024884} \\ 0 \\ {210152163} \end{pmatrix}, \qquad C_2:=\frac{1}{10^{10}} \begin{pmatrix} 6632738028 \\ 6106948881 \\ 3980949609 \end{pmatrix}, \]
\[ C_3:=\frac{1}{10^{10}} \begin{pmatrix} 8193990033 \\ 5298215096 \\ 1230614493 \end{pmatrix}. \]
Lemma 1
✓
#

Lean declarations

\(\| C_1 \| = 1\), \({98 \over 100} {\lt} \| C_2 \| {\lt} {99 \over 100}\), and \({98 \over 100} {\lt} \| C_3 \| {\lt} {99 \over 100}\).

Proof ▶

Trivial arithmetic.

Lemma 2
✓
#

Lean declarations

The radius of the Noperthedron is one.

Proof ▶

By lemma 1, theorem 24, ??, and lemma 7.

Rotations about the \(x, y, z\) axes \(R_x,R_y,R_z:\) \(\mathbb {R}\to \mathbb {R}^{3\times 3}\) are defined in the usual way:

\[ R_x(\alpha ):=\begin{pmatrix} 1 & 0 & 0 \\ 0 & \cos \alpha & -\sin \alpha \\ 0 & \sin \alpha & \cos \alpha \end{pmatrix}, \hspace{1cm} R_y(\alpha ):=\begin{pmatrix} \cos \alpha & 0 & -\sin \alpha \\ 0 & 1 & 0 \\ \sin \alpha & 0 & \cos \alpha \end{pmatrix}, \]
\[ R_z(\alpha ):=\begin{pmatrix} \cos \alpha & -\sin \alpha & 0 \\ \sin \alpha & \cos \alpha & 0 \\ 0 & 0 & 1 \end{pmatrix}. \]

Where Steininger and Yurkevich define a 30-element set \(C_30\)

\[ \mathcal{C}_{30} :=\left\{ (-1)^\ell R_z\left(\frac{2\pi k}{15}\right) \colon k=0,\dots ,14; \ell =0,1\right\} . \]

of rotations, we instead define

Definition 3
✓
#

Lean declarations

\[ \mathcal{C}_{15} :=\left\{ R_z\left(\frac{2\pi k}{15}\right) \colon k=0,\dots ,14 \right\} . \]

without point-symmetricness ‘baked in’ as it is in \(C_{30}\). It’s more convenient for the formalization to apply \(C_{15}\) to the points \(C_1, C_2, C_3\), and then point-symmetrize that set afterwards.

Definition 4
✓
#

Lean declarations

A set \(S \subseteq \operatorname{\mathbb {R}}^3\) is point-symmetric if \(x \in S\) implies \(-x \in S\).

Definition 5
✓
#

Lean declarations

The pointsymmetrization of a collection of vertices \(v_1, \ldots , v_n \in \operatorname{\mathbb {R}}^3\) is \(v_1, \ldots , v_n, -v_1, \ldots , -v_n\).

We write \(\mathcal{C}_{15} \cdot P = \{ c P \, \text{ for } \, c \in \mathcal{C}_{15}\} \) for the orbit of \(P\) under the action of \(\mathcal{C}_{15}\).

Definition 6
✓
#

Uses

Lean declarations

The Noperthedron is polyhedron given by the vertex set that is the pointsymmetrization of

\[ \mathcal{C}_{15} \cdot C_1 \cup \mathcal{C}_{15} \cdot C_2 \cup \mathcal{C}_{15} \cdot C_3 \]
Lemma 7
✓
#

Lean declarations

The norm of any vertex in the prepointsymmetrized version of the Noperthedron is no more than 1.

Proof ▶

Evident from definitions.

Lemma 8
✓
#

Lean declarations

The pointsymmetrization of any set is point-symmetric.

Proof ▶

Evident from definitions.

Lemma 9
✓
#

Uses

Lean declarations

The noperthedron is point-symmetric.

Proof ▶

Follows from Lemma 8.

2.2 Refined Rupert’s property for the Noperthedron

Lemma 10
#

Lean declarations

Let \(\operatorname{\mathbf{P}}= \operatorname{\mathbf{NOP}}\), then for all \(\theta , \varphi , \alpha \in \operatorname{\mathbb {R}}\), the following three identities hold (as sets):

\begin{align*} M({\theta +2\pi /15,\varphi })\cdot \operatorname{\mathbf{P}}& =M(\theta , \varphi ) \cdot \operatorname{\mathbf{P}},\\ R(\alpha +\pi )M(\theta , \varphi ) \cdot \operatorname{\mathbf{P}}& =R(\alpha )M(\theta , \varphi ) \cdot \operatorname{\mathbf{P}},\\ \begin{pmatrix} 1 & 0 \\ 0 & -1 \end{pmatrix} M(\theta , \varphi ) \cdot \operatorname{\mathbf{P}}& = M({\theta +\pi /15,\pi -\varphi }) \cdot \operatorname{\mathbf{P}}. \end{align*}
Proof ▶

See [ SY25 ] , Lemma 7.

Corollary 11
#

Lean declarations

If the noperthedron is Rupert, then there exists a solution with

\begin{align*} \theta _1,\theta _2& \in [0,2\pi /15] \subset [0,0.42], \\ \varphi _1& \in [0,\pi ] \subset [0,3.15],\\ \varphi _2& \in [0,\pi /2] \subset [0,1.58],\\ \alpha & \in [-\pi /2,\pi /2] \subset [-1.58,1.58]. \end{align*}
Proof ▶

See [ SY25 ] , Lemma 8.