math.MG — Metric Geometry
Orthogonal circles and a fixed-dimensional separated-distance counterexample
A finite set of points in Euclidean space is distance-separated if the lengths of any two different unordered edges differ by at least one. Counting distances shows that an n-point distance-separated set has diameter at least binom(n,2), approximately n^2/2, and Erdős asked whether the diameter must be at least (1-o(1))n^2. Ho showed that the answer is no if the dimension may grow with n. The first version of this paper gave counterexamples with diameter below 0.74n^2 in a single fixed dimension. We give a sharper explicit fixed-dimensional counterexample: for every integer n at least 36354, there is a distance-separated n-point set in R^81794 with diameter strictly below (147/200)n^2 = 0.735n^2. The finite conclusion has an accompanying Lean 4 proof, including minimum distance at least one for distinct points and the actual set diameter bound. As in the first version, this construction replaces each vertex of a large macro simplex by a cluster of points. A standard Gram-deficit completion arranges those clusters on circles in mutually orthogonal planes. The arrangement makes every distance between two clusters an exact, explicit, increasing function of two digits and reduces the number of coordinates from 9m-1 to 3m-1 for m clusters. A single quadratic-residue ruler controls both the distances inside clusters and the digits between them. The proof is self-contained apart from Bertrand's postulate.