(This question is inspired by Erich's Packing Center.
I'm just asking about circles in squares to keep things simple, since I suspect
any answer would apply just-as-well to the rest of the problems on that page.)
Define $\: \hspace{.04 in}f : \{\hspace{-0.04 in}1,\hspace{-0.03 in}2\hspace{.02 in},\hspace{-0.04 in}3,\hspace{-0.04 in}4,\hspace{-0.04 in}5,...\hspace{-0.04 in}\} \to [0,\hspace{-0.04 in}\scriptsize+\normalsize \infty \hspace{-0.02 in}) \;$ by letting $\hspace{.04 in}f(n)$ be the side length of the smallest square that
$n$ unit circles can be packed inside. $\;\;\;$ (The existence of a minimum follows from compactness.)
In terms of $n$, what upper bounds are known on the size of algebraic representations of $\hspace{.04 in}f(n)$?
I imagine that "algebraic representations" would mean with
$\;$ the constant $-1$
$\;\;\;\;$ and
$\;$ the binary operations plus and times
$\;\;\;\;$ and
$\;$ extracting a root from a single-variable polynomial given
$\;$ its coefficient-vector and an interval that brackets the root
.
The Only Upper Bound I Know:
For each $n$, $\hspace{.04 in}f(n)$ is the smallest value of the unique free variable in a $\Theta(n)$-variable
existential formula over the reals with $\Theta(n)$ other symbols that satisfies the formula.
Since the quantifiers can be eliminated from such a formula in $n^{O(n)}$ time and the operations plus and times are continuous, $\hspace{.04 in}f(n)$ is a solution to a univariate equation of length $n^{O(n)}$ in the first-order theory
of the reals that does not hold identically. $\:$ With some work (to see that size doesn't blow up), one can
see that such equations are equivalent to standard-form single-variable integer-coefficient polynomial equations of length $n^{O(n)}$ that do not hold identically. $\:$ By Theorem 1.2 (or any root separation bound
that's not much worse), $\hspace{.04 in}f(n)$ can be bracketed by an interval whose endpoints are rationals with $n^{O(n)}\hspace{-0.02 in}$-bit denominators. $\;\;\;$ Since $\: 0\leq \hspace{.02 in}f(n) \leq poly(n) \:$ holds for all $n$, those rationals can be chosen so that additionally their numerators are $n^{O(n)}$ bits long. $\;\;\;$ Thus, $\hspace{.04 in}f(n)$ can be given by a rational interval that brackets a root of an integer-coefficient polynomial such that the total size of that representation is $n^{O(n)}$.
Is anything better known?
${}$