HEXAGONbeta

Orthogonal circles and a fixed-dimensional separated-distance counterexample

Primarily AI-generated textHuman understanding: no partsmath.MG — Metric Geometry

Contributed by John Tripodo ↗

Version 1 / Oct 15, 2026 / CC BY 4.0

Abstract

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.

Provenance statement

Substantial AI assistance was used in mathematical exploration, proof engineering, source comparison, and writing. An AI-generated simplification and readability rewrite informed the construction and presentation. The finite theorem has an accompanying Lean 4 proof. No independent human proof or priority review is asserted.

Tools used

Lean
LeanVersion 4
OpenAI
ChatGPT
Anthropic
Claude Opus

References

  1. P. Erdős, Some unsolved problems , in Combinatorics, Geometry and Probability: A Tribute to Paul Erdős , B. Bollobás and A. Thomason (eds.), Cambridge University Press, 1997, pp. 1--10, Problem 20. doi:10.1017/CBO9780511662034.004 (https://doi.org/10.1017/CBO9780511662034.004).DOI
  2. P. Erdős and P. Turán, On a problem of Sidon in additive number theory, and on some related problems , J. London Math. Soc. 16 (1941), 212--215. doi:10.1112/jlms/s1-16.4.212 (https://doi.org/10.1112/jlms/s1-16.4.212).DOI
  3. Boon Suan Ho, Erdős's diameter conjecture for separated distances fails in high dimensions , 2026, arXiv:2604.15305v1 (https://arxiv.org/abs/2604.15305v1).arXiv
  4. J. Tripodo, Separated Euclidean distances with diameter below 0.74n20.74n^2 in a fixed dimension , research manuscript, 12 October 2026. Public source snapshot , jjtripodo-lgtm/erdos-670-fixed-dimension (https://github.com/jjtripodo-lgtm/erdos-670-fixed-dimension/tree/1e73a12ff1076dd11affadbf619ddbbef587133e), paper/fixed_dimension_670.tex .link
  5. I. J. Schoenberg, Remarks to Maurice Fréchet's article ``Sur la définition axiomatique d'une classe d'espace distanciés vectoriellement applicable sur l'espace de Hilbert'' , Ann. of Math. (2) 36 (1935), 724--732. doi:10.2307/1968654 (https://doi.org/10.2307/1968654).DOI
  6. I. Schur, Bemerkungen zur Theorie der beschränkten Bilinearformen mit unendlich vielen Veränderlichen , J. Reine Angew. Math. 140 (1911), 1--28. doi:10.1515/crll.1911.140.1 (https://doi.org/10.1515/crll.1911.140.1).DOI
  7. G. Sinnamon, Schur's lemma and best constants in weighted norm inequalities , Le Matematiche 57 (2002), fasc. II, 185--204. https://lematematiche.dmi.unict.it/index.php/lematematiche/article/view/207.link
  8. P. L. Robinson, Julia operators and Halmos dilations , arXiv:1803.09329v1, 2018. https://arxiv.org/abs/1803.09329v1.arXiv
  9. P. Erdős, On sets of distances of nn points in Euclidean space , Publ. Math. Inst. Hungar. Acad. Sci. 5 (1960), 165--169. https://users.renyi.hu/~p_erdos/1960-08.pdf.link

Version history

  1. v1Submitted by John TripodoInitial depositCurrentOct 15, 2026