we-solve (beta)

Math-2612 · mathematics · Combinatorics

Optimal-order distinct distances in every dimension at least three

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
For each fixed integer $d>=3$, does there exist $c_d>0$ such that every set of $n>=2$ distinct points in $R^d$ determines at least $c_d$ $n^{2/d}$ different Euclidean distances?

Short English statement

For each fixed integer $d>=3$, does there exist $c_d>0$ such that every set of $n>=2$ distinct points in $R^d$ determines at least $c_d$ $n^{2/d}$ different Euclidean distances?

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

Math-2612-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for Math-2612

Higher-dimensional distinct distances: For each fixed d>=3, every n-point set in R^d has at least c_d n^(2/d) distinct distances; no sharp planar bound is asserted.

With the hypotheses and conventions above, the claimed result addresses the whole mathematical assertion on this page.

Optimal-order distinct distances in every dimension at least three

OpenAI's claim

Higher-dimensional distinct distances: For fixed $d\ge3$, the claimed distance lower bound for $n$ distinct points in $\mathbb R^d$ is $c_d n^{2/d}$. The constant depends only on dimension, with no vanishing subpower factor.

Mathematical statement of the claimed result

Mathematical claim 1.
In every fixed integer dimension $d\ge3$, a constant $c_d>0$ is claimed to satisfy \[\left|\{|x-y|:x,y\in P,\ x\ne y\}\right|\ge c_d|P|^{2/d}\] for every finite set $P\subset\mathbb R^d$ of at least two distinct points. The constant depends only on the dimension. This is a global distinct-distance count, not a bound on how often one distance occurs.

Outline of the argument

Higher-dimensional distinct distances: Polynomial interpolation and Hilbert-function estimates track concentration at several degree scales. Geometry of skew-form evaluation flats gives sparse-cone and rich-motion bounds, with exceptional algebraic families treated explicitly. These incidence estimates are combined with the distance reduction in a way that retains a fixed multiplicative constant rather than only the exponent up to a small loss.

Formal verification

Higher-dimensional distinct distances: The pinned catalogue lists no Lean formalization for this result.

This site has not run the Lean development. These links describe OpenAI’s selected formal statements and should be read with their stated scope.

Status caveat

OpenAI reports that an internal model produced the manuscripts. Their arguments have not been independently verified as proofs by this site. Any portion outside the documented formal scope may contain mistakes, and the catalogue label reports the announced mathematical claim.

Sources

Go to contribution →