Skip to main content
added 8 characters in body
Source Link
Jason Rute
  • 6.3k
  • 2
  • 30
  • 53

Yes, it is computable. Use the decidability of the theory of the real numbers $(\mathbb{R}, 0, 1, \times, +, <)$. With a very little standard work, you can define $\mathbb{R}^3$, vector addition, and the norm function $|x|$. Then using the decidability of real-closed fields search for the minimum $R \in \mathbb{N}$ such that the following is true: $$ \exists x_0, ..., x_n \in \mathbb{R}^3 \left(\bigwedge_{i \neq j} |x_i - x_j| \geq r_i + r_j \quad \land\quad \bigwedge_{i}|x_i| \leq R\right) $$$$ \exists x_0, ..., x_n \in \mathbb{R}^3 \left(\bigwedge_{i \neq j} |x_i - x_j| \geq r_i + r_j \quad \land\quad \bigwedge_{i}|x_i| + r_i \leq R\right) $$ This search will terminate before $R > r_1 + ... r_n$$R > r_1 + ... + r_n$.


If you relax it to reals, then it is also computable. First, we can fit the balls within a large sphere of center the origin and radius $R' = r_1 + ... + r_n$ by lining the balls in a line.

Then you can use compactness. The function $R(x_1, ..., x_n) = \min_i (|x_i| + r_i)$ is computable and it describes the minimal radius $R$ which fits all the balls if they have center $x_i \in \mathbb{R}^3$. Now the desired value $R$ is equal to $\inf_{x_1, ..., x_n} R(x_1, ..., x_n)$ where the minimum is over all $x_i, x_j$ such that $|x_i| \leq R'$ and $|x_i - x_j| \geq r_i + r_j$. Classically, this this is an infimum over a continuous function on a compact domain so it is realized. Computably, this minimum is also computable since it is the minimum of a computable function whose domain is what is called a "computable subset of $\mathbb{R}^3$" in the computable analysis literature.

Yes, it is computable. Use the decidability of the theory of the real numbers $(\mathbb{R}, 0, 1, \times, +, <)$. With a very little standard work, you can define $\mathbb{R}^3$, vector addition, and the norm function $|x|$. Then using the decidability of real-closed fields search for the minimum $R \in \mathbb{N}$ such that the following is true: $$ \exists x_0, ..., x_n \in \mathbb{R}^3 \left(\bigwedge_{i \neq j} |x_i - x_j| \geq r_i + r_j \quad \land\quad \bigwedge_{i}|x_i| \leq R\right) $$ This search will terminate before $R > r_1 + ... r_n$.


If you relax it to reals, then it is also computable. First, we can fit the balls within a large sphere of center the origin and radius $R' = r_1 + ... + r_n$ by lining the balls in a line.

Then you can use compactness. The function $R(x_1, ..., x_n) = \min_i (|x_i| + r_i)$ is computable and it describes the minimal radius $R$ which fits all the balls if they have center $x_i \in \mathbb{R}^3$. Now the desired value $R$ is equal to $\inf_{x_1, ..., x_n} R(x_1, ..., x_n)$ where the minimum is over all $x_i, x_j$ such that $|x_i| \leq R'$ and $|x_i - x_j| \geq r_i + r_j$. Classically, this this is an infimum over a continuous function on a compact domain so it is realized. Computably, this minimum is also computable since it is the minimum of a computable function whose domain is what is called a "computable subset of $\mathbb{R}^3$" in the computable analysis literature.

Yes, it is computable. Use the decidability of the theory of the real numbers $(\mathbb{R}, 0, 1, \times, +, <)$. With a very little standard work, you can define $\mathbb{R}^3$, vector addition, and the norm function $|x|$. Then using the decidability of real-closed fields search for the minimum $R \in \mathbb{N}$ such that the following is true: $$ \exists x_0, ..., x_n \in \mathbb{R}^3 \left(\bigwedge_{i \neq j} |x_i - x_j| \geq r_i + r_j \quad \land\quad \bigwedge_{i}|x_i| + r_i \leq R\right) $$ This search will terminate before $R > r_1 + ... + r_n$.


If you relax it to reals, then it is also computable. First, we can fit the balls within a large sphere of center the origin and radius $R' = r_1 + ... + r_n$ by lining the balls in a line.

Then you can use compactness. The function $R(x_1, ..., x_n) = \min_i (|x_i| + r_i)$ is computable and it describes the minimal radius $R$ which fits all the balls if they have center $x_i \in \mathbb{R}^3$. Now the desired value $R$ is equal to $\inf_{x_1, ..., x_n} R(x_1, ..., x_n)$ where the minimum is over all $x_i, x_j$ such that $|x_i| \leq R'$ and $|x_i - x_j| \geq r_i + r_j$. Classically, this this is an infimum over a continuous function on a compact domain so it is realized. Computably, this minimum is also computable since it is the minimum of a computable function whose domain is what is called a "computable subset of $\mathbb{R}^3$" in the computable analysis literature.

Source Link
Jason Rute
  • 6.3k
  • 2
  • 30
  • 53

Yes, it is computable. Use the decidability of the theory of the real numbers $(\mathbb{R}, 0, 1, \times, +, <)$. With a very little standard work, you can define $\mathbb{R}^3$, vector addition, and the norm function $|x|$. Then using the decidability of real-closed fields search for the minimum $R \in \mathbb{N}$ such that the following is true: $$ \exists x_0, ..., x_n \in \mathbb{R}^3 \left(\bigwedge_{i \neq j} |x_i - x_j| \geq r_i + r_j \quad \land\quad \bigwedge_{i}|x_i| \leq R\right) $$ This search will terminate before $R > r_1 + ... r_n$.


If you relax it to reals, then it is also computable. First, we can fit the balls within a large sphere of center the origin and radius $R' = r_1 + ... + r_n$ by lining the balls in a line.

Then you can use compactness. The function $R(x_1, ..., x_n) = \min_i (|x_i| + r_i)$ is computable and it describes the minimal radius $R$ which fits all the balls if they have center $x_i \in \mathbb{R}^3$. Now the desired value $R$ is equal to $\inf_{x_1, ..., x_n} R(x_1, ..., x_n)$ where the minimum is over all $x_i, x_j$ such that $|x_i| \leq R'$ and $|x_i - x_j| \geq r_i + r_j$. Classically, this this is an infimum over a continuous function on a compact domain so it is realized. Computably, this minimum is also computable since it is the minimum of a computable function whose domain is what is called a "computable subset of $\mathbb{R}^3$" in the computable analysis literature.