7 Rational Versions

Definition 37

✓

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

\begin{align*} \sin _{\mathbb {Q}}(x) & :=x-\frac{x^3}{3}+\frac{x^5}{5!}\mp \dots +\frac{x^{25}}{25!},\\ \cos _{\mathbb {Q}}(x) & :=1-\frac{x^2}{2}+\frac{x^4}{4!}\mp \dots +\frac{x^{24}}{24!}. \end{align*}

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

\[ R_{\operatorname{\mathbb {Q}}}(\alpha ), R'_{\operatorname{\mathbb {Q}}}(\alpha ), X_{\operatorname{\mathbb {Q}}}(\theta , \varphi ), M_{\operatorname{\mathbb {Q}}}(\theta , \varphi ), M_{\operatorname{\mathbb {Q}}}^{\theta }(\theta ,\varphi ),M_{\operatorname{\mathbb {Q}}}^{\varphi }(\theta ,\varphi ). \]

Lemma 38

✓

\[ |\sin _{\mathbb {Q}}(x)-\sin (x)|\leq \frac{|x|^{27}}{27!} \quad \text{and} \quad |\cos _{\mathbb {Q}}(x)-\cos (x)|\leq \frac{|x|^{26}}{26!}. \]

Proof ▶

Appeal to Taylor series bounds, using the fact that all absolute values of higher derivatives of sine and cosine never exceed 1.

Lemma 39

✓

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

\[ |\sin _{\mathbb {Q}}(x)-\sin (x)| \leq \frac{\kappa }{7} \quad \text{and} \quad |\cos _{\mathbb {Q}}(x)-\cos (x)|\leq \frac{\kappa }{7}. \]

Proof ▶

Straightforward numerical calculation from Lemma 38.

Lemma 40

✓

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}.$

Proof ▶

For any $v\in \operatorname{\mathbb {R}}^n$ we have

\begin{align*} \| Av\| ^2 & =\sum _{i=1}^m \left(\sum _{j=1}^na_{i,j}v_j\right)^2 \leq \sum _{i=1}^m\left(\sum _{j=1}^n \delta |v_j|\right)^2 = \delta ^2 m\left(\sum _{j=1}^n |v_j|\right)^2 \leq \delta ^2 m n \| v\| ^2 \end{align*}

using the Cauchy-Schwarz inequality. Dividing by $\| v\| $ and taking the square root proves the claim.

Lemma 41

✓

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 $.

Proof ▶

We’ve replaced the assumption $a_i(z)\in \{ 0,1,-1,\pm \sin (z),\pm \cos (z)\} $ in [ SY25 ] ’s Lemma 40 with $a_i(z)\in [-1,1]$.

By assumption, for fixed $x,y$ every entry of $A(x,y)-A_{\mathbb {Q}}(x,y)$ is of the form $a b - \widetilde{a}\widetilde{b}$ for some $a,b\in [-1,1]$ and $|a-\widetilde{a}|,|b-\widetilde{b}|\leq \kappa /7$ by lemma 39. This implies that

\begin{align*} |ab-\widetilde{a}\widetilde{b}|& \leq |a b-a\widetilde{b}|+|a \widetilde{b}-\widetilde{a}\widetilde{b}| =|a|\cdot |b-\widetilde{b}|+|\widetilde{b}|\cdot |a-\widetilde{a}| \leq 1\cdot \kappa /7+(1+\kappa /7) \cdot \kappa /7 {\lt}\kappa /3. \end{align*}

So we can apply lemma 40 and obtain that $\| A(x,y)-A_{\operatorname{\mathbb {Q}}}(x,y)\| {\lt}\kappa /3\cdot \sqrt{3\cdot 3}=\kappa $.

Corollary 42

✓

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

