Number of normalized factors bounded by total degree

Proved

PachDeZeeuw.Algebraic.card_normalizedFactors_le_totalDegree

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

degree-boundsfactorizationpach-de-zeeuw-bezoutplane-curves

Let $p$ be a nonzero bivariate real polynomial ( $p \ne 0$ in $\mathrm{MvPolynomial}(\mathrm{Fin}\,2, \mathbb{R})$ ). Then the number of factors in its normalized factorization is bounded by its total degree:

|\mathrm{normalizedFactors}(p)| \le \mathrm{totalDegree}(p).

This factor-counting estimate is the bookkeeping input to the factorized B\u00e9zout bound: it controls how many irreducible-pair intersections must be union-bounded when both curves are split into factors.

Preamble

import Mathlib
import Definitions.Def_PdzPrelim

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

Formal statement

theorem PachDeZeeuw.Algebraic.card_normalizedFactors_le_totalDegree {p : MvPolynomial (Fin 2) ℝ} (hp0 : p ≠ 0) :
    (UniqueFactorizationMonoid.normalizedFactors p).card ≤ p.totalDegree := 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#L1475-L1496

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