Dependencies

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

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

Let \(\alpha ,\theta ,\varphi \in [-4,4]\). Then it holds that

Moreover,

Let \(\theta , \varphi \in \operatorname{\mathbb {Q}}\cap [-4,4]\) and \(M_{\operatorname{\mathbb {Q}}} :=M_{\operatorname{\mathbb {Q}}}(\theta , \varphi )\). Three points \(\widetilde{P}_1, \widetilde{P}_2, \widetilde{P}_3 \in \operatorname{\mathbb {Q}}^3\) with \(\| \widetilde{P}_1\| , \| \widetilde{P}_2\| , \| \widetilde{P}_3\| \leq 1+\kappa \) are called \(\varepsilon \)-\(\kappa \)-spanning for \((\theta , \varphi )\) if it holds that:

Let \(\theta , \varphi \in \mathbb {R}\), \(\varepsilon {\gt} 0\), and set \(M := M(\theta , \varphi )\). Three points \(P_1, P_2, P_3 \in \mathbb {R}^3\) with \(\| P_1\| , \| P_2\| , \| P_3\| \leq 1\) are called \(\varepsilon \)-spanning for \((\theta , \varphi )\) if it holds that:

Let \(\operatorname{\mathcal{P}}\subset \operatorname{\mathbb {R}}^2\) be a convex polygon and \(Q \in \operatorname{\mathcal{P}}\) one of its vertices. Define \(\operatorname{\mathrm{Sect}}_\delta (Q) :=\operatorname{\mathrm{Disc}}_{\delta }(Q) \cap \operatorname{\mathcal{P}}^\circ \) as the intersection between \(\operatorname{\mathrm{Disc}}_{\delta }(Q)\) and the interior of the convex hull of \(\operatorname{\mathcal{P}}\).

Moreover, \(Q \in \operatorname{\mathcal{P}}\) is called \(\delta \)-locally maximally distant (\(\delta \)-LMD) if for all \(A \in \operatorname{\mathrm{Sect}}_\delta (Q)\) it holds that \(\| Q\| {\gt} \| A\| \).

(This simplifies Definition 31 of [ SY25 ] , which centers the disc at an auxiliary point \(\overline{Q}\) with \(\| Q - \overline{Q}\| {\lt} \delta \); the only role of \(\overline{Q}\) is to bound \(\| A - Q\| {\lt} 2\delta \), so we center the disc at \(Q\) itself, with the radius playing the role of the paper’s \(2\delta \).)

The Noperthedron is polyhedron given by the vertex set

We define rational approximations of the 90 noperthedron vertices by \(\lfloor x \cdot 10^{16} \rfloor /10^{16}\).

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

Given \(v_1, \dots , v_n \in \operatorname{\mathbb {R}}^n\) write \(\mathrm{span}^+(v_1,\dots ,v_n)\) for the set (simplicial cone) in \(\operatorname{\mathbb {R}}^n\) defined by

which is the natural restriction of \(\mathrm{span}(v_1,\dots ,v_n)\) to positive weights.

We define the two functions \(\sin _{\mathbb {Q}}, \cos _{\mathbb {Q}}: \operatorname{\mathbb {R}}\to \operatorname{\mathbb {R}}\) by:

Further, by replacing \(\sin ,\cos \) with \(\sin _{\mathbb {Q}},\cos _{\mathbb {Q}}\) we define the functions

For \(1 \leq i \leq n\) let \((A_i,B_i)\) be pairs of real matrices, such that for each \(i\) the dimensions of \(A_i\) and \(B_i\) are equal. Assume moreover that the products \(A_1\cdots A_n\) and \(B_1 \cdots B_n\) are well defined. Finally, assume that \(\| A_i-B_i\| \leq \kappa \) and let \(\delta _i\geq \max (\| A_i\| ,\| B_i\| ,1)\). Then it holds that \(\| A_1\cdots A_n-B_1\cdots B_n\| \leq n\kappa \cdot \delta _1\cdots \delta _n\).