\begin{align*} \| R(\alpha )-R_{\operatorname{\mathbb {Q}}}(\alpha )\| , \| R’(\alpha )-R_{\operatorname{\mathbb {Q}}}’(\alpha )\| ,\| X(\theta ,\varphi )-X_{\operatorname{\mathbb {Q}}}(\theta , \varphi )\| , \| M(\theta , \varphi )-M_{\operatorname{\mathbb {Q}}}(\theta , \varphi )\| , \\ \| M^\theta (\theta ,\varphi )-M_{\operatorname{\mathbb {Q}}}^\theta (\theta ,\varphi )\| , \| M^\varphi (\theta ,\varphi ) - M_{\operatorname{\mathbb {Q}}}^\varphi (\theta ,\varphi )\| , \| M^{\theta \theta }(\theta ,\varphi )-M_{\operatorname{\mathbb {Q}}}^{\theta \theta }(\theta ,\varphi )\| , \| M^{\theta \varphi }(\theta ,\varphi )-M_{\operatorname{\mathbb {Q}}}^{\theta \varphi }(\theta ,\varphi )\| , \| M^{\varphi \varphi }(\theta ,\varphi )-M_{\operatorname{\mathbb {Q}}}^{\varphi \varphi }(\theta ,\varphi )\| \leq \kappa . \end{align*}

Moreover,

\[ \| R_{\operatorname{\mathbb {Q}}}(\alpha )\| , \| R'_{\operatorname{\mathbb {Q}}}(\alpha )\| , \| M_{\operatorname{\mathbb {Q}}}(\theta , \varphi )\| , \| M_{\operatorname{\mathbb {Q}}}^{\theta }(\theta ,\varphi )\| , \| M_{\operatorname{\mathbb {Q}}}^{\varphi }(\theta ,\varphi )\| , \| M_{\operatorname{\mathbb {Q}}}^{\theta \theta }(\theta ,\varphi )\| , \| M_{\operatorname{\mathbb {Q}}}^{\theta \varphi }(\theta ,\varphi )\| , \| M_{\operatorname{\mathbb {Q}}}^{\varphi \varphi }(\theta ,\varphi )\| \leq 1+\kappa \]

Proof ▶

The first statement is a direct application of lemma 41 and the second statement follows immediately after using lemma 8 and the triangle inequality. The derivative norm bounds follow similarly, using that the operator norms of $R'$, $M^\theta $, and $M^\varphi $ are at most $1$.

Lemma 43

✓

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$.

Proof ▶

See [ SY25 ] , Lemma 42.

Lemma 44

✓

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:

\begin{align} | \langle M P, w\rangle - \langle M_{\operatorname{\mathbb {Q}}} \widetilde{P}, w\rangle | & \leq 3\kappa , \label{eq:boundskappa1} \\ | \langle M^\theta P, w\rangle - \langle M^\theta _{\operatorname{\mathbb {Q}}} \widetilde{P}, w\rangle | & \leq 3\kappa ,\\ | \langle M^\varphi P, w\rangle - \langle M^\varphi _{\operatorname{\mathbb {Q}}} \widetilde{P}, w\rangle | & \leq 3\kappa ,\\ | \langle R M P, w\rangle - \langle R_{\operatorname{\mathbb {Q}}} M_{\operatorname{\mathbb {Q}}} \widetilde{P}, w\rangle | & \leq 4\kappa ,\label{eq:boundskappa4} \\ | \langle R’ M P, w\rangle - \langle R’_{\operatorname{\mathbb {Q}}} M_{\operatorname{\mathbb {Q}}} \widetilde{P}, w\rangle | & \leq 4\kappa ,\\ | \langle R M^\theta P, w\rangle - \langle R_{\operatorname{\mathbb {Q}}} M^\theta _{\operatorname{\mathbb {Q}}} \widetilde{P}, w\rangle | & \leq 4\kappa ,\\ | \langle R M^\varphi P, w\rangle - \langle R_{\operatorname{\mathbb {Q}}} M^\varphi _{\operatorname{\mathbb {Q}}} \widetilde{P}, w\rangle | & \leq 4\kappa , \end{align}

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 $).

Proof ▶

See [ SY25 ] , Lemma 44.

Theorem 45 Rational Global Theorem

✓

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

