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).