Deficiency bound for equidistant witnesses with no three collinear points

Let $p=(p_1,\dots,p_n)$ be an injective configuration of $n$ points in the plane, with image $P=\{p_1,\dots,p_n\}$, and assume that no three points of $P$ are collinear. For indices $a\ne b$ let

be the number of configuration points equidistant from $p_a$ and $p_b$. Let $D$ be the number of distinct values $|p_i-p_j|$ with $i\ne j$; since $p$ is injective, $D=D(P)$, the number of distinct distances determined by $P$. Then every set $\Phi$ of ordered pairs $(a,b)$ of distinct indices satisfies

The quantity $3D-n+1$ measures how far $D$ lies above $(n-1)/3$. In apex-counting arguments an upper bound for $\alpha$ on the pairs of $\Phi$ turns this inequality into an upper bound for $|\Phi|$.

Formalization Note $\alpha(a,b)$ is (IndexedEquidistantWitnesses p a b).card and $D$ is NumDistancesOrdered p. Indices are elements of Fin n, and the inequality is stated in the real numbers.