Return to Answer

This could also be solved by quantifier elimination, and perhaps someone with more knowledge of quantifier elimination can see how to do it feasibly.

A box of side lengths $(a,b,c)$ fits inside a box of side lengths $(x,y,z)$ iff there are vectors $(\mathbf{t},\mathbf u,\mathbf{v})$ for the sides satisfying: \begin{gather*} \begin{aligned} \mathbf{t}\cdot\mathbf{t}=a^2,&& & \mathbf{u}\cdot\mathbf{u}=b^2,&& \mathbf{v}\cdot\mathbf{v}=c^2, \\ \mathbf{t}\cdot\mathbf{u}=0,&&& \mathbf{u}\cdot\mathbf{v}=0,&& \mathbf{v}\cdot\mathbf{t}=0, \end{aligned} \\ \pm\mathbf{t} \pm \mathbf{u} \pm \mathbf{v} \le (x,y,z) \end{gather*} where the last line represents three coordinate inequalities for each choice of signs. In other words, we are checking a statement of the form $\exists t_i t_j t_k u_i u_j u_k v_i v_j v_k\ \phi$, where $\phi$ is the conjunction of 6 equalities and 24 inequalities in those 9 bound variables and in $a$, $b$, $c$, $x$, $y$, $z$.

Quantifier elimination should then provide some list of polynomial inequalities in $a$, $b$, $c$, $x$, $y$, $z$ which together are equivalent to the small box fitting inside the large box.

Update: This works in the 2-d case, with interesting results. Assuming that $0<a<b$ and $0<x<y$, the $a\times b$ rectangle can fit inside the $x\times y$ rectangle iff either: $$a \le x$$ $$b \le y$$ or: $$a \le x$$ $$a^2+b^2 \le x^2+y^2$$ $$\phantom{(ax+by)^2+}(b^2-a^2)^2 \le (ax-by)^2+(ay-bx)^2$$

This could also be solved by quantifier elimination, and perhaps someone with more knowledge of quantifier elimination can see how to do it feasibly.

A box of side lengths $(a,b,c)$ fits inside a box of side lengths $(x,y,z)$ iff there are vectors $(\mathbf{t},\mathbf u,\mathbf{v})$ for the sides satisfying: \begin{gather*} \begin{aligned} \mathbf{t}\cdot\mathbf{t}=a^2,&& & \mathbf{u}\cdot\mathbf{u}=b^2,&& \mathbf{v}\cdot\mathbf{v}=c^2, \\ \mathbf{t}\cdot\mathbf{u}=0,&&& \mathbf{u}\cdot\mathbf{v}=0,&& \mathbf{v}\cdot\mathbf{t}=0, \end{aligned} \\ \pm\mathbf{t} \pm \mathbf{u} \pm \mathbf{v} \le (x,y,z) \end{gather*} where the last line represents three coordinate inequalities for each choice of signs. In other words, we are checking a statement of the form $\exists t_i t_j t_k u_i u_j u_k v_i v_j v_k\ \phi$, where $\phi$ is the conjunction of 6 equalities and 24 inequalities in those 9 bound variables and in $a$, $b$, $c$, $x$, $y$, $z$.

Quantifier elimination should then provide some list of polynomial inequalities in $a$, $b$, $c$, $x$, $y$, $z$ which together are equivalent to the small box fitting inside the large box.

Update: This works in the 2-d case, with interesting results. Assuming that $0<a<b$ and $0<x<y$, the $a\times b$ rectangle can fit inside the $x\times y$ rectangle iff either: $$a \le x$$ $$b \le y$$ or: $$a \le x$$ $$\phantom{(ax+by)^2+}(b^2-a^2)^2 \le (ax-by)^2+(ay-bx)^2$$

This could also be solved by quantifier elimination, and perhaps someone with more knowledge of quantifier elimination can see how to do it feasibly.

A box of side lengths $(a,b,c)$ fits inside a box of side lengths $(x,y,z)$ iff there are vectors $(\mathbf{t},\mathbf u,\mathbf{v})$ for the sides satisfying: \begin{gather*} \begin{aligned} \mathbf{t}\cdot\mathbf{t}=a^2,&& & \mathbf{u}\cdot\mathbf{u}=b^2,&& \mathbf{v}\cdot\mathbf{v}=c^2, \\ \mathbf{t}\cdot\mathbf{u}=0,&&& \mathbf{u}\cdot\mathbf{v}=0,&& \mathbf{v}\cdot\mathbf{t}=0, \end{aligned} \\ \pm\mathbf{t} \pm \mathbf{u} \pm \mathbf{v} \le (x,y,z) \end{gather*} where the last line represents three coordinate inequalities for each choice of signs. In other words, we are checking a statement of the form $\exists t_i t_j t_k u_i u_j u_k v_i v_j v_k\ \phi$, where $\phi$ is the conjunction of 6 equalities and 24 inequalities in those 9 bound variables and in $a$, $b$, $c$, $x$, $y$, $z$.

