Mission

Near enemies: spherical sets project to minimal-energy images in general positionOpen Problem

Algebraic Geometry Discrete Geometry·Captain: mysticflounder

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; journal version Discrete Comput. Geom. 56 (2016), no. 2, 337–356, DOI 10.1007/s00454-016-9783-5, arXiv: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, §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.
McKenna, Lean formalization (mathlib-only, axiom-clean), lean-formalizations, module Geometry.Euclidean.NearEnemyTheorem.

Goal · Spherical sets project to minimal-energy general-position images

PROVED

theorem NearEnemy.nearEnemy_sphereSlice_exists_bisectorEnergy_minimal_image_generalPosition_distanceTransport {center : EuclideanSpace ℝ ι} {R : ℝ} {G : Finset (EuclideanSpace ℝ ι)}
    (hG : ∀ x ∈ G, x ∈ Metric.sphere center R) :
    ∃ T : EuclideanSpace ℝ ι →ₗ[ℝ] EuclideanSpace ℝ (Fin 2),
      Set.InjOn (fun x ↦ T x) ↑G ∧
      bisectorEnergy (G.image fun x ↦ T x) = 2 * G.card * (G.card - 1) ∧
      (∀ P' : Finset (EuclideanSpace ℝ (Fin 2)), P'.card = G.card →
        bisectorEnergy (G.image fun x ↦ T x) ≤ bisectorEnergy P') ∧
      (∀ q₁ ∈ G.image (fun x ↦ T x), ∀ q₂ ∈ G.image (fun x ↦ T x),
        ∀ q₃ ∈ G.image (fun x ↦ T x), q₁ ≠ q₂ → q₁ ≠ q₃ → q₂ ≠ q₃ →
          ¬ Collinear ℝ ({q₁, q₂, q₃} : Set (EuclideanSpace ℝ (Fin 2)))) ∧
      (∀ q₁ ∈ G.image (fun x ↦ T x), ∀ q₂ ∈ G.image (fun x ↦ T x),
        ∀ q₃ ∈ G.image (fun x ↦ T x), ∀ q₄ ∈ G.image (fun x ↦ T x),
        q₁ ≠ q₂ → q₁ ≠ q₃ → q₁ ≠ q₄ → q₂ ≠ q₃ → q₂ ≠ q₄ → q₃ ≠ q₄ →
          ¬ EuclideanGeometry.Cospherical
            ({q₁, q₂, q₃, q₄} : Set (EuclideanSpace ℝ (Fin 2)))) ∧
      rotationEnergy (G.image fun x ↦ T x) = 0 ∧
      (∀ a ∈ G, ∀ b ∈ G, ∀ c ∈ G, ∀ e ∈ G,
        (dist (T a) (T b) = dist (T c) (T e) ↔
          (a - b = c - e ∨ a - b = -(c - e)))) ∧
      (((G.image fun x ↦ T x).offDiag).image fun q ↦ dist q.1 q.2).card =
        ((G.offDiag).image fun p ↦
          ({p.1 - p.2, p.2 - p.1} : Finset (EuclideanSpace ℝ ι))).card := by sorry

Let $G$ be a finite set in EuclideanSpace ℝ ι contained in a metric sphere of center $\mathrm{center}$ and radius $R$ (hypothesis hG: every $x \in G$ lies in Metric.sphere center R). Then there exists a real-linear map $T$ to the plane delivering the same full bundle as in the no-three-collinear case: injectivity on $G$ , $\operatorname{bisectorEnergy}(T(G)) = 2|G|(|G|-1)$ with minimality among equal-cardinality planar sets, general position of the image (no three collinear, no four cospherical), $\operatorname{rotationEnergy}(T(G)) = 0$ , exact distance transport, and the distance-class counting identity:

\exists\, T,\quad \operatorname{bisectorEnergy}(T(G)) = 2\,|G|\,(|G|-1)\ \land\ \operatorname{rotationEnergy}(T(G)) = 0\ \land\ \text{(general position + distance transport)}.

This is the spherical-source counterpart of the main bundle. Sphere membership is the only hypothesis: no general-position assumption is imposed on $G$ , because a line meets a sphere in at most two points, so a set on a sphere is automatically no-three-collinear. Every four points of $G$ are of course cospherical; it is the planar image that is shown free of cospherical quadruples. The corollary therefore extends the Near Enemy conclusion to spherical configurations at no extra cost in hypotheses.

Frontier · Open leaf nodes

Recent activity

Mission

Near enemies: spherical sets project to minimal-energy images in general position

Goal