we-solve (beta)

Math-2230 · mathematics · Combinatorics

Distances among Point Sets in $\mathbb{R}^2$ and $\mathbb{R}^3$

Status Partially solved · unsolvedmath.comLLM status Open unverified

Statement

Definitions and mathematical statement

Shared notation.
$\mathbb N$, $\mathbb Z$, $\mathbb Q$, $\mathbb R$, and $\mathbb C$ denote the natural numbers, integers, rationals, reals, and complex numbers, respectively. All additional parameters and hypotheses are specified in the question.
Statement recorded in the supplied source.
For a point set $P$ in $\mathbb{R}^d$, let $f_d(P)$ be the number of unit-distance point pairs: $$f_d(P) = \left| \{ (u,v) \mid u, v \in P, \, \|u-v\| = 1 \} \right| \;;$$ and let $f_d(n)$ be the maximum over all sets of $n$ points: $$f_d(n) = \max_{|P| = n} f_d(P) \;.$$ Further, let $g_d(P)$ denote the number of distinct distances induced by a set of points $P$: $$g_d(P) = \left| \{ \|u-v\| \mid u, v \in P \} \right| \;;$$ and let $g_d(n)$ be the minimum over all sets of $n$ points: $$g_d(n) = \min_{|P|=n} g_d(P) \;.$$ Give upper and lower bounds on $f_d(n)$ and $g_d(n)$, particularly for $d=2$ and $d=3$.

Formulation references: [S1], [S2], [S3].

Short English statement

For a point set $P$ in $\mathbb{R}^d$, let $f_d(P)$ be the number of unit-distance point pairs: $$f_d(P) = \left| \{ (u,v) \mid u, v \in P, \, \|u-v\| = 1 \} \right| \;;$$ and let $f_d(n)$ be the maximum over all sets of $n$ points: $$f_d(n) = \max_{|P| = n} f_d(P) \;.$$ Further, let $g_d(P)$ denote the number of distinct distances induced by a set of points $P$: $$g_d(P) = \left| \{ \|u-v\| \mid u, v \in P \} \right| \;;$$ and let $g_d(n)$ be the minimum over all sets of $n$ points: $$g_d(n) = \min_{|P|=n} g_d(P) \;.$$ Give upper and lower bounds on $f_d(n)$ and $g_d(n)$, particularly for $d=2$ and $d=3$.

Sources

Catalogue entry

Statement licence: CC-BY-4.0 · Source file

Contributions 1

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

OpenAI claim summary for Math-2230

Planar unit-distance power saving: The bound u(n)<=C n^beta with beta<4/3 is an improved planar upper bound, not the conjectured n^(1+o(1)) order, an exact extremal value, or the other bundled dimension/distance questions.

Higher-dimensional distinct distances: The lower bound c_3 n^(2/3), together with the grid upper bound, settles the order of the three-dimensional distinct-distance minimum; the planar distinct-distance and unit-distance maximum clauses remain open.

Almost all planar pins: The theorem supplies n^(1-epsilon) distinct distances from almost every planar pin and therefore globally, but not the sharp planar order or the other three-dimensional and unit-distance clauses.

This page records partial support. Complete resolution of the catalogue question is not established by this record.

Distances among Point Sets in \$
\textbackslash{}
mathbb{R}^2\$ and \$
\textbackslash{}
mathbb{R}^3\$

OpenAI's claim

Planar unit-distance power saving: The unit-distance manuscript claims an absolute exponent $\beta<4/3$ bounding the number of unordered unit pairs by $C n^\beta$; the point configuration is otherwise arbitrary.

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.

Almost all planar pins: For any fixed positive $\varepsilon$, the claimed number of pins determining fewer than $n^{1-\varepsilon}$ nonzero distances is $o(n)$ uniformly over planar $n$-point sets; this is an almost-all-pins conclusion rather than an exact linear lower bound at every pin.

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.
Mathematical claim 2.
For $P\subset\mathbb R^2$ of $n$ distinct points let $u(P)$ count unordered pairs at Euclidean distance $1$, and let $u(n)=\max_{|P|=n}u(P)$. The claim is that absolute constants $C<\infty$ and $1\le\beta<4/3$ satisfy \[u(n)\le Cn^\beta\quad(n\ge0).\] The unspecified saving $4/3-\beta>0$ improves the known exponent but does not establish every proposed near-linear bound.
Mathematical claim 3.
For finite $P\subset\mathbb R^2$ put $D_x(P)=\{|y-x|:y\in P\setminus\{x\}\}$ and $k_P(x,y)=|\{z\in P\setminus\{x\}:|z-x|=|y-x|\}|$. The claim states that for every $s>0$, \[\sup_{|P|=n}\frac{|\{(x,y)\in P^2:x\ne y,\ k_P(x,y)\ge n^s\}|}{n(n-1)}\longrightarrow0.\] Consequently, for every $\epsilon>0$, $\sup_{|P|=n}|\{x:|D_x(P)|<n^{1-\epsilon}\}|/n\to0$. Thus all but $o(n)$ pins determine at least $n^{1-\epsilon}$ distances, uniformly over the configuration; the sharp $n/\sqrt{\log n}$ global scale is not asserted.

Outline of the argument

Planar unit-distance power saving: A near-extremal incidence sequence is transferred to algebraic configurations and analyzed using distance identities over a negligible-height coefficient field. After differentiating those identities, valuations distinguish the individual radicands and allow independent square-root sign changes. One unused sign change contradicts the differentiated system; a separate exclusion of popular unit circles handles the possible square-class failure, preventing approach to exponent $4/3$.

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.

Almost all planar pins: An extremal pair graph is extracted from large distance fibers while retaining nonconcentration within those fibers. Real-closed-field transfer moves finite configurations into number fields without altering their distance relations. Factorization into two complex coordinates and the product formula balance local closeness partitions across absolute values, giving an incompatibility with the assumed abundance of large fibers.

Formal verification

Family 167 describes Lean coverage for the weak pinned-distance conclusion and the separate fixed-power unit-distance improvement.

Planar unit-distance power saving: The manuscript links PinnedDistances.lean (declaration OAI.WeakPinned.main), PlanarUnitDistances.lean.

The documented selection includes this manuscript’s main assertion; that assertion retains the restrictions stated above.

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

Almost all planar pins: The manuscript links PinnedDistances.lean (declaration OAI.WeakPinned.main), PlanarUnitDistances.lean.

The documented selection includes this manuscript’s main assertion; that assertion retains the restrictions stated above.

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 →