Centroid mass and the distance-annulus radius

For an indexed configuration $p=(p_1,\dots,p_n)$ of points in the plane with centroid $c(p)$ (configCentroid p) and distance values $R(p)=\{|p_i-p_j|: i\ne j\}$, this module defines three real numbers.

1. centroidSquaredMass p: $M(p)=\sum_{i}|p_i-c(p)|^2$.
2. distanceAnnulusRadiusSq p:

3. distanceAnnulusRadius p: the real square root $\rho(p)=\sqrt{\rho^2(p)}$.

For an injective configuration with $n\ge1$ and no four points on a common circle, every $|p_i-c(p)|^2$ is at most $\rho^2(p)$, and the theorem Esgk.thin_annulus_sq_of_noFourCocircular bounds it from below in terms of the number of distinct distances.

Formalization Note The quantity $\rho^2(p)$ is a formula, not a square, and distanceAnnulusRadius applies Real.sqrt, which returns $0$ for negative arguments. For $n=0$ the division by $n$ gives $0$ in Lean.