Quantifier elimination should then provide some list of polynomial inequalities in $a$, $b$, $c$, $x$, $y$, $z$ which together are equivalent to the small box fitting inside the large box.

This could also be solved by quantifier elimination, and perhaps someone with more knowledge of quantifier elimination can see how to do it feasibly.

A box of side lengths $(a,b,c)$ fits inside a box of side lengths $(x,y,z)$ iff there are vectors $(\mathbf{t},\mathbf u,\mathbf{v})$ for the sides satisfying: \begin{gather*} \begin{aligned} \mathbf{t}\cdot\mathbf{t}=a^2,&& & \mathbf{u}\cdot\mathbf{u}=b^2,&& \mathbf{v}\cdot\mathbf{v}=c^2, \\ \mathbf{t}\cdot\mathbf{u}=0,&&& \mathbf{u}\cdot\mathbf{v}=0,&& \mathbf{v}\cdot\mathbf{t}=0, \end{aligned} \\ \pm\mathbf{t} \pm \mathbf{u} \pm \mathbf{v} \le (x,y,z) \end{gather*} where the last line represents three coordinate inequalities for each choice of signs. In other words, we are checking a statement of the form $\exists t_i t_j t_k u_i u_j u_k v_i v_j v_k\ \phi$, where $\phi$ is the conjunction of 6 equalities and 24 inequalities in those 9 bound variables and in $a$, $b$, $c$, $x$, $y$, $z$.

Quantifier elimination should then provide some list of polynomial inequalities in $a$, $b$, $c$, $x$, $y$, $z$ which together are equivalent to the small box fitting inside the large box.

Update: This works in the 2-d case, with interesting results. Assuming that $0<a<b$ and $0<x<y$, the $a\times b$ rectangle can fit inside the $x\times y$ rectangle iff either: $$a \le x$$ $$b \le y$$ or: $$a \le x$$ $$a^2+b^2 \le x^2+y^2$$ $$\phantom{(ax+by)^2+}(b^2-a^2)^2 \le (ax-by)^2+(ay-bx)^2$$

This could also be solved by quantifier elimination, and perhaps someone with more knowledge of quantifier elimination can see how to do it feasibly.

A box of side lengths $(a,b,c)$ fits inside a box of side lengths $(x,y,z)$ iff there are vectors $(\mathbf{t,u,v})$ for the sides satisfying: $$\mathbf{t.t}=a^2, \mathbf{u.u}=b^2, \mathbf{v.v}=c^2,$$ $$\mathbf{t.u}=0,\phantom{^2} \mathbf{u.v}=0,\phantom{^2} \mathbf{v.t}=0,\phantom{^2}$$ $$\mathbf{\pm t\pm u\pm v} \le (x,y,z)$$ where the last line represents three coordinate inequalities for each choice of signs. In other words, we are checking a statement of the form $\exists t_i t_j t_k u_i u_j u_k v_i v_j v_k\ \phi$, where $\phi$ is the conjunction of 6 equalities and 24 inequalities in those 9 bound variables and in $a,b,c,x,y,z$.

Quantifier elimination should then provide some list of polynomial inequalities in $a,b,c,x,y,z$ which together are equivalent to the small box fitting inside the large box.

This could also be solved by quantifier elimination, and perhaps someone with more knowledge of quantifier elimination can see how to do it feasibly.

A box of side lengths $(a,b,c)$ fits inside a box of side lengths $(x,y,z)$ iff there are vectors $(\mathbf{t},\mathbf u,\mathbf{v})$ for the sides satisfying: \begin{gather*} \begin{aligned} \mathbf{t}\cdot\mathbf{t}=a^2,&& & \mathbf{u}\cdot\mathbf{u}=b^2,&& \mathbf{v}\cdot\mathbf{v}=c^2, \\ \mathbf{t}\cdot\mathbf{u}=0,&&& \mathbf{u}\cdot\mathbf{v}=0,&& \mathbf{v}\cdot\mathbf{t}=0, \end{aligned} \\ \pm\mathbf{t} \pm \mathbf{u} \pm \mathbf{v} \le (x,y,z) \end{gather*} where the last line represents three coordinate inequalities for each choice of signs. In other words, we are checking a statement of the form $\exists t_i t_j t_k u_i u_j u_k v_i v_j v_k\ \phi$, where $\phi$ is the conjunction of 6 equalities and 24 inequalities in those 9 bound variables and in $a$, $b$, $c$, $x$, $y$, $z$.

Quantifier elimination should then provide some list of polynomial inequalities in $a$, $b$, $c$, $x$, $y$, $z$ which together are equivalent to the small box fitting inside the large box.