Let \(A = (a_{i,j})_{1 \leq i \leq m,\ 1 \leq j \leq n} \in \operatorname{\mathbb {R}}^{m \times n}\) and \(\delta {\gt}0\). Assume that \(|a_{i,j}| \leq \delta \). Then it holds that \(\| A\| \leq \delta \sqrt{mn}.\)

For \(A,B\in \operatorname{\mathbb {R}}^{m\times n}\) and \(P_1,P_2\in \operatorname{\mathbb {R}}^n\) one has

Let \(\alpha , \theta , \varphi \in [-4,4]\), \(P\in \operatorname{\mathbb {R}}^3\) with \(\| P\| \leq 1\) and let \(\widetilde{P}\) be a \(\kappa \)-rational approximation of \(P\). Set \(M = M(\theta , \varphi )\) and \(M_{\operatorname{\mathbb {Q}}} = M_{\operatorname{\mathbb {Q}}}(\theta , \varphi )\), \(M^\theta = M^\theta (\theta , \varphi )\), \(M^\theta _{\operatorname{\mathbb {Q}}} = M^\theta _{\operatorname{\mathbb {Q}}}(\theta , \varphi )\), \(M^\varphi = M^\varphi (\theta , \varphi )\), \(M^\varphi _{\operatorname{\mathbb {Q}}} = M^\varphi _{\operatorname{\mathbb {Q}}}(\theta , \varphi )\) as well as \(R = R(\alpha )\), \(R_{\operatorname{\mathbb {Q}}} = R_{\operatorname{\mathbb {Q}}}(\alpha )\), \(R' = R'(\alpha )\), \(R'_{\operatorname{\mathbb {Q}}} = R'_{\operatorname{\mathbb {Q}}}(\alpha )\). Finally let \(w \in \operatorname{\mathbb {R}}^2\) with \(\| w\| = 1\). Then:

