Erdős Problem 655

Reference: erdosproblems.com/655

def Erdos655.IsValid (X : Finset (EuclideanSpace ℝ (Fin 2))) : Prop

A collection $x_1, \dots, x_n\in\mathbb{R}^2$ is valid if no circle whose centre is one of the $x_i$ contains three other points.

Equations

• Erdos655.IsValid X = ∀ x ∈ X, ∀ r > 0, ¬3 ≤ (Metric.sphere x r ∩ ↑X).ncard

theorem Erdos655.erdos_655 : True ↔ ∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (X : Finset (EuclideanSpace ℝ (Fin 2))), X.card = n → IsValid X → (1 + c) * ↑n / 2 ≤ ↑(EuclideanGeometry.distinctDistances X)

Let $x_1,\ldots,x_n\in \mathbb{R}^2$ be such that no circle whose centre is one of the $x_i$ contains three other points. Are there at least $$(1+c)\frac{n}{2}$$ distinct distances determined between the $x_i$, for some constant $c>0$ and all $n$ sufficiently large?

Zach Hunter has observed that taking $n$ points equally spaced on a circle disproves one natural interpretation of this conjecture.

theorem Erdos655.erdos_655.variants.general_position : True ↔ ∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (X : Finset (EuclideanSpace ℝ (Fin 2))), X.card = n → IsValid X → EuclideanGeometry.InGeneralPosition X → (1 + c) * ↑n / 2 ≤ ↑(EuclideanGeometry.distinctDistances X)

Let $x_1,\ldots,x_n\in \mathbb{R}^2$ be such that no circle whose centre is one of the $x_i$ contains three other points. Are there at least$$(1+c)\frac{n}{2}$$ distinct distances determined between the $x_i$, for some constant $c>0$ and all $n$ sufficiently large?

In the spirit of related conjectures of Erdős and others, presumably some kind of assumption that the points are in general position (e.g. no three on a line and no four on a circle) was intended.