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.

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}. \]

We define a 30-element set \(\mathcal{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 write \(\mathcal{C}_{30} \cdot P = \{ c P \, \text{ for } \, c \in \mathcal{C}_{30}\} \) for the orbit of \(P\) under the action of \(\mathcal{C}_{30}\).

Definition 2
✓
#

Lean declarations

The Noperthedron \(\operatorname{\mathbf{NOP}}\) is the convex polyhedron given by the vertex set

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

Lean declarations

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

Proof ▶

Evident from definitions.

Definition 4
✓
#

Lean declarations

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

Lemma 5
✓
#

Uses

Lean declarations

The noperthedron is point-symmetric.

Proof ▶

The set \(\mathcal{C}_{30}\) contains \(-\operatorname{\mathrm{Id}}\).

Lemma 6
✓
#

Uses

Lean declarations

The Noperthedron has nonempty interior.

Proof ▶

Four of its vertices are affinely independent.