Equal-circle packing constants in the unit square

Point. A point is an ordered pair of real numbers, so the type of points is $\mathbb{R}\times\mathbb{R}$.

sqDist. For any two points $p=(p_1,p_2)$ and $q=(q_1,q_2)$ in $\mathbb{R}\times\mathbb{R}$, define their squared distance by $\operatorname{sqDist}(p,q)=(p_1-q_1)^2+(p_2-q_2)^2$. No distinctness assumption is imposed; in particular, this value is zero when $p=q$.

InInnerSquare. For any real number $r$ and any point $p=(p_1,p_2)\in\mathbb{R}\times\mathbb{R}$, the predicate $\operatorname{InInnerSquare}(r,p)$ means that $r\le p_1\le 1-r$ and $r\le p_2\le 1-r$. The boundary inequalities are inclusive. There is no assumption that $r$ is nonnegative; negative values are permitted, whereas for $r>1/2$ no point satisfies the predicate.

Packable. For every natural number $n$, including zero, and every real number $r$, the predicate $\operatorname{Packable}(n,r)$ means that $0\le r\le 1/2$ and there exists a family of points $p_i=(x_i,y_i)\in\mathbb{R}\times\mathbb{R}$ indexed by $i\in\{0,\ldots,n-1\}$ such that $r\le x_i\le 1-r$ and $r\le y_i\le 1-r$ for every index $i$, and $(2r)^2\le (x_i-x_j)^2+(y_i-y_j)^2$ for every pair of distinct indices $i,j$. Equality in the separation inequality is allowed. Distinct indices are not independently required to have distinct points, so coincident points are allowed when $r=0$. For $n=0$ the family is empty and all indexed conditions are vacuous, leaving exactly $0\le r\le 1/2$.

r_n. For every natural number $n$, including zero, define $r_n$ to be the real supremum of the set of all real numbers $r$ for which $\operatorname{Packable}(n,r)$ holds.

c_n. For every natural number $n$, including zero, define $c_n=n\pi r_n^2$, where $n$ is cast to a real number.