Erdős Problem 97

Reference: erdosproblems.com/97

def Erdos97.HasNEquidistantPointsAt (n : ℕ) (A : Finset (EuclideanSpace ℝ (Fin 2))) (p : EuclideanSpace ℝ (Fin 2)) : Prop

A set of points $A$ has n equidistant points at $p$ if there exist at least $n$ other points in $A$ that are equidistant from $p$.

Equations

• Erdos97.HasNEquidistantPointsAt n A p = ∃ r > 0, {q ∈ A | dist p q = r}.card ≥ n

def Erdos97.HasNEquidistantPointsOn (n : ℕ) (A B : Finset (EuclideanSpace ℝ (Fin 2))) : Prop

A set of points $A$ has n equidistant points on a set of points $B$ if for every point in $B$, there exist at least $n$ other points in $A$ that are equidistant from it.

Equations

• Erdos97.HasNEquidistantPointsOn n A B = ∀ p ∈ B, Erdos97.HasNEquidistantPointsAt n A p

def Erdos97.HasNEquidistantProperty (n : ℕ) (A : Finset (EuclideanSpace ℝ (Fin 2))) : Prop

A set of points $A$ has n equidistant property if for every point in $A$, there exist at least $n$ other points in $A$ that are equidistant from it.

Equations

• Erdos97.HasNEquidistantProperty n A = Erdos97.HasNEquidistantPointsOn n A A

def Erdos97.HasNUnitDistancePointsAt (n : ℕ) (A : Finset (EuclideanSpace ℝ (Fin 2))) (p : EuclideanSpace ℝ (Fin 2)) : Prop

A set of points $A$ has n unit distance points at $p$ if there exist at least $n$ other points in $A$ that are at unit distance from $p$.

Equations

• Erdos97.HasNUnitDistancePointsAt n A p = ({q ∈ A | dist p q = 1}.card ≥ n)

def Erdos97.HasNUnitDistancePointsOn (n : ℕ) (A B : Finset (EuclideanSpace ℝ (Fin 2))) : Prop

A set of points $A$ has n unit distance points on a set of points $B$ if for every point in $B$, there exist at least $n$ other points in $A$ that are at unit distance from it.

Equations

• Erdos97.HasNUnitDistancePointsOn n A B = ∀ p ∈ B, Erdos97.HasNUnitDistancePointsAt n A p

def Erdos97.HasNUnitDistanceProperty (n : ℕ) (A : Finset (EuclideanSpace ℝ (Fin 2))) : Prop

A set of points $A$ has n unit distance property if for every point in $A$, there exist at least $n$ other points in $A$ that are at unit distance from it.

Equations

• Erdos97.HasNUnitDistanceProperty n A = Erdos97.HasNUnitDistancePointsOn n A A

theorem Erdos97.erdos_97 : (∀ (A : Finset (EuclideanSpace ℝ (Fin 2))), A.Nonempty → EuclideanGeometry.ConvexIndep ↑A → ¬HasNEquidistantProperty 4 A) ↔ sorry

Does every convex polygon have a vertex with no other 4 vertices equidistant from it?

theorem Erdos97.erdos_97.variants.three_equidistant : ∃ (A : Finset (EuclideanSpace ℝ (Fin 2))), A.Nonempty ∧ EuclideanGeometry.ConvexIndep ↑A ∧ HasNEquidistantProperty 3 A

Erdős originally conjectured this (in [Er46b]) with no 3 vertices equidistant, but Danzer found a convex polygon on 9 points such that every vertex has three vertices equidistant from it (but this distance depends on the vertex). Danzer's construction is explained in [Er87b].

[Er46b] Erdős, P., On sets of distances of $n$ points. Amer. Math. Monthly (1946), 248-250. [Er87b] Erdős, P., Some combinatorial and metric problems in geometry. Intuitive geometry (Siófok, 1985), 167-177.

theorem Erdos97.erdos_97.variants.k_equidistant : (∃ (k : ℕ), ∀ (A : Finset (EuclideanSpace ℝ (Fin 2))), A.Nonempty → EuclideanGeometry.ConvexIndep ↑A → ¬HasNEquidistantProperty k A) ↔ sorry

Erdős also conjectured that there is a $k$ for which every convex polygon has a vertex with no other $k$ vertices equidistant from it.

theorem Erdos97.erdos_97.variants.three_unit_distance : ∃ (A : Finset (EuclideanSpace ℝ (Fin 2))), A.Nonempty ∧ EuclideanGeometry.ConvexIndep ↑A ∧ HasNUnitDistanceProperty 3 A

Fishburn and Reeds [FiRe92] have found a convex polygon on 20 points such that every vertex has three vertices equidistant from it (and this distance is the same for all vertices).

[FiRe92] Fishburn, P. C. and Reeds, J. A., Unit distances between vertices of a convex polygon. Comput. Geom. (1992), 81-91.

def Erdos97.IsCut (V A B : Finset (EuclideanSpace ℝ (Fin 2))) : Prop

A two-part partition $\{A, B\}$ of $V$ is a cut if the convex hulls of $A$ and $B$ are disjoint.

Equations

• Erdos97.IsCut V A B = (A ∪ B = V ∧ Disjoint A B ∧ Disjoint ((convexHull ℝ) ↑A) ((convexHull ℝ) ↑B))

theorem Erdos97.erdos_97.variants.three_unit_distance_cut_min : sInf {n : ℕ | ∃ (V : Finset (EuclideanSpace ℝ (Fin 2))) (A : Finset (EuclideanSpace ℝ (Fin 2))) (B : Finset (EuclideanSpace ℝ (Fin 2))), n = V.card ∧ EuclideanGeometry.ConvexIndep ↑V ∧ A.Nonempty ∧ B.Nonempty ∧ IsCut V A B ∧ HasNUnitDistancePointsOn 3 B A ∧ HasNUnitDistancePointsOn 3 A B} = 20

Fishburn and Reeds [FiRe92] also proved that the smallest $n$ for which there exists a convex $n$-gon and a cut $\{A, B\}$ of its vertices such that $|\{b \in B : d(a, b) = 1\}| ≥ 3$ for all $a \in A$, and $|\{a \in A : d(a, b) = 1\}| ≥ 3$ for all $b \in B$, is $n = 20$.