Superlinear growth of distinct distances in general position

For every real constant $A>0$, there is a threshold $N_A$ such that, for every natural number $n \ge N_A$ and every injective configuration $p : \operatorname{Fin}(n) \to \mathbb R^2$ whose image has no three collinear points and no four cocircular points, let $P = \operatorname{image}(p)$. The number $D(P)$ of distinct Euclidean distances determined by $P$ satisfies

The threshold may depend on $A$, while the conclusion must hold uniformly for every qualifying configuration of size $n$. Here $D(P)$ counts each distance value once, even when multiple ordered pairs determine it. This is the superlinear-growth target of Erdős Problem 98 and remains an open problem in this Lean formalization.