HEXAGONbeta

Separated distances in fixed dimension

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

Contributed by John Tripodo

Version 2 / Oct 15, 2026 / CC BY 4.0

Abstract

A finite Euclidean point set is distance-separated if the lengths of any two distinct unordered edges differ by at least one. Counting gives a diameter lower bound of binom(n,2), whereas Erdős asked for a lower bound with leading term n^2. We give two constructions in fixed dimension. For every 0 < epsilon <= 1/2, put m0 = ceil(8192/epsilon). For every n >= 4m0 there is a distance-separated n-point set in dimension 10m0-1 with diameter < (1/2+epsilon)n^2. A six-cluster construction gives arbitrarily large configurations in R^29 with diameter < 0.998n^2, and an explicit prime-interval bound gives diameter < 0.999n^2 for every n >= 400000. The constructions use two orthogonal circle families to control distances within and between clusters separately. Their common geometric argument reduces to a uniform operator estimate for the first result and three rational positive-definiteness certificates for the second. Lean 4 formalizations accompany the tolerance family and the dimension-29 result for arbitrarily large sizes; the all-size corollary is a written consequence.

Provenance statement

Substantial AI assistance was used in mathematical exploration, proof engineering, source comparison, and writing. This version reorganizes the two-circle tolerance family and dimension-29 construction into shared proof lemmas and adds a written all-size dimension-29 corollary using Dusart's explicit prime-interval theorem. The paper identifies the exact internal Lean endpoints and their source-specific verification scope; the newer complete Lean proof closures are not included in the public package. Exact arithmetic reconstruction code accompanies the paper. No new Lean execution, independent human proof or historical-priority review is asserted. Earlier Palomar and Prove2Me records concern the archived 0.74 theorem only. The public version history and source package are at https://github.com/jjtripodo-lgtm/erdos-670-fixed-dimension .

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
  10. J. Tripodo, Orthogonal circles and a fixed-dimensional separated-distance counterexample , Hexagon preprint hexagon:2610.00254v1 (https://hexagonmath.org/2610.00254?version=1), 15 October 2026.hexagon
Show all 14 referencesShow fewer references
  1. J. Tripodo, Consecutive Euclidean distances within square-root-logarithmic excess of the counting bound , research manuscript, 2026. This is the separate unrestricted-dimensional result; its source identity is recorded in the companion source map.
  2. J. Tripodo, Deterministic all-positive incidence signs , internal research addendum, 11 October 2026. Preserved source identity: fc556ffdd922ee4183c971ad644f1d1ea3903785 . This earlier internal source is cited to distinguish the existing asymptotic order from the later two-circle proof organization; it is not a public deposit.
  3. J. Tripodo, Erdős #670: result and formalization status , 19 October 2026, immutable documentation snapshot 2caf66c (https://github.com/jjtripodo-lgtm/erdos-670-fixed-dimension/blob/2caf66c312c5d498d17e1c150588684b66300e68/PUBLIC_STATUS.md).link
  4. P. Dusart, Estimates of some functions over primes without R.H. , arXiv:1002.0442v1 (https://arxiv.org/abs/1002.0442v1), 2010, Proposition 6.8, p. 8.arXiv

Version history

  1. v1Submitted by John TripodoInitial depositSupersededOct 15, 2026
  2. v2Submitted by John TripodoSubmitted as a new versionCurrentOct 20, 2026