Erdős Problem 1082

Reference: erdosproblems.com/1082

theorem Erdos1082.erdos_1082.parts.i : True ↔ ∀ (A : Finset (EuclideanSpace ℝ (Fin 2))), EuclideanGeometry.NonTrilinear ↑A → A.card / 2 ≤ EuclideanGeometry.distinctDistances A

Let $A\subset \mathbb{R}^2$ be a set of $n$ points with no three on a line. Does $A$ determine at least $\lfloor n/2\rfloor$ distinct distances?

theorem Erdos1082.erdos_1082.parts.ii : False ↔ ∀ (A : Finset (EuclideanSpace ℝ (Fin 2))), A.Nonempty → EuclideanGeometry.NonTrilinear ↑A → ∃ (a : EuclideanSpace ℝ (Fin 2)) (_ : a ∈ A), A.card / 2 ≤ EuclideanGeometry.distinctDistancesFrom A a - 1

Let $A\subset \mathbb{R}^2$ be a set of $n$ points with no three on a line. Must there exist a single point from which there are at least $\lfloor n/2\rfloor$ distinct distances?

This question has been answered negatively by Xichuan in the comments, who gave a set of $42$ points in $\mathbb{R}^2$, with no three on a line, such that each point determines only $20$ distinct distances.

A smaller counterexample has been formalised here: it comprised of $8$ points, where each point only determines $3$ distances.

This counterexample has originally been found by Heiko Harborth.