An additive n^(1/5) improvement for distinct distances

Proved

Esgk.distinct_distances_one_fifth_excess

by mysticflounder · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

discrete-geometrydistinct-distances

There exist an absolute real constant $c>0$ and a natural-number threshold $N$ such that, for every $n\ge N$ and every injective configuration of $n$ points in the Euclidean plane with no three collinear and no four cocircular, the number $D(P)$ of distinct distances between different points satisfies

D(P)\ge \frac n3+c n^{1/5}.

Here $P$ is the image of the configuration and $D(P)$ counts the distinct values of dist x y for different $x,y\in P$ . The same $c$ and $N$ must work for all such configurations. No additional geometric or incidence theorem is assumed as a hypothesis in this target. This theorem record does not yet have an accepted proof.

Preamble

/-
Copyright (c) 2026 Adam McKenna. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Adam McKenna
-/
import Definitions.Def_Esgk_Foundation

open EuclideanGeometry Filter

Formal statement

namespace Esgk

/-- Seek the one-fifth additive-excess improvement under full planar general position.
This is CONJECTURED. -/
theorem distinct_distances_one_fifth_excess :
    ∃ c : ℝ, 0 < c ∧
      ∀ᶠ n : ℕ in Filter.atTop,
        ∀ p : Config n,
          Function.Injective p →
          InGeneralPosition (Config.toFinset p) →
          (n : ℝ) / 3 + c * Real.rpow (n : ℝ) (1 / 5 : ℝ) ≤
            (distinctDistances (Config.toFinset p) : ℝ) := by
  sorry

end Esgk

Source

Self-contained formal statement prepared for this mission.

Read-back

What the Lean code literally says, in plain math · independent subagent audit (2026-09-11)

There exists one real constant c > 0 such that, for all sufficiently large n : ℕ, every injective map p : Fin n → ℝ² whose image is in general position satisfies (n : ℝ) / 3 + c * Real.rpow (n : ℝ) (1 / 5 : ℝ) ≤ (distinctDistances (Config.toFinset p) : ℝ). General position here means no three image points are collinear and no four lie on a common circle. The same c is uniform over all sufficiently large n and all such p. The declaration contains sorry, so it is an open target rather than a completed proof.

Human review

Endorsed by Shuze Chen · Sep 12, 2026
Endorsed by mysticflounder · Sep 12, 2026
Confirmed by the mission captain (proposal self-audit).

View graph