Every normalized factor of $p$ is irreducible

Proved

PachDeZeeuw.Algebraic.normalized_factor_irreducible

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

factorizationpach-de-zeeuw-bezoutunique-factorization

Let $p$ and $h$ be bivariate real polynomials and let $h_h$ witness that $h$ belongs to the multiset $\mathrm{normalizedFactors}\,p$ of normalized prime factors of $p$ . Then $h$ is irreducible:

{\mathrm{Irreducible}\,h.}

This packages the unique-factorization-domain fact that normalized factors are (prime, hence) irreducible elements, licensing the application of all irreducible-case lemmas --- fiber bounds, pair-intersection bounds, nonzero-partial results --- to each factor when decomposing a reducible curve for 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.normalized_factor_irreducible {p h : MvPolynomial (Fin 2) ℝ}
    (hh : h ∈ UniqueFactorizationMonoid.normalizedFactors p) :
    Irreducible 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#L1413-L1418

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

Every normalized factor of ppp is irreducible

Every normalized factor of $p$ is irreducible