Five deficiency-threshold branches for planar distinct distances

Proved

Esgk.distinct_distances_deficiency_threshold_alternatives

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, let $D(P)$ be its number of distinct distances, and define the natural deficiency $\sigma$ by

(n-1)+\sigma=3D(P),\qquad s=\sigma+1.

There are absolute positive integers $T,C$ and a threshold $N$ such that, whenever $n\ge N$ , at least one of the following holds:

$n\le3s$ ;
$n\le s^2$ ;
$n\le s$ ;
$n^2<128T s^7$ ;
$n\le32C s^5$ .

The same $T,C,N$ work for every qualifying configuration. These are the exact circle, nonabsolute, small-deficiency, threshold-failure, and threshold-success branches of the distance--Newton bootstrap.

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 deficiency--Newton argument reaches one of five exact numerical branches. -/
theorem distinct_distances_deficiency_threshold_alternatives :
    ∃ T C : ℕ, 0 < T ∧ 0 < C ∧
      ∀ᶠ n : ℕ in Filter.atTop,
        ∀ p : Config n,
          Function.Injective p →
          InGeneralPosition (Config.toFinset p) →
          ∃ σ : ℕ,
            (n - 1) + σ = 3 * distinctDistances (Config.toFinset p) ∧
            let s := σ + 1
            n ≤ 3 * s ∨ n ≤ s ^ 2 ∨ n ≤ s ∨
              n ^ 2 < 128 * T * s ^ 7 ∨ n ≤ 32 * C * s ^ 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 15--16.

View graph