Near enemies: spherical sets project to minimal-energy images in general positionOpen Problem
## Motivation
How few distinct distances can a planar point set determine? The near enemies
of this mission are the closest competitors to the extremal configuration:
points in **no-three-collinear position** (no line through three of them) and
points lying on a common **sphere** — the lattice-sphere slice of
Erdős–Füredi–Pach–Ruzsa is the motivating example. The **bisector energy** of a
set counts ordered quadruples $(a,b,c,d)$ of points for which the pair $a,b$ and
the pair $c,d$ have the same perpendicular bisector; it measures how far the set
is from generic. Lund–Sheffer–de Zeeuw fixed the floor of this statistic:
$2n(n-1)$ is a universal lower bound, and bisector injectivity is sufficient
for equality. The Near Enemy theorem is the projection statement on top of it —
every admissible set admits one generic projection whose image attains that
floor, sits in general position, has zero rotation energy, and carries the
whole distance-transport package.
## Setting
Work with finite sets $P$ of points in the Euclidean plane
(`EuclideanSpace ℝ (Fin 2)`), and in the transport direction with points in
`EuclideanSpace ℝ ι` for a general finite index type. Following
Lund–Sheffer–de Zeeuw, the **bisector energy** is
$$\mathcal{E}(P) = \bigl|\{(a,b,c,d) \in P^4 \;:\; a \neq b,\; c \neq d,\; \mathrm{perpBisector}(a,b) = \mathrm{perpBisector}(c,d)\}\bigr|.$$
The **rotation energy** counts the ordered congruent quadruples whose difference
vectors are neither equal nor opposite, so it discards the translation and
half-turn channels and isolates the proper-rotation one. A linear map $T$ is
**projection-generic** for a set $G$ when exactly two conditions hold: $T$ sends
the difference of any two distinct points of $G$ to a nonzero vector, and for
two distinct unordered pairs of $G$ the images never combine a parallel pair of
differences with an orthogonal midpoint difference. Perpendicular bisectors,
difference classes and distance images are all `Finset` operations.
## Target
The mission goal is the spherical complete profile: for every finite set $G$
lying on a common sphere, in any dimension, there is a linear map $T$ to the
plane whose image satisfies six conclusions at once —
$$\exists\,T:\quad \mathcal{E}(T(G)) = 2|G|(|G|-1) \;\wedge\; \mathcal{E}(T(G)) \le \mathcal{E}(P') \text{ for every } |P'| = |G| \;\wedge\; \mathrm{rotationEnergy}(T(G)) = 0$$
together with injectivity of $T$ on $G$, general position of the image (no three
collinear, no four cospherical), and exact distance transport. The projection is
chosen per set — its very type depends on the ambient dimension — but a single
projection delivers all six conclusions together, and that bundled form is what
downstream incidence arguments consume.
Milestones ascend in five steps: the universal energy floor, the
bisector-injectivity equality case, the attainment of the floor by
projection-generic maps, the existence of such a map for every
no-three-collinear set, and the no-three-collinear transport bundle that the
goal then specialises to the spherical case.
## Significance
Lund–Sheffer–de Zeeuw introduced the extremal picture for bisector energy at
the level of the exact constant. In footnote 1 on p. 538 of the SoCG 2015
version (LIPIcs vol. 34, 537–552) they state that $\mathcal{E}(P) = 2n(n-1)$
when every distinct pair determines a distinct bisector, with the enumeration
of the trivial quadruples that proves the floor. The universal asymptotic form
$\mathcal{E}(P) = \Omega(n^2)$ is a remark in their §3.4.
This mission builds a complete machine-checked development of the
floor, its attainment and the sufficiency direction, from first principles in
Lean 4 over mathlib; the `rotationEnergy` statistic together with the
`rotationEnergy = 0` certificate for the projected image, where
`rotationEnergy(P) = 0` follows from the published "distance Sidon set"
property; and a **single** generic projection of a given set that carries the
bisector floor at the same time as the Erdős–Füredi–Pach–Ruzsa general-position
package. Four of that bundle's six conjuncts are already in
Erdős–Füredi–Pach–Ruzsa 1993, whose Theorem 3.1 supplies them.
Formalizing it matters because the argument composes analysis (generic
projections obtained from nonvanishing of circle determinants), algebra
(inner-product and determinant polynomial witnesses carrying
`linear_combination` certificates) and counting (fiberwise difference-class
tallies) — and the interfaces between the three must agree exactly. The
projection-genericity and polynomial-witness lemmas are reusable for any
Euclidean extremal formalization.
## Difficulty
The hard step is keeping the projection generic through every predicate at once:
a projection that preserves no-three-collinearity can still kill a circle
determinant, or create a coincidence that the counting needs to keep distinct.
The naive first idea — project along a random direction and hope — fails because
each predicate forbids a different algebraic hypersurface of directions; the fix
is a single simultaneous-avoidance argument over the union, with each forbidden
set shown proper by an explicit polynomial witness. That step is the largest
proof in the mission and carries its own milestone.
## Formalization scope
Points are `EuclideanSpace`; finite sets are `Finset`; energies are `ℕ`-valued
statistics. Generic projections are linear maps carrying the explicit
two-clause `ProjectionGeneric` predicate, so there is no hidden regularity
assumption. Dimension is a general `ι` with `[Fintype ι]` wherever the transport
needs it. The goal's only hypothesis is membership of a common sphere;
no-three-collinearity is derived from it rather than assumed, because a line
meets a sphere at most twice. No statement is vacuous: explicit witnesses were
checked in the kernel for the goal and for every milestone.
Welcome contributions: the converse of the equality case — bisector injectivity
is proved here to be sufficient for the floor, and necessity is open in this
development; sharpness examples beyond the Erdős–Füredi–Pach–Ruzsa
configuration; and the incidence assembly that consumes this mission's output.
## Selected references
- B. Lund, A. Sheffer and F. de Zeeuw, Bisector energy and few distinct
distances, Proc. 31st SoCG 2015, LIPIcs vol. 34, 537–552, DOI
[10.4230/LIPIcs.SOCG.2015.537](https://doi.org/10.4230/LIPIcs.SOCG.2015.537);
journal version *Discrete Comput. Geom.* **56** (2016), no. 2, 337–356,
DOI 10.1007/s00454-016-9783-5,
[arXiv:1411.6868](https://arxiv.org/abs/1411.6868). Source of the
bisector-energy statistic and its upper bounds. Footnote 1 on p. 538 of the
SoCG version gives $\mathcal{E}(P) = 2n(n-1)$ for every set whose pairs have
distinct bisectors, with the count of trivial quadruples that proves the
floor; §3.4 (p. 545) gives $\mathcal{E}(P) = \Omega(n^2)$ for every set. The
footnote is not in arXiv:1411.6868v1.
- P. Erdős, Z. Füredi, J. Pach and I. Z. Ruzsa, The grid revisited,
*Discrete Math.* **111** (1993), 189–196,
DOI 10.1016/0012-365X(93)90155-M — the lattice-sphere-slice configuration
that gives this mission its name, and (proof of Theorem 3.1, p. 193) the
generic planar projection that is injective, keeps general position and
transports distances.
- J. Solymosi and T. Tao, An incidence theorem in higher dimensions,
*Discrete Comput. Geom.* **48** (2012), no. 2, 255–280,
DOI 10.1007/s00454-012-9420-x,
[arXiv:1103.2926](https://arxiv.org/abs/1103.2926), §5.1 — the canonical
statement of the generic-projection trick this construction borrows. The same
trick is used in J. Pach and F. de Zeeuw, Distinct distances on algebraic
curves in the plane, *Combin. Probab. Comput.* **26** (2017), no. 1, 99–117,
[arXiv:1308.0177](https://arxiv.org/abs/1308.0177).
- McKenna, Lean formalization (mathlib-only, axiom-clean),
[lean-formalizations](https://github.com/mysticflounder/lean-formalizations),
module `Geometry.Euclidean.NearEnemyTheorem`.
20 thms1 active userReviewed
🏆Completed
Captain: mysticflounder
Pach-de Zeeuw: finite Bezout bound for real plane curvesResearch Paper
## Motivation
The **distinct-distances problem** asks how few distinct distances a finite planar
point set can determine. Guth and Katz proved the near-optimal bound
$\Omega(n / \log n)$ in 2015. Their argument passes through incidence geometry:
distances become incidences between points and curves, and the Elekes–Sharir
framework converts the problem into an incidence bound for lines in
three-space. Pach and de Zeeuw showed the same pipeline works for points on a
fixed algebraic curve, replacing line incidences with curve incidences. The
algebraic prerequisite for that replacement — that two bounded-degree real
plane curves with no shared component meet in finitely many points, with an
explicit degree-dependent bound — is what this mission formalizes.
## Setting
A **real plane curve** here is the real zero set of a nonzero bivariate polynomial
$p \in \mathbb{R}[x, y]$, written $V(p) = \{(x,y) : p(x,y) = 0\}$. Its
**total degree** is the maximum $i+j$ over monomials $x^i y^j$ with nonzero
coefficient. A curve is **irreducible** when its polynomial is irreducible.
The paper says two curves have a **common component** when their polynomials
share a nonconstant factor. The Lean development uses a different, weaker
hypothesis, `NoCommonCurveComponent`: no *infinite* irreducible real curve lies
inside both sets. A shared factor whose real zero set is finite (for example
$x^2 + y^2$) violates the paper's hypothesis but satisfies the Lean one, so the
Lean theorem covers strictly more pairs of curves than the paper's statement.
**Currying** views $p$ as a univariate polynomial in one coordinate whose
coefficients are polynomials in the other. In the Lean code the polynomial
variable is coordinate $0$ and the coefficient (base) variable is coordinate $1$;
this description writes the base coordinate as $x$ and the fiber coordinate as
$y$, so a line $\{x = c\}$ is called **vertical**. The **resultant** of two
curried polynomials is a polynomial in $x$ alone. The development uses one
direction of its defining property: if the two specializations at $x$ share a
real root, the resultant vanishes at $x$. All Lean statements use
`MvPolynomial (Fin 2) ℝ` for plane polynomials and `EuclideanSpace ℝ (Fin 2)`
for points.
## Target
The mission's goal is a finite-intersection bound in the spirit of Theorem 2.1
of Pach–de Zeeuw (Bézout's inequality), but it is not that theorem. It differs
in both directions:
$$ \forall d_1, d_2,\ \exists C > 0,\ \forall C_1, C_2 \text{ of total degree} \le d_1, d_2 \text{ with no common infinite irreducible component}:\quad C_1 \cap C_2 \text{ is finite and } |C_1 \cap C_2| \le C. $$
- The conclusion is an existential degree-dependent constant. The proof's
witness is $C = (d_1+d_2+1)^8 + 1$. The paper's sharp bound $d_1 \cdot d_2$ is
not proved here.
- The hypothesis is the weaker "no common infinite irreducible component"
described above, so the statement is not a formal consequence of the paper's
Theorem 2.1; the shared-finite-factor case is handled separately in the proof
by a singular-point count.
The six milestones are the algebraic inputs: coefficient-root counting, the two
resultant-nonvanishing criteria, the fiber bound, and the two mixed
vertical/nonvertical pair bounds that carry the constant $d_1 \cdot d_2$. The
nonvertical–nonvertical pair bound (`primitive_nonvertical_pair_intersection_bound`)
carries the cruder constant $((d_1+d_2)^2+1)\cdot\max(d_1,d_2)$. Above the
milestones sit the irreducible-pair assembly with constant $(d_1+d_2+1)^4$ and
the factorized assembly with constant $(d_1+d_2+1)^8$, from which the goal
follows.
## Significance
The result is the algebraic input to the Pach–de Zeeuw distinct-distances
theorem for points on curves: without a uniform finite-intersection bound, the
incidence count that drives the distance bound cannot even be stated. The
formalization pins down every constant and every non-degeneracy hypothesis
(non-verticality, no shared infinite component, coprimality) that the argument
consumes.
The proof composes four toolkits — univariate root counting, Sylvester-matrix
resultant degree bounds, normalized-factor decompositions, and a smooth
implicit-function nonsingularity argument — whose interfaces must agree
exactly. The resulting lemmas (resultant criteria, fiber bounds,
partial-derivative degree bounds) are reusable for other real-algebraic
incidence formalizations over `MvPolynomial`.
## Difficulty
The central difficulty is elimination with explicit constants: the resultant
converts a two-variable intersection problem into a one-variable root count,
but every step (currying, specialization, factor-pair summation) must preserve
a usable degree bound, and the degenerate configurations (vertical fibers,
shared factors with finite real zero set, singular points) each need a separate
finite bound.
The textbook route — Bézout's inequality over $\mathbb{C}$, then observing
that real intersection points are complex ones — is not taken, for two
reasons. Mathlib has no plane-curve Bézout theorem to invoke. And under the
weaker Lean hypothesis the two polynomials may share an irreducible factor with
finite real zero set, in which case the complex intersection is infinite and no
complex count applies; that branch is closed by bounding the singular points of
the shared factor instead.
## Formalization scope
Points are `EuclideanSpace ℝ (Fin 2)`; curves are `MvPolynomial (Fin 2) ℝ`
zero sets; finiteness is `Set.Finite` with `Set.ncard` bounds. The development
commits to total degree (not weighted degrees) and to the currying order that
eliminates Lean coordinate $0$; `variable`-style implicit degree bounds
$d_1, d_2$ are explicit `{d₁ d₂ : ℕ}` binders on the platform. No statement is
vacuous: every intersection bound carries the non-degeneracy hypothesis
(non-associated irreducibles, non-divisibility, nonzero partials) that excludes
the infinite-intersection cases. Contributions welcome: the sharp $d_1 d_2$
general bound (currently an existential constant), the paper's hypothesis form
(no common factor at all), and the incidence assembly that consumes this
mission's output.
## Selected references
- János Pach and Frank de Zeeuw, Distinct distances on algebraic curves in the
plane, Combin. Probab. Comput. 26 (2017), no. 1, 99–117,
[arXiv:1308.0177](https://arxiv.org/abs/1308.0177), DOI
10.1017/S0963548316000225. Theorem 2.1 there cites C. G. Gibson, Elementary
Geometry of Algebraic Curves, Lemma 14.4, for Bézout's inequality.
- McKenna, Lean formalization of the algebraic preliminaries and Bézout bound,
[lean-formalizations](https://github.com/mysticflounder/lean-formalizations),
modules `PachDeZeeuw.AlgebraicPrelim` and `PachDeZeeuw.Bezout` (mathlib-only,
axiom-clean).
39 thms1 active userReviewed
🏆Completed
Captain: mysticflounder
Erdős Problems 97 and 96: Convex Point Sets and Unit DistancesOpen Problem
# Closed — negative resolution of Erdős Problems 96 and 97
Adam McKenna closed this mission on 13 September 2026 following **Unit distances in convex polygons**, by **Liam Kruer, Jensen Kohlmeyer, and Liam Price**. Their construction gives strictly convex point sets with Ω(n log log n) unit-distance pairs and arbitrarily large minimum unit-distance degree, answering both questions and the general fixed-k version of Problem 97 negatively.
[Paper and complete Lean source](https://github.com/Leeham06972452/erdos-96-97/tree/0e98f5f9bdaf36007e3eb405cbefe2eda778a9b2). All credit for the counterexample and its formalization belongs to those authors. Adam McKenna prepared the Prove2Me adapters.
**Do not start further proof attempts or solver runs for the affirmative conjectures.** Existing statements, conditional lemmas, partial proofs, and milestones remain as historical work. The owner has authorized closure assuming the external result is correct; individual theorem pages report Prove2Me verification status.
---
## Historical mission description
# Motivation
The mission is to prove the combined open goal
$$
\text{Problem 97} \;\land\; \text{Problem 96}
$$
for finite point sets in strictly convex position in the Euclidean plane.
## Why Problems 97 and 96 belong together
Problem 97 gives the local step needed for Problem 96. Assume Problem 97. Every
nonempty convex-independent finite set then has a vertex with at most three
neighbors at each positive radius, in particular at radius $1$. Delete that
vertex and preserve convex independence. Apply the same step to every subset
created by deletion until no points remain.
Charge each unordered unit-distance pair to the first endpoint deleted. Each
deleted vertex receives at most three charges, so an $n$-point set determines
at most $3n$ unordered unit-distance pairs. This gives the Problem 96 bound
and therefore $O(n)$. The package uses this one-way dependency; it does not
seek a reverse implication.
# Setting
Let $A\subset\mathbb R^2$ be finite. Strict convex position means that every
point of $A$ is an extreme point of the convex hull of $A$. For $p\in A$, the pinned
multiplicity at radius $r>0$ counts points $q\in A$ with
$\lVert p-q\rVert=r$. Problem 97 asks for a point where no radius has four
such other points. Problem 96 counts unordered pairs at distance $1$, then
takes the supremum over convex-independent $n$-point sets.
The historical progression is part of the setting. Erdős’s 1946 paper posed an
earlier three-neighbor version. His 1987 account reports Danzer’s convex
nonagon in which every vertex has three equidistant witnesses, and asks about
four witnesses. Fishburn and Reeds’s 1992 work gives a 20-vertex convex
configuration with the same unit distance at every vertex, placing the local
question beside the unit-distance problem.
# Target
The Problem 97 target is the canonical statement that every nonempty finite
convex-independent $A$ has no four-equidistant-point property:
$$
\forall A,\quad A\ne\varnothing\;\to\;\operatorname{ConvexIndep}(A)
\;\to\;\neg\operatorname{HasNEquidistantProperty}(4,A).
$$
The Problem 96 target is the canonical asymptotic statement
$$
U_c(n)=O(n),
$$
where $U_c(n)$ is the supremum of the unordered unit-distance counts
determined by convex-independent $n$-point sets. The bound is asymptotic;
the Problem 97 route would give the stronger explicit bound $U_c(n)\le3n$
for every natural number $n$.
# Significance
The package records a formal proof route joining a pinned geometric obstruction
to a global extremal bound. A successful Problem 97 proof would immediately
settle Problem 96 with the explicit constant $3$, while preserving the
combinatorial meaning of the count. It also separates the historical
three-neighbor constructions from the still-open four-neighbor assertion.
# Difficulty
The source proof reduces Problem 97 to strong induction on $|A|$. Its counting
engine follows Dumitrescu's 2006 isosceles-count method, with the cap-witness
refinements used in the source attributed to Nivasch--Pach--Pinchasi--Zerbib
(2013). This engine forces every counterexample to have at least nine points; a
finite geometric analysis excludes exactly nine points; and the remaining step must
produce a removable vertex for every larger minimal counterexample. The
removable-vertex statement carries the induction hypothesis that every
strictly smaller nonempty convex 4-equidistant set is contradictory. That
large-cardinality geometric step remains open, so both headline targets remain
open. Finite computational certificates can support local cases but do not
replace the universal geometric statement.
# Counterexample routes
Problem 97 is open, so the mission also records the parallel negative route.
The source formalization calls a nonempty convex-independent
finite set with the four-equidistant property a
[`Problem97.IsCounterexample`](https://github.com/mysticflounder/erdos-97-96-formalization/blob/a46894f6078319d3001d06310531df50af0f6bbd/lean/Erdos9796Proof/P97/UniversalProblem97.lean#L24-L29).
Constructing one such set would refute Problem 97 and therefore refute the
mission's affirmative conjunction, regardless of whether Problem 96 remains
true. The counterexample milestone keeps this resolution path visible beside
the nonexistence proof. A successful witness must use exact coordinates or
exact algebraic data from which Lean verifies both strict convex position and
the four-equidistant property; a numerical approximation or a realizable
incidence pattern alone is insufficient.
Problem 96 has its own negative route. Because its claim is asymptotic, one
finite convex configuration cannot refute it. A counterexample must instead
give convex-independent point sets at arbitrarily large cardinalities whose
unit-distance counts exceed every proposed linear constant. The mission tracks
this superlinear-family statement separately, together with a reduction from
it to the exact negation of Problem 96. This keeps both possible outcomes
visible: a direct or Problem-97-derived linear upper bound, and an explicit
family proving that no such bound exists.
# Formalization scope
The canonical source is pinned at commit
`757d852766f377f7c1a0ffeeef6d3526bc0cb7a4`. It contains the formal source
statements for [Problem 97](https://github.com/mysticflounder/erdos-97-96-formalization/blob/757d852766f377f7c1a0ffeeef6d3526bc0cb7a4/lean/Erdos9796Proof/P97/UpstreamBridge.lean#L30)
and [Problem 96](https://github.com/mysticflounder/erdos-97-96-formalization/blob/757d852766f377f7c1a0ffeeef6d3526bc0cb7a4/lean/Erdos9796Proof/P96/UpstreamBridge.lean#L96).
The source repository reports closed proofs of the conditional bridge to the $3n$ bound
([conditional three-times bound](https://github.com/mysticflounder/erdos-97-96-formalization/blob/757d852766f377f7c1a0ffeeef6d3526bc0cb7a4/lean/Erdos9796Proof/P96/EuclideanPeeling.lean#L273)),
the $|A|\ge9$ counting milestone
([nine-point counting bound](https://github.com/mysticflounder/erdos-97-96-formalization/blob/757d852766f377f7c1a0ffeeef6d3526bc0cb7a4/lean/Erdos9796Proof/P97/Counting.lean#L95)),
and the exact nine-point exclusion
([exact nine-point exclusion theorem](https://github.com/mysticflounder/erdos-97-96-formalization/blob/757d852766f377f7c1a0ffeeef6d3526bc0cb7a4/lean/Erdos9796Proof/P97/N9Endpoint/Closure.lean#L56)).
The remaining large-cardinality milestone is the
[removable-vertex step](https://github.com/mysticflounder/erdos-97-96-formalization/blob/757d852766f377f7c1a0ffeeef6d3526bc0cb7a4/lean/Erdos9796Proof/P97/RemovableVertexAxiom/RemovableVertexOfLarge.lean#L50),
with its minimality hypothesis retained. The current platform mission contains
accepted transfers of the counting argument, the conditional bridge, and the
exact nine-point exclusion, while the removable-vertex step remains open. Its definitions make
convex independence and the positive-radius condition explicit; no theorem is
assumed inside a definition. Singletons and two-point sets are included in
Problem 97, while Problem 96's counting definitions also include the empty set.
The source repository uses Lean `v4.27.0`; these mission statements target the
platform's `v4.33.1`. Source-proof transfer and revalidation remain separate work.
The Lean declarations and proofs are this project's own formalization. The
Dumitrescu and Nivasch--Pach--Pinchasi--Zerbib citations record mathematical
provenance; they do not indicate that a paper proof was imported or
machine-checked directly.
These source results establish the intended dependency graph: the P97 universal
root feeds low-unit-degree extraction, strong induction, and then the P96
supremum bound. The platform mission records those contracts and milestones;
it does not claim to have transplanted their proof bodies.
The milestones include the two canonical roots, their conditional bridge, the
`|A| ≥ 9` count, the `n = 9` exclusion, the `|A| > 9` removable-vertex step,
the documented Danzer nine-point three-neighbor example, the parallel goal of
constructing a Problem 97 counterexample, and the superlinear-family route to
a counterexample to Problem 96.
# References
- Erdős, *On Sets of Distances of n Points* (1946), [DOI](https://doi.org/10.1080/00029890.1946.11991674).
- Erdős, *Some Combinatorial and Metric Problems in Geometry* (1987), [scan](https://www.renyi.hu/~p_erdos/1987-27.pdf).
- Fishburn–Reeds, *Unit Distances Between Vertices of a Convex Polygon* (1992), [publisher record](https://www.sciencedirect.com/science/article/pii/092577219290026O).
- Dumitrescu, *On Distinct Distances from a Vertex of a Convex Polygon* (2006), [Springer record](https://link.springer.com/article/10.1007/s00454-006-1262-y); provenance for the source counting method.
- Nivasch–Pach–Pinchasi–Zerbib, *The Number of Distinct Distances from a Vertex of a Convex Polygon* (2013), [arXiv:1207.1266](https://arxiv.org/abs/1207.1266); provenance for the cap-witness refinements used by the source formalization.