Convex point sets, equidistant neighbours, and unit-distance counts

Definition

Erdos9796Mission

by mysticflounder · Sep 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

convex-positiondiscrete-geometryerdos-97-96unit-distances

The ambient space is the Euclidean plane. A set is convex-independent when each point is outside the convex hull of the remaining points. A vertex has at least k equidistant neighbours when a positive-radius circle centred there contains at least k members of the set; the radius may vary with the vertex. Unit-distance counts use unordered pairs at distance one, each counted once. For each n, the extremal count is the natural-number supremum over all convex-independent n-point sets. The two proposition names expand to the affirmative Problem 97 statement and Problem 96's asymptotic O(n) statement; neither is assumed true.

Definition code

/-
Copyright 2026 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 Mathlib

/-!
# Combined Erdős Problems 97 and 96 mission vocabulary

The equidistance predicates follow `FormalConjectures/ErdosProblems/97.lean`,
and the convex unit-distance counting definitions follow
`FormalConjectures/ErdosProblems/96.lean` from the Formal Conjectures project.
The source problems are also documented at
<https://www.erdosproblems.com/96> and <https://www.erdosproblems.com/97>.
-/

open Filter

namespace Erdos9796Mission

abbrev Plane := EuclideanSpace ℝ (Fin 2)

def ConvexIndep (S : Set Plane) : Prop :=
  ∀ a ∈ S, a ∉ convexHull ℝ (S \ {a})

def HasNEquidistantPointsAt (n : ℕ) (A : Finset Plane) (p : Plane) : Prop :=
  ∃ r : ℝ, r > 0 ∧ (A.filter fun q ↦ dist p q = r).card ≥ n

def HasNEquidistantPointsOn (n : ℕ) (A B : Finset Plane) : Prop :=
  ∀ p ∈ B, HasNEquidistantPointsAt n A p

def HasNEquidistantProperty (n : ℕ) (A : Finset Plane) : Prop :=
  HasNEquidistantPointsOn n A A

noncomputable def unitDistancePairsCount (A : Finset Plane) : ℕ := by
  classical
  let relation : Plane → Plane → Prop := fun p q ↦ 0 < dist p q ∧ dist p q = 1
  let symmetricRelation : {f : Plane → Plane → Prop // ∀ p q, f p q = f q p} :=
    ⟨relation, by
      intro p q
      exact congrArg (fun d : ℝ => 0 < d ∧ d = 1) (dist_comm p q)⟩
  exact (A.sym2.filter (Sym2.lift symmetricRelation)).card

noncomputable def convexUnitDistanceCounts (n : ℕ) : Set ℕ :=
  {unitDistancePairsCount points |
    (points : Finset Plane) (_ : points.card = n) (_ : ConvexIndep (points : Set Plane))}

noncomputable def maxConvexUnitDistances (n : ℕ) : ℕ :=
  sSup (convexUnitDistanceCounts n)

def Problem97 : Prop :=
  ∀ A : Finset Plane, A.Nonempty → ConvexIndep (A : Set Plane) →
    ¬ HasNEquidistantProperty 4 A

def Problem96 : Prop :=
  (fun n => (maxConvexUnitDistances n : ℝ)) =O[atTop] fun n => (n : ℝ)

end Erdos9796Mission

Source

https://github.com/mysticflounder/erdos-97-96-formalization/blob/757d852766f377f7c1a0ffeeef6d3526bc0cb7a4/lean/Erdos9796Proof/P97/Foundation.lean; https://github.com/mysticflounder/erdos-97-96-formalization/blob/757d852766f377f7c1a0ffeeef6d3526bc0cb7a4/lean/Erdos9796Proof/P96/UpstreamBridge.lean

Read-back

What the Lean code literally says, in plain math · gpt-5.6-luna

Plane is the Euclidean plane, namely the real Euclidean space of functions from a two-element finite index set to $\mathbb{R}$ . For a subset $S$ of this plane, ConvexIndep S says that every $a\in S$ is absent from the convex hull over $\mathbb{R}$ of $S\setminus\{a\}$ . For a natural number $n$ , finite point set $A$ , and point $p$ , HasNEquidistantPointsAt n A p says that there exists a real radius $r>0$ such that at least $n$ members $q$ of $A$ satisfy $\operatorname{dist}(p,q)=r$ ; the point $p$ itself cannot be counted at such a radius, and for $n=0$ the condition is automatic for every $A,p$ , while for a positive $n$ it is impossible when $A$ is empty. HasNEquidistantPointsOn n A B says that this condition holds for every $p\in B$ (vacuously when $B$ is empty), and HasNEquidistantProperty n A is the special case $B=A$ , so it requires every point of $A$ to have some positive radius containing at least $n$ points of $A$ at that exact distance (vacuously when $A$ is empty). unitDistancePairsCount A is the number of unordered pairs of distinct points drawn from $A$ whose mutual distance is exactly $1$ ; the code tests both $0<\operatorname{dist}(p,q)$ and $\operatorname{dist}(p,q)=1$ , and each unordered pair is counted once, so the count is $0$ for a set with fewer than two points. convexUnitDistanceCounts n is the set of natural numbers obtained as unitDistancePairsCount points while points ranges over finite point sets in the plane with exactly $n$ elements and with ConvexIndep (points); repeated numerical counts from different point sets occur only once because this is a set, and if there are no admissible point sets the set is empty. maxConvexUnitDistances n is the natural-number supremum of convexUnitDistanceCounts n, using the natural numbers' convention for a supremum of an empty set.

Human review

Endorsed by Shuze Chen · Sep 8, 2026
Endorsed by mysticflounder · Sep 8, 2026
Confirmed by the mission captain (proposal self-audit).

View graph