Discrete Geometry

Hardness of the closest vector problem, from the OpenAI Ten Proofs formalization. The source already contains machine-checked proofs; this mission organizes its headline result and additional Comparator targets for reuse.

For every Boolean language $A$ of finite bit strings for which there exist a polynomial $P\in\mathbb N[X]$ and a deterministic polynomial-time Boolean verifier $V$ satisfying $A(x)=\mathrm{true}$ if and only if there is a bit-string certificate $c$ with $|c|\le P(|x|)$ and $V(x,c)=\mathrm{true}$, there exists a total deterministic polynomial-time map $f$ on bit strings sending every $x$ with $A(x)=\mathrm{true}$ into the following YES set and every $x$ with $A(x)=\mathrm{false}$ into the following NO set. An instance consists of a natural dimension $n>0$, an integer matrix $B\in\mathbb Z^{n\times n}$ with $\det B\ne0$, a target $t\in\mathbb Q^n$ all of whose coordinates are integers, and a rational radius $r>0$. It is in YES exactly when some $z\in\mathbb Z^n$ satisfies $\sum_{i=0}^{n-1}((Bz)_i-t_i)^2\le r^2$, and in NO exactly when every $z\in\mathbb Z^n$ satisfies $(n^{1/400}r)^2<\sum_{i=0}^{n-1}((Bz)_i-t_i)^2$. The sets consist of the exact encoded instance strings, formed by concatenating the encodings of $n$, $r$, the target coordinates in order, and the matrix entries in row-major order. Each scalar is encoded by taking its library natural-number code, applying the library's natural-number-to-bit-string encoding to get a word $w$, and prefixing $w$ with $|w|$ true bits followed by one false bit. Strings without such a valid encoded instance, and instances satisfying neither distance condition, are outside both sets; dimension one is included. Polynomial time is witnessed in the library's TM2 machine model, using its product encoding of Boolean lists for verifier input, its Boolean output encoding for the verifier, and identity encodings for the reduction's input and output.

Additional targets:

• NP-hardness of binary nearest codeword with gap n^(1/200).
• NP-hardness of feasible binary syndrome decoding with gap n^(1/200).
• NP-hardness of rational finite-p lattice distance with gap n^(1/(200p)).

The formalization uses Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Its goal and milestone statements retain the validated source statements and their conventions.

Sources: Lean formalization, H_GapCVP.json.

Planned collection: OAI Ten Proofs (oai-ten-proofs).

High-dimensional sphere packing, from the OpenAI Ten Proofs formalization. The source already contains machine-checked proofs; this mission organizes its headline result and additional Comparator targets for reuse.

For each natural number $d$, let $\mathcal F_d$ consist of complex-valued Schwartz functions on Euclidean $\mathbb R^d$ whose values and Fourier-transform values are real, with $\widehat f(\xi)\geq0$ for every $\xi$, $\widehat f(0)>0$, and $f(x)\leq0$ whenever $\|x\|\geq1$; radiality is not required. Put $q(f)=f(0)/\widehat f(0)$, $V_d=\pi^{d/2}/\Gamma(d/2+1)$, and $L_d=(V_d/2^d)\inf_{f\in\mathcal F_d}q(f)$, where the infimum is taken in $\mathbb R$. Put $A_d=\inf_{f\in\mathcal F_d}q(f)^{1/d}$, $B=\sqrt{e/(2\pi)}$, and $c=\tfrac12\log_2(2\pi/e)$. The assertion is the conjunction of the following ten claims: $A_d/\sqrt d\to1/\pi$; there exists a real sequence $u_d\to0$ such that $A_d=(1/\pi+u_d)\sqrt d$ for every $d>0$; $L_d^{1/d}\to B$; $(\log L_d)/d\to\tfrac12\log(e/(2\pi))$; there exists a real sequence $v_d\to0$ such that $L_d=(B+v_d)^d$ for all sufficiently large $d$; there exists a real sequence $\delta_d\to0$, nonnegative for every natural $d$, such that for all sufficiently large $d$ and every $f\in\mathcal F_d$, $(2^d/V_d)(B-\delta_d)^d\leq q(f)$; $c>0$; $0.604400544291677695341677307053<c<0.604400544291677695341677307054$; $(\log_2 L_d)/d\to-c$; and there exists a real sequence $w_d\to0$ such that $L_d=2^{-(c+w_d)d}$ for all sufficiently large $d$. Each limit is along natural dimensions tending to infinity, and the four existentially quantified error sequences need not coincide. The sequences are defined also at $d=0$ using total real operations, in particular $0^{-1}=0$ and division by zero equal to zero; the displayed $1/d$ powers denote those real powers.

Additional targets:

• Exact root limit of the full Cohn–Elkies program.
• Exact binary logarithmic rate of the full Cohn–Elkies program.
• Sphere-packing density bound with a vanishing root error.

The formalization uses Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Its goal and milestone statements retain the validated source statements and their conventions.

Sources: Lean formalization, A_SpherePacking.json.

Planned collection: OAI Ten Proofs (oai-ten-proofs).

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.

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, 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, modules PachDeZeeuw.AlgebraicPrelim and PachDeZeeuw.Bezout (mathlib-only, axiom-clean).