Erdős Problem 91

Reference:

• [Er87b] Erdős, P., Some combinatorial and metric problems in geometry. Intuitive geometry (Siófok, 1985) (1987), 167-177.
• [Ko24c] Z. Kovács, A note on Erdős's mysterious remark. arXiv:2412.05190 (2024).
• erdosproblems.com/91

noncomputable def Erdos91.IsOptimal (A : Finset (EuclideanSpace ℝ (Fin 2))) (n : ℕ) : Prop

A set $A$ is 'optimal' if it has $n$ points and achieves the minimum distance count.

Equations

• Erdos91.IsOptimal A n = (A.card = n ∧ EuclideanGeometry.distinctDistances A = EuclideanGeometry.minimalDistinctDistances n)

def Erdos91.DilationEquivSimilar (A B : Finset (EuclideanSpace ℝ (Fin 2))) : Prop

Two finite sets of points in $\mathbb{R}^2$ are similar if one can be mapped to the other by a DilationEquiv.

Equations

• Erdos91.DilationEquivSimilar A B = ∃ (f : EuclideanSpace ℝ (Fin 2) ≃ᵈ EuclideanSpace ℝ (Fin 2)), ⇑f '' ↑A = ↑B

noncomputable def Erdos91.equiTriangle : Finset (EuclideanSpace ℝ (Fin 2))

Equilateral triangle with unit side length, resting on the x-axis with one vertex at the origin.

Equations

• Erdos91.equiTriangle = {!₂[0, 0], !₂[1, 0], !₂[1 / 2, √3 / 2]}

noncomputable def Erdos91.unitSquare : Finset (EuclideanSpace ℝ (Fin 2))

Equations

• Erdos91.unitSquare = {!₂[0, 0], !₂[0, 1], !₂[1, 0], !₂[1, 1]}

noncomputable def Erdos91.circleSeven : Finset (EuclideanSpace ℝ (Fin 2))

Regular 7-gon with unit side length, touching both axes in the first quadrant.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Erdos91.wheelSeven : Finset (EuclideanSpace ℝ (Fin 2))

Wheel graph on 7 vertices (center + regular hexagon) with unit side length, touching both axes in the first quadrant.

Equations

• Erdos91.wheelSeven = {!₂[1, √3 / 2], !₂[2, √3 / 2], !₂[3 / 2, √3], !₂[1 / 2, √3], !₂[0, √3 / 2], !₂[1 / 2, 0], !₂[3 / 2, 0]}

theorem Erdos91.erdos_91.test.equiTriangle_optimal : IsOptimal equiTriangle 3

theorem Erdos91.erdos_91.test.equiTriangle_unique_optimal (A : Finset (EuclideanSpace ℝ (Fin 2))) : IsOptimal A 3 → DilationEquivSimilar A equiTriangle

theorem Erdos91.erdos_91.test.unitSquare_optimal : IsOptimal unitSquare 4

theorem Erdos91.erdos_91.test.circleSeven_optimal : IsOptimal circleSeven 7

theorem Erdos91.erdos_91.test.wheelSeven_optimal : IsOptimal wheelSeven 7

theorem Erdos91.erdos_91.test.dissimilar_circleSeven_wheelSeven : ¬DilationEquivSimilar circleSeven wheelSeven

def Erdos91.UniqueMinimizer (n : ℕ) : Prop

The predicate on $n$ asserting all $A, B\subset \mathbb{R}^2$, with $\lvert A\rvert=n = \lvert B\rvert$, which minimise the number of distinct points for all sets with $n$ elements are similar.

Equations

• Erdos91.UniqueMinimizer n = ∀ (A B : Finset (EuclideanSpace ℝ (Fin 2))), Erdos91.IsOptimal A n → Erdos91.IsOptimal B n → Erdos91.DilationEquivSimilar A B

theorem Erdos91.erdos_91 : (∀ᶠ (n : ℕ) in Filter.atTop, ¬UniqueMinimizer n) ↔ True

Suppose $A\subset \mathbb{R}^2$ has $\lvert A\rvert=n$ and minimises the number of distinct distances between points in $A$. Prove that for large $n$ there are at least two (and probably many) such $A$ which are non-similar.

theorem Erdos91.erdos_91.variants.three : UniqueMinimizer 3

For $n = 3$ the equilateral triangle is the only such set.

theorem Erdos91.erdos_91.variants.four : ¬UniqueMinimizer 4

For $n=4$ the square or two equilateral triangles sharing an edge give two non-similar examples.

theorem Erdos91.erdos_91.variants.five : UniqueMinimizer 5

For $n = 5$ the regular pentagon is the unique such set (which has two distinct distances). Erdős mysteriously remarks in [Er90] this was proved by 'a colleague'. (In [Er87b] this is described as 'a colleague from Zagreb (unfortunately I do not have his letter)'.) A published proof of this fact is provided by Kovács [Ko24c].

theorem Erdos91.erdos_91.variants.six : ¬UniqueMinimizer 6

In [Er87b] on p.171 Erdős says that there are at least two non-similar examples for $n = 6$.

theorem Erdos91.erdos_91.variants.seven : ¬UniqueMinimizer 7

In [Er87b] on p.171 Erdős says that there are at least two non-similar examples for $n = 7$.

theorem Erdos91.erdos_91.variants.eight : ¬UniqueMinimizer 8

In [Er87b] on p.171 Erdős says that there are at least two non-similar examples for $n = 8$.

theorem Erdos91.erdos_91.variants.nine : ¬UniqueMinimizer 9

In [Er87b] on p.171 Erdős says that there are at least two non-similar examples for $n = 9$.