FormalConjectures.ErdosProblems.«92»

/-
Copyright 2025 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil

Erdős Problem 92

Both questions here are disproved, by way of Erdős Problem 90. The source says so directly: this is a stronger form of the unit distance conjecture, so the disproof of that conjecture disproves these too. See FormalConjectures.ErdosProblems.«90».

Reference: erdosproblems.com/92

open Filteropen scoped EuclideanGeometrynamespace Erdos92

For a given point x and a set of other points, this function finds the maximum number of points that lie on a single circle centered at x. It does this by grouping the other points by their distance to x and finding the size of the largest group.

noncomputable def maxEquidistantPointsAt (x : ℝ²) (points : Finset ℝ²) : ℕ :=
  letI otherPoints := points.erase x
  letI distances := otherPoints.image (dist x)
  sSup (distances.image fun d ↦ (otherPoints.filter fun p ↦ dist x p = d).card)

This property holds for a set of points A if every point x in A has at least k other points from A that are equidistant from x.

def hasMinEquidistantProperty (k : ℕ) (A : Finset ℝ²) : Prop :=
  A.Nonempty ∧ ∀ x ∈ A, k ≤ maxEquidistantPointsAt x A

The set of all possible values k for which there exists a set of n points satisfying the hasMinEquidistantProperty k. The function f(n) will be the supremum of this set.

noncomputable def possible_f_values (n : ℕ) : Set ℕ :=
  {k | ∃ (points : Finset ℝ²) (_ : points.card = n), hasMinEquidistantProperty k points}

A sanity check to ensure the set of possible f(n) values is bounded above. A trivial bound is n, since the points equidistant from any x form a subset of the other n - 1 points. This ensures sSup is well-defined.


@[category test, AMS 52]
theorem possible_f_values_BddAbove (n : ℕ) : BddAbove (possible_f_values n) := byn:ℕ⊢ BddAbove (possible_f_values n)
  refine ⟨n, fun k hk => ?_⟩n:ℕk:ℕhk:k ∈ possible_f_values n⊢ k ≤ n
  obtain ⟨points, hcard, ⟨x, hx⟩, hall⟩ := hkn:ℕk:ℕpoints:Finset ℝ²hcard:points.card = nhall:∀ x ∈ points, k ≤ maxEquidistantPointsAt x pointsx:ℝ²hx:x ∈ points⊢ k ≤ n
  refine (hall x hx).trans ?_n:ℕk:ℕpoints:Finset ℝ²hcard:points.card = nhall:∀ x ∈ points, k ≤ maxEquidistantPointsAt x pointsx:ℝ²hx:x ∈ points⊢ maxEquidistantPointsAt x points ≤ n
  unfold maxEquidistantPointsAtn:ℕk:ℕpoints:Finset ℝ²hcard:points.card = nhall:∀ x ∈ points, k ≤ maxEquidistantPointsAt x pointsx:ℝ²hx:x ∈ points⊢ sSup ↑(Finset.image (fun d ↦ {p ∈ points.erase x | dist x p = d}.card) (Finset.image (dist x) (points.erase x))) ≤ n
  refine csSup_le' fun m hm => ?_n:ℕk:ℕpoints:Finset ℝ²hcard:points.card = nhall:∀ x ∈ points, k ≤ maxEquidistantPointsAt x pointsx:ℝ²hx:x ∈ pointsm:ℕhm:m ∈ ↑(Finset.image (fun d ↦ {p ∈ points.erase x | dist x p = d}.card) (Finset.image (dist x) (points.erase x)))⊢ m ≤ n
  rw [Finset.mem_coe,n:ℕk:ℕpoints:Finset ℝ²hcard:points.card = nhall:∀ x ∈ points, k ≤ maxEquidistantPointsAt x pointsx:ℝ²hx:x ∈ pointsm:ℕhm:m ∈ Finset.image (fun d ↦ {p ∈ points.erase x | dist x p = d}.card) (Finset.image (dist x) (points.erase x))⊢ m ≤ nn:ℕk:ℕpoints:Finset ℝ²hcard:points.card = nhall:∀ x ∈ points, k ≤ maxEquidistantPointsAt x pointsx:ℝ²hx:x ∈ pointsm:ℕhm:∃ a ∈ Finset.image (dist x) (points.erase x), {p ∈ points.erase x | dist x p = a}.card = m⊢ m ≤ n Finset.mem_imagen:ℕk:ℕpoints:Finset ℝ²hcard:points.card = nhall:∀ x ∈ points, k ≤ maxEquidistantPointsAt x pointsx:ℝ²hx:x ∈ pointsm:ℕhm:∃ a ∈ Finset.image (dist x) (points.erase x), {p ∈ points.erase x | dist x p = a}.card = m⊢ m ≤ nn:ℕk:ℕpoints:Finset ℝ²hcard:points.card = nhall:∀ x ∈ points, k ≤ maxEquidistantPointsAt x pointsx:ℝ²hx:x ∈ pointsm:ℕhm:∃ a ∈ Finset.image (dist x) (points.erase x), {p ∈ points.erase x | dist x p = a}.card = m⊢ m ≤ n] at hmn:ℕk:ℕpoints:Finset ℝ²hcard:points.card = nhall:∀ x ∈ points, k ≤ maxEquidistantPointsAt x pointsx:ℝ²hx:x ∈ pointsm:ℕhm:∃ a ∈ Finset.image (dist x) (points.erase x), {p ∈ points.erase x | dist x p = a}.card = m⊢ m ≤ n
  obtain ⟨d, hd, rfl⟩ := hmn:ℕk:ℕpoints:Finset ℝ²hcard:points.card = nhall:∀ x ∈ points, k ≤ maxEquidistantPointsAt x pointsx:ℝ²hx:x ∈ pointsd:ℝhd:d ∈ Finset.image (dist x) (points.erase x)⊢ {p ∈ points.erase x | dist x p = d}.card ≤ n
  calc ((points.erase x).filter fun p => dist x p = d).card
      ≤ (points.erase x).card := Finset.card_filter_le _ _
    _ ≤ points.card := Finset.card_erase_le
    _ = n := hcard

