Close pair among three equidistant points of a thin annulus, radius at most $\sqrt{3}\,\rho$

Let $c,p\in\mathbb R^2$, let $q_0,q_1,q_2\in\mathbb R^2$, and let $\rho,x,\sigma,\kappa,\gamma,t$ be real numbers such that

1. $\rho>0$, $\sigma>0$, $\sigma^2\le 1-x$, $\kappa>0$, $\gamma\ge 0$ and $\gamma^2<1$;
2. $1\le 2\sigma\gamma\kappa$, $3\le 4\gamma^2\sigma^2$, $\kappa^2x+1\le 2\gamma\kappa$ and $(3+x)^2\le 12\gamma^2$;
3. $4\kappa^2x^2\le t$ and $x^2\le 4\sigma^2(1-\gamma^2)\,t$.

Assume that $p,q_0,q_1,q_2$ lie in the closed annulus

that $q_0,q_1,q_2$ are equidistant from $p$, that is $|p-q_i|=|p-q_j|$ for all $i,j$, and that $|p-q_i|^2\le 3\rho^2$. Then there are indices $i\ne j$ with

The points $q_i$ need not be distinct.

This is a scale-free close-pair statement for three points of a thin annulus on a circle of radius at most $\sqrt3\,\rho$ about a point of the annulus. All parameter conditions are polynomial inequalities, so for rational parameters they can be checked by exact arithmetic. With $c$ the centroid of a point configuration and $\rho$ its outer radius, it gives close pairs among configuration points that lie on a common circle about another configuration point.

Formalization Note Points are elements of EuclideanSpace ℝ (Fin 2), the triple is a function Fin 3 → ℝ², and all thresholds are stated for squared distances.