and the same bounds hold with \(M\) replaced by any of the second-derivative matrices \(M^{\theta \theta }, M^{\theta \varphi }, M^{\varphi \varphi }\) (at \(3\kappa \) without a rotation factor, at \(4\kappa \) with \(R\) in front) and with \(R'\) in place of \(R\) in front of \(M^\theta \) and \(M^\varphi \) (at \(4\kappa \)).

Let \(P,Q \in \operatorname{\mathbb {R}}^3\) with \(\| P\| ,\| Q\| \leq 1\) and \(\widetilde{P},\widetilde{Q}\) some respective \(\kappa \)-rational approximations. Moreover, let \(\alpha , \theta , \varphi \in \operatorname{\mathbb {R}}\in [-4,4]\) and set \(X = X(\theta , \varphi )\), \(X_{\operatorname{\mathbb {Q}}} = X_{\operatorname{\mathbb {Q}}}(\theta , \varphi )\) as well as \(M = M(\theta , \varphi )\), \(M_{\operatorname{\mathbb {Q}}} = M_{\operatorname{\mathbb {Q}}}(\theta , \varphi )\). Then

In the setting of lemma 48, let \(\sqrt[+]{x}\) be an upper square-root function, i.e., \(\sqrt{x} \leq \sqrt[+]{x}\) for all real \(x \geq 0\) with rational output on rational input. Set \(\| x\| _{+} :=\sqrt[+]{\| x\| ^2}\). Set

as well as

Assume that \(A \geq 0\). Then it holds that \(A \geq A_{\operatorname{\mathbb {Q}}}\).

(In the Lean formalization, each applied vector \(M_{\operatorname{\mathbb {Q}}} \widetilde{x}\) appearing in \(A_{\operatorname{\mathbb {Q}}}\) is additionally rounded down componentwise to a multiple of \(10^{-13}\) — Pose.rotM₂Rℚ — so that the checker’s dot products and norms run on small denominators; the resulting perturbation, at most \(2 \cdot 10^{-12}\) in the numerator and \(2 \cdot 10^{-13}\) in each norm, is absorbed into the \(10\kappa \), \(3\kappa \) and \(6\kappa \) terms.)

Let \(P_1,P_2,P_3, Q_1,Q_2,Q_3 \in \operatorname{\mathbb {R}}^3\). Define the \(3 \times 3\) matrices \(P :=(P_1|P_2|P_3)\) and \(Q :=(Q_1|Q_2|Q_3)\) and assume that \(Q\) is invertible. Then \(P_1, P_2, P_3\) and \(Q_1, Q_2, Q_3\) are congruent if and only if \(P^t P = Q^t Q\).

Let \(\varepsilon {\gt}0\) and \(\theta ,\overline{\theta }, \varphi , \overline{\varphi }\in \operatorname{\mathbb {R}}\) with \(|\theta - \overline{\theta }|, |\varphi - \overline{\varphi }| \leq \varepsilon \). Define \(M = M(\theta , \varphi )\) and \(\overline{M} = M(\overline{\theta }, \overline{\varphi })\) and let \(P, Q \in \operatorname{\mathbb {R}}^3\) with \(\| P\| , \| Q\| \leq 1\). Assume that

Then:

Let \(A(x,y)\) be an \(m\times n\) matrix with \(1 \leq m,n\leq 3\) such that every entry is of the form \(a_1(x)\cdot a_2(y)\) where \(a_i(z)\in \{ 0,1,-1,\pm \sin (z),\pm \cos (z)\} .\) Define \(A_{\mathbb {Q}}(x,y)\) by replacing \(\sin \) with \(\sin _{\mathbb {Q}}\) and \(\cos \) with \(\cos _{\mathbb {Q}}\). Then for every \(x,y\in [-4,4]\) it holds that \(\| A(x,y)-A_{\mathbb {Q}}(x,y)\| \leq \kappa \).

Let \(P_1, P_2, P_3 \in \operatorname{\mathbb {R}}^3\) with \(\| P_i\| \leq 1\) and \(\widetilde{P}_1, \widetilde{P}_2, \widetilde{P}_3 \in \operatorname{\mathbb {Q}}^3\) be their \(\kappa \)-rational approximations. Assume that \(\widetilde{P}_1, \widetilde{P}_2, \widetilde{P}_3\) are \(\varepsilon \)-\(\kappa \)-spanning for some \(\theta , \varphi \in \operatorname{\mathbb {Q}}\cap [-4,4]\), then \(P_1, P_2, P_3\) are \(\varepsilon \)-spanning for \(\theta , \varphi \).

Let \(P_1, P_2, P_3 \in \operatorname{\mathbb {R}}^3\) with \(\| P_1\| ,\| P_2\| ,\| P_3\| \leq 1\) be \(\varepsilon \)-spanning for \((\overline{\theta }, \overline{\varphi })\) and let \(\theta , \varphi \in \operatorname{\mathbb {R}}\) such that \(|\theta - \overline{\theta }|, |\varphi - \overline{\varphi }| \leq \varepsilon \). Assume that \(\langle X(\theta , \varphi ), P_i \rangle {\gt} 0\) for \(i=1,2,3\). Then

Suppose \(V = V_1, \ldots , V_m \subseteq \operatorname{\mathbb {R}}^n\) be a finite sequence of points. Suppose \(\mathsf{Co}(V)\) is its convex hull. Let \(S \in \mathsf{Co}(V)\) and \(w \in \operatorname{\mathbb {R}}^n\) be given. then

Let \(P, Q \in \operatorname{\mathbb {R}}^3\) with \(\| P\| , \| Q\| \leq 1\). Let \(\varepsilon {\gt}0\) and \(\overline{\theta }_1,\overline{\varphi }_1,\overline{\theta }_2,\overline{\varphi }_2,\overline{\alpha }\in \operatorname{\mathbb {R}}\) with

Finally, let \(\theta _1, \varphi _1, \theta _2, \varphi _2, \alpha \in \operatorname{\mathbb {R}}\) with \(|\overline{\theta }_1-\theta _1|, |\overline{\varphi }_1 - \varphi _1|, |\overline{\theta }_2-\theta _2|, |\overline{\varphi }_2-\varphi _2|, |\overline{\alpha }- \alpha | \leq \varepsilon \). Then

For every \(x\in [-4,4]\) it holds that

Let \(V_1,V_2,V_3,Y,Z \in \operatorname{\mathbb {R}}^3\) with \(\| Y \| =\| Z \| \) and \(Y,Z \in \mathrm{span}^+(V_1,V_2,V_3)\). Then there exists an \(i\) with

Let \(S \in \operatorname{\mathbb {R}}^3\) and \(w \in \operatorname{\mathbb {R}}^2\) be unit vectors and set \(f(x_1,x_2,x_3) = \langle R(x_3) M(x_1,x_2)S,w \rangle \). Then for all \(x_1,x_2,x_3 \in \operatorname{\mathbb {R}}\) and any \(i,j,k \in \{ 1,2,3\} \) it holds that

Let \(\operatorname{\mathcal{P}}\) be a convex polygon and \(Q \in \operatorname{\mathcal{P}}\) be one of its vertices. Let \(\delta {\gt} 0\). Assume that for some \(r {\gt} 0 \) such that \(\| Q\| {\gt} r\) it holds that

for all other vertices \(P_j \in \operatorname{\mathcal{P}}\setminus Q\). Then \(Q \in \operatorname{\mathcal{P}}\) is \(2\delta \)-locally maximally distant.

Let \(P \in \operatorname{\mathbb {R}}^3\) with \(\| P\| \leq 1\). Further, let \(\varepsilon , r{\gt}0\) and \(\overline{\theta },\overline{\varphi }, \theta , \varphi \in \operatorname{\mathbb {R}}\) such that \(|\overline{\theta }-\theta |, |\overline{\varphi }- \varphi | \leq \varepsilon \). If \( \| M(\overline{\theta },\overline{\varphi }) P \| {\gt} r + \sqrt{2}\varepsilon \) then \( \| M(\theta ,\varphi ) P \| {\gt} r. \)

Let \(f:\operatorname{\mathbb {R}}^n\to \operatorname{\mathbb {R}}\) be a \(C^3\)-function, let \(\varepsilon _1,\dots ,\varepsilon _n \geq 0\), and let \(x_1,\dots ,x_n,y_1,\dots ,y_n \in \operatorname{\mathbb {R}}\) be such that \(|x_i-y_i|\leq \varepsilon _i\) for all \(i\). If \( \left|\partial _{x_i}\partial _{x_j}\partial _{x_k}f(v)\right| \leq 1 \) for all \(i,j,k \in \{ 1,\dots ,n\} \) and all \(v \in \operatorname{\mathbb {R}}^n\), then

(At \(\varepsilon _1 = \dots = \varepsilon _n = \varepsilon \) this recovers the isotropic remainder \(\frac{n^3}{6}\varepsilon ^3\).)

Let \(A,B,C\in \mathbb {R}^2\) be such that \( \langle R({\pi /2}) A,B\rangle , \langle R({\pi /2}) B,C\rangle , \langle R({\pi /2}) C,A\rangle {\gt}0\). Then the origin lies strictly in the triangle \(ABC\).

For any \(P \in \mathbb {R}^3\) one has \(\big\| M(\theta , \varphi ) P\big\| ^2=\| P\| ^2-\langle X({\theta ,\varphi }),P\rangle ^2\).

Let \(\varepsilon {\gt}0\), \(|\alpha -\overline{\alpha }|\leq \varepsilon \) and \(a \in \{ x,y,z\} \) then \(\| R_a(\alpha )-R_a({\overline{\alpha }})\| =\| R(\alpha )-R(\overline{\alpha })\| {\lt} \varepsilon \).

For any \(\alpha , \theta ,\varphi \in \operatorname{\mathbb {R}}\) and \(a \in \{ x,y,z\} \) one has \(\| R(\alpha )\| = \| R_a(\alpha )\| = \| R'(\alpha ) \| =\| M(\theta , \varphi )\| = 1\) and \(\| M^\theta (\theta ,\varphi )\| , \| M^\varphi (\theta ,\varphi )\| \leq 1\).

The partial derivatives of all relevant rotations, projections, and inner products used in the Global Theorem are as expected. Specifically:

• \[ f^\alpha (\theta ,\varphi ,\alpha ) = \langle R'(\alpha ) M(\theta , \varphi ) S, w \rangle \]
• \[ f^\theta (\theta ,\varphi ,\alpha ) = \langle R(\alpha ) M^\theta (\theta , \varphi ) S, w \rangle \]
• \[ f^\varphi (\theta ,\varphi ,\alpha ) = \langle R(\alpha ) M^\varphi (\theta , \varphi ) S, w \rangle \]
• \[ g^\theta (\theta ,\varphi ) = \langle M^\theta (\theta , \varphi ) P, w \rangle \]
• \[ g^\varphi (\theta ,\varphi ) = \langle M^\varphi (\theta , \varphi ) P, w \rangle \]

where \(f(\theta ,\varphi ,\alpha ) = \langle R(\alpha ) M(\theta ,\varphi ) S / \| S\| , w\rangle \) and \(g(\theta ,\varphi ) = \langle M(\theta ,\varphi ) P / \| P\| , w\rangle \).

For any \(\alpha ,\beta \in \mathbb {R}\) one has

with equality only for \(\alpha = \beta = 0\).

For \(A,\overline{A},B,\overline{B}\in \operatorname{\mathbb {R}}^{m\times n}\) and \(P_1,P_2\in \operatorname{\mathbb {R}}^n\) it holds that

Let \(\varepsilon {\gt}0\) and \(|\theta -\overline{\theta }|,|\varphi -\overline{\varphi }| \leq \varepsilon \) then \(\| M(\theta , \varphi )-M(\overline{\theta },\overline{\varphi })\| , \| X({\theta , \varphi })-X(\overline{\theta },\overline{\varphi })\| {\lt} \sqrt{2}\varepsilon .\)

Let \(\varepsilon {\gt}0\) and \(|\theta -\overline{\theta }|,|\varphi -\overline{\varphi }|,|\alpha -\overline{\alpha }|\leq \varepsilon \) then \(\| R(\alpha ) M(\theta , \varphi )-R(\overline{\alpha })M(\overline{\theta },\overline{\varphi })\| {\lt} \sqrt{5} \varepsilon .\)

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

Let \(P \in \operatorname{\mathbb {R}}^3\) with \(\| P\| \leq 1\). Further, let \(\varepsilon {\gt}0\) and \(\overline{\theta },\overline{\varphi }, \theta , \varphi \in \operatorname{\mathbb {R}}\) such that \(|\overline{\theta }-\theta |, |\overline{\varphi }- \varphi | \leq \varepsilon \). If \( \langle X(\overline{\theta },\overline{\varphi }),P \rangle {\gt}\sqrt{2}\varepsilon \) then \( \langle X(\theta , \varphi ),P \rangle {\gt}0. \)

The noperthedron is point-symmetric.

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

There exists a valid solution table whose zeroth row covers

Let \(\operatorname{\mathbf{P}}\) be a pointsymmetric convex polyhedron with radius \(\rho =1\) and let \(S \in \operatorname{\mathbf{P}}\). Further let \(\overline{\theta }_1,\overline{\varphi }_1,\overline{\theta }_2,\overline{\varphi }_2,\overline{\alpha }\in \operatorname{\mathbb {R}}\), let \(\varepsilon _\alpha , \varepsilon _{\theta _1}, \varepsilon _{\varphi _1}, \varepsilon _{\theta _2}, \varepsilon _{\varphi _2} \geq 0\) be per-axis radii, and let \(w\in \operatorname{\mathbb {R}}^2\) be a unit vector. Denote \(\overline{M_1}:=M(\overline{\theta }_1, \overline{\varphi }_1)\), \( \overline{M_2}:=M(\overline{\theta }_2, \overline{\varphi }_2)\) as well as \(\overline{M_1}^{\theta } :=M^\theta (\overline{\theta }_1, \overline{\varphi }_1)\), \(\overline{M_1}^{\varphi } :=M^\varphi (\overline{\theta }_1, \overline{\varphi }_1)\) and analogously for \(\overline{M_2}^{\theta }, \overline{M_2}^{\varphi }\). Finally set

If \(G{\gt}\max _{P\in \operatorname{\mathbf{P}}} H_P\) then there does not exist a solution to Rupert’s condition with

(This is a second-order, anisotropic strengthening of [ SY25 ] , Theorem 17, whose penalty is first-order and isotropic with quadratic remainders \(9\varepsilon ^2/2\) and \(2\varepsilon ^2\): here the exact second partials at the center pose are charged with per-axis weights — with multiplicities from the symmetric Hessian table — and only the cubic Lagrange remainders \((\varepsilon _\alpha +\varepsilon _{\theta _1}+\varepsilon _{\varphi _1})^3/6\) and \((\varepsilon _{\theta _2}+\varepsilon _{\varphi _2})^3/6\) are bounded via Lemma 19. On the diagonal \(\varepsilon _\alpha = \varepsilon _{\theta _1} = \dots = \varepsilon \), these are \(\frac{3^3}{6}\varepsilon ^3 = \frac{9\varepsilon ^3}{2}\) and \(\frac{2^3}{6}\varepsilon ^3 = \frac{4\varepsilon ^3}{3}\).)

Let \(\operatorname{\mathbf{P}}\) be a pointsymmetric convex polyhedron with radius \(\rho =1\) and \(\widetilde{\operatorname{\mathbf{P}}}\) a \(\kappa \)-rational approximation. Let \(\widetilde{S} \in \widetilde{\operatorname{\mathbf{P}}}\). Further let \(\varepsilon _\alpha , \varepsilon _{\theta _1}, \varepsilon _{\varphi _1}, \varepsilon _{\theta _2}, \varepsilon _{\varphi _2} \in \operatorname{\mathbb {Q}}_{\geq 0}\) be per-axis radii and \(\overline{\theta }_1,\overline{\varphi }_1,\overline{\theta }_2,\overline{\varphi }_2,\overline{\alpha }\in \operatorname{\mathbb {Q}}\cap [-4,4]\). Let \(w\in \operatorname{\mathbb {Q}}^2\) be a unit vector. Denote \(\overline{M_1}:=M_{\operatorname{\mathbb {Q}}}(\overline{\theta }_1, \overline{\varphi }_1)\), \( \overline{M_2}:=M_{\operatorname{\mathbb {Q}}}(\overline{\theta }_2, \overline{\varphi }_2)\) as well as \(\overline{M_1}^{\theta } :=M_{\operatorname{\mathbb {Q}}}^\theta (\overline{\theta }_1, \overline{\varphi }_1)\), \(\overline{M_1}^{\varphi } :=M_{\operatorname{\mathbb {Q}}}^\varphi (\overline{\theta }_1, \overline{\varphi }_1)\) and analogously for \(\overline{M_2}^{\theta }, \overline{M_2}^{\varphi }\). Write \(E_1 :=\varepsilon _\alpha + \varepsilon _{\theta _1} + \varepsilon _{\varphi _1}\) and \(E_2 :=\varepsilon _{\theta _2} + \varepsilon _{\varphi _2}\), and set

If \(G^{\operatorname{\mathbb {Q}}}{\gt}\max _{P\in \widetilde{\operatorname{\mathbf{P}}}} H^{\operatorname{\mathbb {Q}}}_P\) then there does not exist a solution to Rupert’s condition to \(\operatorname{\mathbf{P}}\) with

(On the diagonal \(\varepsilon _\alpha = \dots = \varepsilon \) the slack terms are \(4\kappa (1+3\varepsilon +\tfrac 92\varepsilon ^2)\) and \(3\kappa (1+2\varepsilon +2\varepsilon ^2)\).)

Let \(\operatorname{\mathbf{P}}\) be a polyhedron with radius \(\rho =1\) and \(P_1, P_2, P_3, Q_1, Q_2, Q_3 \in \operatorname{\mathbf{P}}\) be not necessarily distinct. Assume that \(P_1, P_2, P_3\) and \(Q_1, Q_2, Q_3\) are congruent.

Let \(\varepsilon {\gt}0\) and \(\overline{\theta }_1,\overline{\varphi }_1,\overline{\theta }_2,\overline{\varphi }_2,\overline{\alpha }\in \operatorname{\mathbb {R}}\), then set \(\overline{X_1}:=X(\overline{\theta }_1,\overline{\varphi }_1), \overline{X_2}:=X(\overline{\theta }_2,\overline{\varphi }_2)\) as well as \(\overline{M_1}:=M(\overline{\theta }_1,\overline{\varphi }_1), \overline{M_2}:=M(\overline{\theta }_2,\overline{\varphi }_2)\). Assume that there exist \(\sigma _P, \sigma _Q \in \{ 0,1\} \) such that

for all \(i=1,2,3\). Moreover, assume that \(P_1,P_2,P_3\) are \(\varepsilon \)-spanning for \((\overline{\theta }_1,\overline{\varphi }_1)\) and that \(Q_1,Q_2,Q_3\) are \(\varepsilon \)-spanning for \((\overline{\theta }_2,\overline{\varphi }_2)\). Finally, assume that for all \(i = 1,2,3\) and any \(Q_j \in \operatorname{\mathbf{P}}\setminus Q_i\) it holds that

for some \(r {\gt}0\) such that \(\min _{i=1,2,3}\| \overline{M_2}Q_i \| {\gt} r + \sqrt{2} \varepsilon \) and for some \(\delta \in \operatorname{\mathbb {R}}\) with

Then there exists no solution to Rupert’s problem \(R(\alpha ) M(\theta _1,\varphi _1)\operatorname{\mathbf{P}}\subset M(\theta _2,\varphi _2)\operatorname{\mathbf{P}}^\circ \) with

Let \(\operatorname{\mathbf{P}}\) be a polyhedron with radius \(\rho =1\) and \(\widetilde{P}_i\) be a \(\kappa \)-rational approximation of \(P_i \in \operatorname{\mathbf{P}}\). Set \(\widetilde{\operatorname{\mathbf{P}}} = \{ \widetilde{P}_i \text{ for } P_i \in \operatorname{\mathbf{P}}\} \). Let \(P_1, P_2, P_3, Q_1, Q_2, Q_3 \in \operatorname{\mathbf{P}}\) be not necessarily distinct and assume that \(P_1, P_2, P_3\) and \(Q_1, Q_2, Q_3\) are congruent. Let \(\varepsilon {\gt}0\) and \(\overline{\theta }_1,\overline{\varphi }_1,\overline{\theta }_2,\overline{\varphi }_2,\overline{\alpha }\in \operatorname{\mathbb {Q}}\cap [-4,4]\). Set \(\overline{X_1}:=X_{\operatorname{\mathbb {Q}}}(\overline{\theta }_1,\overline{\varphi }_1), \overline{X_2}:=X_{\operatorname{\mathbb {Q}}}(\overline{\theta }_2,\overline{\varphi }_2)\) as well as \(\overline{M_1}:=M_{\operatorname{\mathbb {Q}}}(\overline{\theta }_1,\overline{\varphi }_1), \overline{M_2}:=M_{\operatorname{\mathbb {Q}}}(\overline{\theta }_2,\overline{\varphi }_2)\). Assume that there exist \(\sigma _P, \sigma _Q \in \{ 0,1\} \) such that

for all \(i=1,2,3\). Moreover, assume that \(\widetilde{P}_1,\widetilde{P}_2,\widetilde{P}_3\) are \(\varepsilon \)-\(\kappa \)-spanning for \((\overline{\theta }_1,\overline{\varphi }_1)\) and that \(\widetilde{Q}_1,\widetilde{Q}_2,\widetilde{Q}_3\) are \(\varepsilon \)-\(\kappa \)-spanning for \((\overline{\theta }_2,\overline{\varphi }_2)\). Let \(\sqrt[+]{x}\) and \(\sqrt[-]{x}\) be upper- and lower-square-root functions (bounding \(\sqrt{x}\) from above/below for all real \(x \geq 0\), with rational output on rational input), then set \(\| Z\| _{+} :=\sqrt[+]{\| Z\| ^2}\) and \(\| Z\| _{-} :=\sqrt[-]{\| Z\| ^2}\) for \(Z \in \operatorname{\mathbb {R}}^n\). Finally, assume that for all \(i = 1,2,3\) and any \(\widetilde{Q}_j \in \widetilde{\operatorname{\mathbf{P}}} \setminus \widetilde{Q}_i\) it holds that

for some \(r {\gt}0\) such that \(\min _{i=1,2,3}\| \overline{M_2}\widetilde{Q}_i \| _{-} {\gt} r + \sqrt{2} \varepsilon + 3\kappa \) and for some \(\delta \in \operatorname{\mathbb {R}}\) with

Then there exists no solution to Rupert’s problem \(R(\alpha ) M(\theta _1,\varphi _1)\operatorname{\mathbf{P}}\subset M(\theta _2,\varphi _2)\operatorname{\mathbf{P}}^\circ \) with

(In the Lean formalization, the applied vector \(\overline{M_2}\widetilde{Q}_i\) in the \(r\)-condition \(\| \overline{M_2}\widetilde{Q}_i \| _{-} {\gt} r + \sqrt{2} \varepsilon + 3\kappa \) is additionally rounded down componentwise to a multiple of \(10^{-13}\) — Pose.rotM₂Rℚ, as in condition B\(^{\operatorname{\mathbb {Q}}}_\varepsilon \) — so that the checker’s lower norm runs on small denominators; the resulting perturbation of at most \(2 \cdot 10^{-13}\) is absorbed into the \(3\kappa \) term.)

There is no pose that makes the noperthedron have the Rupert property.

There is no 5-parameter pose that makes the noperthedron have the Rupert property.

There is no purely rotational pose that makes the noperthedron have the Rupert property.

There does not in fact exist a noperthedron Rupert solution with

The noperthedron is not a Rupert polyhedron.

The noperthedron is not a Rupert set.

nopertQ is a \(\kappa \)-rational approximation of the Noperthedron.

Given a pose with zero offset, there exists a 5-parameter pose that is equivalent to it.

If we have a valid solution table, then there is no Rupert solution of the interval of its zeroth row.

If we have a valid solution table, and in particular its \(i\)th row is valid, then there is no Rupert solution of the interval of its \(i\)th row.

The following are equivalent:

• The convex polyhedron with vertex set \(v\) is Rupert.

• The convex closure of \(v\) is a Rupert set.

If a set is point symmetric and convex, then it being Rupert implies it being purely rotationally Rupert.

If a global node in the solution tree is valid, then there is no Rupert solution for its interval.

If a local node in the solution tree is valid, then there is no Rupert solution for its interval.