Zero set of $p$ covered by zero sets of its normalized factors

Proved

PachDeZeeuw.Algebraic.zeroSet_subset_normalizedFactor_union

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

factorizationpach-de-zeeuw-bezoutplane-curves

Let $p$ be a nonzero bivariate real polynomial ( $h_{p0} : p \neq 0$ ). Then its plane zero set is covered by the zero sets of its normalized factors:

{\mathrm{PlaneCurveZeroSet}\,p \subseteq \bigcup_{h \in (\mathrm{normalizedFactors}\,p).\mathrm{toFinset}} \mathrm{PlaneCurveZeroSet}\,h.}

This is the geometric counterpart of unique factorization: since $p$ equals (up to a unit) the product of its normalized factors, every zero of $p$ is a zero of some factor. It is the reduction step that lifts per-irreducible-component intersection bounds to reducible curves in the factorized Bezout bound.

Preamble

import Mathlib
import Definitions.Def_PdzPrelim

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

Formal statement

theorem PachDeZeeuw.Algebraic.zeroSet_subset_normalizedFactor_union {p : MvPolynomial (Fin 2) ℝ} (hp0 : p ≠ 0) :
    PlaneCurveZeroSet p ⊆
      ⋃ h ∈ (UniqueFactorizationMonoid.normalizedFactors p).toFinset,
        PlaneCurveZeroSet h := 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#L1506-L1532

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

Zero set of ppp covered by zero sets of its normalized factors

Zero set of $p$ covered by zero sets of its normalized factors