Vertical-line factor from a vanishing specialization

Proved

PachDeZeeuw.Algebraic.coeffLineFactor_dvd_of_specialized_zero

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

divisibilitypach-de-zeeuw-bezoutplane-curvesspecialization

Let $p$ be a bivariate real polynomial and $x \in \mathbb{R}$ a real number such that the specialization of $p$ at $x$ vanishes identically, $\mathrm{Specialized}_0(x, p) = 0$ . Then the vertical-line polynomial divides $p$ :

\mathrm{CoeffLineFactor}(x) \mid p, \quad \text{i.e. } (X_1 - x) \mid p.

This is the key algebraic step linking a degenerate fiber (specialization identically zero) to a geometric vertical-line component, used to show that nonvertical curves have only finitely many bad fibers.

Preamble

import Mathlib
import Definitions.Def_PdzPrelim

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

Formal statement

theorem PachDeZeeuw.Algebraic.coeffLineFactor_dvd_of_specialized_zero (p : MvPolynomial (Fin 2) ℝ) (x : ℝ)
    (hx : Specialized0 x p = 0) :
    CoeffLineFactor x ∣ p := 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/AlgebraicPrelim.lean#L626-L700

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