Finite singularity bound for an irreducible plane curve

Proved

PachDeZeeuw.Algebraic.finite_singularities_of_irreducible_bound

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

intersection-boundspach-de-zeeuw-bezoutplane-curvessingularities

Let $h$ be an irreducible plane polynomial of total degree at most $d$ with a nonzero partial derivative $\mathrm{pderiv}_i(h) \ne 0$ . Then its singular locus (common zeros of $h$ and both partials) is finite with an explicit bound:

|\mathrm{SingularPointSet}(h)| \le (d+1)^5.

The proof covers the singular set by intersections of $h$ with factors of the nonzero partial and applies the factor-intersection bound. Finiteness of singularities is needed in the Pach--de Zeeuw incidence argument to discard a controlled bad set and work on the smooth part of the curve.

Preamble

import Mathlib
import Definitions.Def_PdzBezout
import Definitions.Def_PdzPrelim

open EuclideanGeometry
open scoped Topology
open PachDeZeeuw.Algebraic
open PachDeZeeuw.Algebraic.PlaneCurve

Formal statement

theorem PachDeZeeuw.Algebraic.finite_singularities_of_irreducible_bound {d : ℕ} (h : PlanePoly)
    (hh : Irreducible h)
    (hdeg : h.totalDegree ≤ d)
    {i : Fin 2}
    (hpi : MvPolynomial.pderiv i h ≠ 0) :
    (SingularPointSet h).Finite ∧
      (SingularPointSet h).ncard ≤ (d + 1) ^ 5 := by sorry

Source

Standard algebra used in proving Bézout's inequality, Theorem 2.1 of Pach–de Zeeuw, Distinct distances on algebraic curves in the plane (arXiv:1308.0177), which cites Gibson, Elementary Geometry of Algebraic Curves, Lemma 14.4; this lemma is not stated in the paper; formalized in https://github.com/mysticflounder/lean-formalizations/blob/dd46c17a2a034d7bfa0df02e7f77834d35592864/lean/LeanFormalizations/PachDeZeeuw/Bezout.lean#L1090-L1159

Human review

Endorsed by Shuze Chen · Sep 17, 2026
Endorsed by mysticflounder · Sep 17, 2026
Confirmed by the mission captain (proposal self-audit).

View graph