\begin{align*} G^{\operatorname{\mathbb {Q}}} :={}& \langle R_{\operatorname{\mathbb {Q}}}(\overline{\alpha }) \overline{M_1}\widetilde{S},w \rangle - \varepsilon _\alpha |\langle R_{\operatorname{\mathbb {Q}}}’(\overline{\alpha }) \overline{M_1}\widetilde{S},w \rangle | - \varepsilon _{\theta _1}|\langle R_{\operatorname{\mathbb {Q}}}(\overline{\alpha }) \overline{M_1}^\theta \widetilde{S},w \rangle | - \varepsilon _{\varphi _1}|\langle R_{\operatorname{\mathbb {Q}}}(\overline{\alpha }) \overline{M_1}^\varphi \widetilde{S},w \rangle | \\ & - \frac{1}{2}\big(\varepsilon _\alpha ^2|\langle R_{\operatorname{\mathbb {Q}}}(\overline{\alpha }) \overline{M_1}\widetilde{S},w \rangle | + 2\varepsilon _\alpha \varepsilon _{\theta _1}|\langle R_{\operatorname{\mathbb {Q}}}’(\overline{\alpha }) \overline{M_1}^\theta \widetilde{S},w \rangle | + 2\varepsilon _\alpha \varepsilon _{\varphi _1}|\langle R_{\operatorname{\mathbb {Q}}}’(\overline{\alpha }) \overline{M_1}^\varphi \widetilde{S},w \rangle |\\ & \qquad \quad + \varepsilon _{\theta _1}^2|\langle R_{\operatorname{\mathbb {Q}}}(\overline{\alpha }) \overline{M_1}^{\theta \theta } \widetilde{S},w \rangle | + 2\varepsilon _{\theta _1}\varepsilon _{\varphi _1}|\langle R_{\operatorname{\mathbb {Q}}}(\overline{\alpha }) \overline{M_1}^{\theta \varphi } \widetilde{S},w \rangle | + \varepsilon _{\varphi _1}^2|\langle R_{\operatorname{\mathbb {Q}}}(\overline{\alpha }) \overline{M_1}^{\varphi \varphi } \widetilde{S},w \rangle |\big)\\ & \hspace{9cm}- \frac{E_1^3}{6} - 4\kappa \big( 1 + E_1 + \tfrac 12 E_1^2\big),\\ H^{\operatorname{\mathbb {Q}}}_P :={}& \langle \overline{M_2}P,w \rangle + \varepsilon _{\theta _2}|\langle \overline{M_2}^\theta P,w \rangle |+\varepsilon _{\varphi _2}|\langle \overline{M_2}^\varphi P,w \rangle |\\ & + \frac{1}{2}\big(\varepsilon _{\theta _2}^2|\langle \overline{M_2}^{\theta \theta } P,w \rangle | + 2\varepsilon _{\theta _2}\varepsilon _{\varphi _2}|\langle \overline{M_2}^{\theta \varphi } P,w \rangle | + \varepsilon _{\varphi _2}^2|\langle \overline{M_2}^{\varphi \varphi } P,w \rangle |\big) + \frac{E_2^3}{6} + 3\kappa \big( 1+E_2+\tfrac 12 E_2^2\big). \end{align*}

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

\[ (\theta _1,\varphi _1,\theta _2,\varphi _2,\alpha ) \in [\overline{\theta }_1\pm \varepsilon _{\theta _1}]\times [\overline{\varphi }_1\pm \varepsilon _{\varphi _1}]\times [\overline{\theta }_2\pm \varepsilon _{\theta _2}]\times [\overline{\varphi }_2\pm \varepsilon _{\varphi _2}]\times [\overline{\alpha }\pm \varepsilon _\alpha ]. \]

(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)$.)

Proof ▶

Definition 46

✓

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:

\begin{align*} \langle R(\pi /2) M_{\operatorname{\mathbb {Q}}} \widetilde{P}_1,M_{\operatorname{\mathbb {Q}}} \widetilde{P}_{2}\rangle {\gt} 2 \varepsilon (\sqrt{2} + \varepsilon ) + 6\kappa ,\\ \langle R(\pi /2) M_{\operatorname{\mathbb {Q}}} \widetilde{P}_2,M_{\operatorname{\mathbb {Q}}} \widetilde{P}_{3}\rangle {\gt} 2 \varepsilon (\sqrt{2} + \varepsilon ) + 6\kappa ,\\ \langle R(\pi /2) M_{\operatorname{\mathbb {Q}}} \widetilde{P}_3,M_{\operatorname{\mathbb {Q}}} \widetilde{P}_{1}\rangle {\gt} 2 \varepsilon (\sqrt{2} + \varepsilon ) + 6\kappa . \end{align*}

Lemma 47

✓

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 $.

Proof ▶

See [ SY25 ] , Lemma 46.

Lemma 48

✓

