FormalConjectures/ErdosProblems/958.lean

GitHub source file

3 declarations, 1 contain sorry, 0 declared as axioms

1. def Erdos958.IsEquidistantOnLine A is a set of equidistant points on a line: there are a point a and a non-zero direction v such that A consists of the points a + i • v for 0 ≤ i < #A line 37 source

   Source documentation

   A is a set of equidistant points on a line: there are a point a and a non-zero direction v such that A consists of the points a + i • v for 0 ≤ i < #A.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Finset, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat

   Proof uses: Exists, And, Ne, ENNReal, Eq, Set, Set.ofPred, LT.lt, Finset.card, HAdd.hAdd, HSMul.hSMul

   31 instances, coercions and auxiliary constants left out.

   def IsEquidistantOnLine (A : Finset ℝ²) : Prop :=
   …

2. def Erdos958.IsEquidistantOnCircle Documented declaration: IsEquidistantOnCircle line 43 source

   Source documentation

   A is a set of equidistant points on a circle: there are a centre c, a radius r > 0, an initial angle θ and a non-zero angular step α such that A consists of the points of the circle of centre c and radius r at the angles θ + i * α for 0 ≤ i < #A.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Finset, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat

   Proof uses: Exists, And, LT.lt, Ne, Eq, Set, Set.ofPred, Finset.card, HAdd.hAdd, WithLp, ENNReal, HSMul.hSMul, WithLp.toLp, Matrix.vecCons, Real.cos, HMul.hMul, Real.sin, Matrix.vecEmpty

   31 instances, coercions and auxiliary constants left out.

   def IsEquidistantOnCircle (A : Finset ℝ²) : Prop :=
   …

3. theorem Erdos958.erdos_958 Let $A\subset \mathbb{R}^2$ be a finite set of size $n$, and let $\{d_1,\ldots,d_k\}$ be the set of distances determined by $A$ sorry line 66 source

   Source documentation

   Let $A\subset \mathbb{R}^2$ be a finite set of size $n$, and let $\{d_1,\ldots,d_k\}$ be the set of distances determined by $A$. Let $f(d)$ be the multiplicity of $d$, that is, the number of unordered pairs from $A$ of distance $d$ apart.

   Is it true that $k=n-1$ and $\{f(d_i)\}=\{n-1,\ldots,1\}$ if and only if $A$ is a set of equidistant points on a line or a circle?

   Erdős conjectured that the answer is no, and other such configurations exist.

   This was proved by Clemen, Dumitrescu, and Liu [CDL25], who observed that equidistant points on a short circular arc on a circle of radius $1$, together with the centre, are also an example.

   The classification is asked for all sufficiently large $n$. Small exceptions such as $\{(0,0), (1,0), (0,1), (0,-1)\}$ exist, so the negative answer asserts counterexamples of arbitrarily large size, as in [CDL25].

   depends on sorry what this means

   Statement uses: Iff, False, Exists, Nat, GE.ge, Finset, EuclideanSpace, Real, Fin, OfNat.ofNat, Eq, Finset.card, And, distanceSet, ENNReal, HSub.hSub, Finset.image, distanceMultiplicity, Finset.Icc, Or and 2 more

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   32 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   theorem erdos_958 : answer(False) ↔
       ∃ N : ℕ, ∀ n ≥ N, ∀ A : Finset ℝ², #A = n →
         ((#(distanceSet A) = n - 1 ∧
               (distanceSet A).image (distanceMultiplicity A) = Finset.Icc 1 (n - 1)) →
           (IsEquidistantOnLine A ∨ IsEquidistantOnCircle A)) := by
   …

   Mentions: distanceSet, distanceMultiplicity, Erdos958.IsEquidistantOnLine, Erdos958.IsEquidistantOnCircle