$\operatorname{ProjectionGeneric}$ projections are injective on $G$

Proved

NearEnemy.injOn_of_projectionGeneric

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

general-positiongeneric-projectioninjectivitynear-enemy

Let $T$ be a real-linear map from EuclideanSpace ℝ ι to the plane (EuclideanSpace ℝ (Fin 2)) that is ProjectionGeneric T G for a finite set $G$ (i.e. $T$ avoids all finitely many degeneracy polynomials: no collapsed pairs, no new collinearities, no new cosphericalities, separated distances). Then $T$ is injective on $G$ :

\operatorname{Set.InjOn}(T,\, G).

Injectivity on the source set is the most basic consequence of genericity: distinct source points must remain distinct after projection, and is invoked every time cardinalities of images are identified with cardinalities of $G$ (e.g. in the energy computation $2|G|(|G|-1)$ ).

Preamble

import Mathlib
import Definitions.Def_NearEnemyDefs

universe u_1
open scoped RealInnerProductSpace
open scoped Classical
open MvPolynomial
variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V]
variable {ι : Type*} [Fintype ι]
open NearEnemy

Formal statement

theorem NearEnemy.injOn_of_projectionGeneric {T : EuclideanSpace ℝ ι →ₗ[ℝ] EuclideanSpace ℝ (Fin 2)} {G : Finset (EuclideanSpace ℝ ι)} (hT : ProjectionGeneric T G) :
    Set.InjOn (fun x ↦ T x) ↑G := by sorry

Source

Prior art: Lund-Sheffer-de Zeeuw, Bisector energy and few distinct distances, SoCG 2015, LIPIcs vol. 34, 537-552, DOI 10.4230/LIPIcs.SOCG.2015.537, footnote 1 on p. 538, state that E(P) = 2n(n-1) when every pair of distinct points has a distinct perpendicular bisector, with the count of trivial quadruples that proves the floor (this footnote is not in arXiv:1411.6868v1); the asymptotic floor E(P) = Omega(n^2) is in their section 3.4. The generic planar projection that is injective, keeps general position and transports distances is Erdos-Furedi-Pach-Ruzsa, The grid revisited, Discrete Math. 111 (1993), proof of Theorem 3.1. Formalized in https://github.com/mysticflounder/lean-formalizations/blob/dd46c17a2a034d7bfa0df02e7f77834d35592864/lean/LeanFormalizations/Geometry/Euclidean/NearEnemyTheorem.lean#L899-L904

View graph

ProjectionGeneric⁡\operatorname{ProjectionGeneric}ProjectionGeneric projections are injective on GGG

$\operatorname{ProjectionGeneric}$ projections are injective on $G$