Let $P \in \operatorname{\mathbb {R}}^3$ with $\| P\| \leq 1$ and $\widetilde{P}$ a $\kappa $-rational approximation of $P$. Moreover, let $\theta , \varphi \in [-4,4]$ and set $X = X(\theta , \varphi )$, $X_{\operatorname{\mathbb {Q}}} = X_{\operatorname{\mathbb {Q}}}(\theta , \varphi )$. Then

\begin{align} |\langle X, P \rangle - \langle X_{\operatorname{\mathbb {Q}}}, \widetilde{P} \rangle | & \leq 3 \kappa . \label{eq:boundskappa3.1} \end{align}

(The inner-product and norm bounds for $M$, $M_{\operatorname{\mathbb {Q}}}$ from Lemma 49 of [ SY25 ] are formalized only in the generalized forms used by corollary 49.)

Proof ▶

See [ SY25 ] , Lemma 49.

Corollary 49

✓

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

\[ A = \frac{\langle M P, M(P-Q)\rangle - 2 \varepsilon \| P-Q\| \cdot (\sqrt{2}+\varepsilon )}{ \big(\| M P\| +\sqrt{2} \varepsilon \big) \cdot \big(\| M(P-Q)\| +2 \sqrt{2} \varepsilon \big)} \]

as well as

\[ A_{\operatorname{\mathbb {Q}}} = \frac{\langle M_{\operatorname{\mathbb {Q}}} \widetilde{P}, M_{\operatorname{\mathbb {Q}}} (\widetilde{P}-\widetilde{Q})\rangle - 10\kappa - 2 \varepsilon ( \| \widetilde{P}-\widetilde{Q}\| + 2 \kappa ) \cdot (\sqrt{2}+\varepsilon )}{ \big(\| M_{\operatorname{\mathbb {Q}}} \widetilde{P}\| _{+}+\sqrt{2} \varepsilon + 3\kappa \big) \cdot \big(\| M_{\operatorname{\mathbb {Q}}}(\widetilde{P}-\widetilde{Q})\| _{+}+2 \sqrt{2} \varepsilon + 6\kappa \big)}. \]

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.)

Proof ▶

See [ SY25 ] , Corollary 51.

Theorem 50 Rational Local Theorem

✓

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

\[ (-1)^{\sigma _P} \langle \overline{X_1},\widetilde{P}_i\rangle {\gt}\sqrt{2}\varepsilon + 3\kappa \quad \text{and} \quad (-1)^{\sigma _Q} \langle \overline{X_2}, \widetilde{Q}_i\rangle {\gt}\sqrt{2}\varepsilon + 3\kappa , \tag {A$^{\operatorname{\mathbb {Q}}}_\varepsilon $} \]

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

\[ \frac{\langle \overline{M_2}\widetilde{Q}_i,\overline{M_2}(\widetilde{Q}_i-\widetilde{Q}_j)\rangle - 10\kappa - 2 \varepsilon ( \| \widetilde{Q}_i-\widetilde{Q}_j\| _{+} + 2 \kappa ) \cdot (\sqrt{2}+\varepsilon )}{ \big(\| \overline{M_2}\widetilde{Q}_i\| _{+}+\sqrt{2} \varepsilon + 3\kappa \big) \cdot \big(\| \overline{M_2}(\widetilde{Q}_i-\widetilde{Q}_j)\| _{+}+2 \sqrt{2} \varepsilon + 6\kappa \big)} {\gt} \frac{\sqrt{5} \varepsilon + \delta }{r}, \tag {B$^{\operatorname{\mathbb {Q}}}_\varepsilon $} \]

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

\[ \delta \geq \max _{i=1,2,3}\left\| R_{\operatorname{\mathbb {Q}}}(\overline{\alpha }) \overline{M_1}\widetilde{P}_i-\overline{M_2}\widetilde{Q}_i\right\| _{+}/2 + 3\kappa . \]

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

\[ (\theta _1, \varphi _1, \theta _2, \varphi _2, \alpha ) \in [\overline{\theta }_1\pm \varepsilon ,\overline{\varphi }_1\pm \varepsilon ,\overline{\theta }_2\pm \varepsilon ,\overline{\varphi }_2\pm \varepsilon ,\overline{\alpha }\pm \varepsilon ] \subseteq \operatorname{\mathbb {R}}^5. \]

(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.)

Proof ▶