Degree bound $(d_1+d_2)^2$ on the coefficient resultant

Proved

PachDeZeeuw.Algebraic.degreeOf_resultant_le

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

bezoutdegree-boundspach-de-zeeuw-bezoutresultants

Let $p$ and $q$ be bivariate real polynomials of total degrees bounded by $d_1$ and $d_2$ respectively ( $p.\mathrm{totalDegree} \le d_1$ , $q.\mathrm{totalDegree} \le d_2$ ). Then the coefficient-degree of their coefficient resultant satisfies

\mathrm{degreeOf}_0(\mathrm{ResultantCoeff}(p, q)) \le (d_1 + d_2)^2.

Here $\mathrm{ResultantCoeff}(p,q)$ is the resultant of the curried polynomials over the coefficient ring. Bounding its degree bounds the number of its roots, hence the number of bad fibers over which the two specializations can share a root; this is the quantitative heart of the resultant-based intersection bound.

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.degreeOf_resultant_le (p q : MvPolynomial (Fin 2) ℝ)
    {d₁ d₂ : ℕ}
    (hpdeg : p.totalDegree ≤ d₁)
    (hqdeg : q.totalDegree ≤ d₂) :
    MvPolynomial.degreeOf (0 : Fin 1) (ResultantCoeff p q) ≤ (d₁ + d₂) ^ 2 := 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#L127-L206

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

Degree bound (d1+d2)2(d_1+d_2)^2(d1​+d2​)2 on the coefficient resultant

Degree bound $(d_1+d_2)^2$ on the coefficient resultant