Let $f(n)$ be maximal such that there exists a set $A$ of $n$ points in $\mathbb^2$ in which every $x \in A$ has at least $f(n)$ points in $A$ equidistant from $x$.

noncomputable def f (n : ℕ) : ℕ := sSup <| possible_f_values n

Is it true that $f(n)\leq n^{o(1)}$?

The source records this as disproved: "This is a stronger form of the unit distance conjecture (see [90]). As such the recent disproof of [90] also disproves this." That disproof is Erdos90.erdos_90, which this repository already records as research solved with the answer False.

@[category research solved, AMS 52]
theorem erdos_92.variants.weak : answer(False) ↔ ∃ o : ℕ → ℝ,
  o =o[atTop] (1 : ℕ → ℝ) ∧ ∀ n, (f n : ℝ) ≤ n^(o n) := by⊢ False ↔ ∃ o, o =o[atTop] 1 ∧ ∀ (n : ℕ), ↑(f n) ≤ ↑n ^ o n
  sorryAll goals completed! 🐙

Or even $f(n) < n^{c/\log\log n}$ for some constant $c > 0$?

Also disproved, and by the weak form rather than separately: since $c/\log\log n \to 0$, the bound $n^{c/\log\log n}$ is of the form $n^{o(1)}$, so this statement implies erdos_92.variants.weak and is false whenever that one is.

@[category research solved, AMS 52]
theorem erdos_92.variants.strong : answer(False) ↔
    ∃ c > 0, ∀ᶠ n in atTop, (f n : ℝ) ≤ n^(c / (n : ℝ).log.log) := by⊢ False ↔ ∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ↑(f n) ≤ ↑n ^ (c / Real.log (Real.log ↑n))
  sorryAll goals completed! 🐙

-- TODO(firsching): formalize the rest of the remarks

end Erdos92