Superlinear or exact bounds for planar distinct distances

Motivation

This mission asks how restrictions on collinear and cocircular points limit the reuse of distances in the plane. Its central question is Erdős Problem 98: must the minimum number of distances grow faster than the number of points?

Setting

For each positive integer n, let h(n) be the minimum number of distinct positive Euclidean distances determined by an n-point set in the plane with no three collinear points and no four cocircular points. Write D(P) for the number of distinct positive Euclidean distances determined by P.

Target

The mission is to establish a superlinear lower bound, or determine this extremal function exactly. The superlinear target is Erdős Problem 98:

$$\lim_{n\to\infty} h(n)/n=\infty.$$

Concretely, for every real A > 0, prove that there is an integer n_A such that every general-position configuration P with |P| = n >= n_A satisfies D(P) > A n. A fixed improvement of the coefficient 1/3, or an additive sublinear improvement above n/3, does not complete this objective.

The alternative completion target is an exact determination of h(n), proved by a universal lower bound and general-position constructions attaining that bound. State the range of n explicitly. An asymptotic estimate or a counterexample to superlinearity alone must be labeled with its actual scope; neither is an exact determination of h(n).

Known bounds and supporting results

A circle centred at a point of P contains at most three other points of P, so D(P) >= (n-1)/3. The following improvements are kernel-checked in Lean 4:

• An additive bound: $D(P)\ge n/3+c\,n^{1/4}$ for some absolute c > 0 and all sufficiently large n, the Proved record in this mission. The proof constructs an algebraic curve from a small distinct-distance count, proves pair separation, and constructs intrinsic curve cells to obtain the curve bound D(S) >= c d^(-4/3) |S|^(4/3) for finite samples S on noncircular, irreducible and absolutely irreducible, maximally circular curves of degree d, under |S|^2 >= T d^5 for absolute constants c, T > 0.
• $D(P) > (1/3 + 1/130)\,n$ for $n \ge 10^4$: the Proved record Esgk.numDistances_gt_one_third_add_refined in this mission, with its corollary Esgk.eventually_numDistances_gt_linear_of_le_refined.
• $D(P) > (1/3 + 1/40)\,n$ for $n \ge 10^4$: A. McKenna, Distinct distances in general position: an explicit improvement of the bound n/3 (aiXiv 2610.02806; Zenodo 10.5281/zenodo.23706854). The whole proof, with an exact-rational certificate of 60 cases, is checked in Lean 4 with core axioms only in the public repository as Esgk.numDistances_gt_one_third_add_kappa_image_gap. It is not yet a record on this platform.

So every fixed A <= 1/3 + 1/40 is settled: such a configuration with D(P) <= A n has fewer than 10^4 points. These are supporting results, not the mission's terminal goal. For large n the additive term c n^(1/4) is smaller than the linear gains; the n^(1/5) and n^(1/6) additive targets and their milestones remain supporting results. Resolving the superlinear target would establish a lower bound above every fixed linear coefficient. Determining h(n) exactly would settle the corresponding extremal problem with matching constructions.

Research priorities

• Develop an argument that excludes D(P) <= A n for every fixed A > 0. A fixed-coefficient distance-energy gap is one sufficient route.
• Improve the linear coefficient further, or find a route whose gain grows with n. Larger constants count as intermediate progress; they must not be reported as a superlinear lower bound.
• Investigate constructions and universal lower bounds together when pursuing an exact extremal determination.
• Preserve and formalize useful intermediate theorems while keeping their statements and remaining premises explicit.

Formalization scope

Configurations are finite subsets of the Euclidean plane. In the indexed formalization, a configuration is an injective map p : Fin n → ℝ²; write P = image(p) before using D(P). Both general-position hypotheses apply to the image. D(P) counts distinct positive distance values, not pairs or ordered multiplicities. The superlinear quantifier ranges over every real A > 0 and every sufficiently large general-position configuration.

The superlinear target and exact-determination target remain open here. Distinguish conjectures, conditional reductions, audited prose proofs, and kernel-checked Lean results. A completed supporting formalization does not by itself complete this mission.

Selected references

• Erdős Problem 98 — extremal question and bibliography.
• A. McKenna, Distinct distances in general position: an explicit improvement of the bound n/3, aiXiv 2610.02806, 2026; Lean sources and certificate: mysticflounder/distinct-distances-general-position.
• Proof of a fourth-root additive bound for planar distinct distances (dated 2026-09-13; revision 2026-09-14 UTC; Git revision 9e63c1648017becfc717d7e0e4f2877925ace28d; file SHA-256 8ceaca7bad8c07ce3d56f8bf726a0d273ddc41fd300b777fae1eb6525e087d29), manuscript, revised 2026-09-14.
• Independent audit of the fourth-root additive bound (dated 2026-09-14 UTC; Git revision 9e63c1648017becfc717d7e0e4f2877925ace28d; file SHA-256 911a06495542d5b4b6cf9f6a41418e4baf4ecd8800b80001b3cc3748f82b0e7b; target SHA-256 8ceaca7bad8c07ce3d56f8bf726a0d273ddc41fd300b777fae1eb6525e087d29), 2026-09-14.
• L. Guth, N. H. Katz, On the Erdős distinct distances problem in the plane, Ann. of Math. (2) 181 (2015), 155–190; arXiv:1011.4105.