Natural quintic bound for the distinct-distance deficiency

Proved

Esgk.distinct_distances_deficiency_quintic_nat_bound

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

discrete-geometrydistinct-distances

Let $P$ be an injectively indexed set of $n$ planar points in general position and let $D(P)$ be its number of distinct distances. There are an absolute positive integer $A$ and a threshold $N$ such that, whenever $n\ge N$ , there is a natural deficiency $\sigma$ satisfying

(n-1)+\sigma=3D(P)

and

n\le A(\sigma+1)^5.

The same $A,N$ work for every qualifying configuration. This is the exact natural-number endpoint consumed by the real fifth-root wrapper.

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

/-- The exact natural deficiency satisfies a uniform quintic bound. -/
theorem distinct_distances_deficiency_quintic_nat_bound :
    ∃ A : ℕ, 0 < A ∧
      ∀ᶠ n : ℕ in Filter.atTop,
        ∀ p : Config n,
          Function.Injective p →
          InGeneralPosition (Config.toFinset p) →
          ∃ σ : ℕ,
            (n - 1) + σ = 3 * distinctDistances (Config.toFinset p) ∧
            n ≤ A * (σ + 1) ^ 5 := by
  sorry

end Esgk

Source

Consolidated argument for a fifth-root additive bound (dated 2026-08-25; revision 2026-09-13; Git revision 8a4c11ac6083f1c5e354b1a2556eae086f4b3ee5; file SHA-256 af6ee6023fe1ff3730b492ea3756d240818df46a877abe3b7ac1153fc7c0245c); Sections 2 and 16.3.

View graph