Bivariate evaluation as specialized univariate evaluation

Proved

PachDeZeeuw.Algebraic.eval_eq_specialized_eval

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

evaluationpach-de-zeeuw-bezoutplane-curvesspecialization

Let $p$ be a bivariate real polynomial and $z$ a point of the plane ( $\mathrm{Point2}$ ). Then evaluating $p$ at $z$ equals evaluating the specialized univariate polynomial at the eliminated coordinate:

p(z) = \mathrm{eval}(\mathrm{elimCoord}(z),\, \mathrm{Specialized}_0(\mathrm{coeffCoord}(z), p)).

In coordinates $z = (y, x)$ , this says $p(y,x)$ is obtained by first specializing the coefficient variable to $x$ and then evaluating at $y$ . This fiber-decomposition identity is the workhorse connecting plane zero sets to univariate fibers, used in every fiber-counting argument.

Preamble

import Mathlib
import Definitions.Def_PdzPrelim

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

Formal statement

theorem PachDeZeeuw.Algebraic.eval_eq_specialized_eval (p : MvPolynomial (Fin 2) ℝ) (z : Point2) :
    MvPolynomial.eval (fun i => z i) p =
      Polynomial.eval (elimCoord z) (Specialized0 (coeffCoord z) p) := by sorry

Source

Lean bridge lemma (definitional unfolding or coordinate bookkeeping) for the formalization of Pach–de Zeeuw, arXiv:1308.0177, Theorem 2.1; not a literature statement; formalized in https://github.com/mysticflounder/lean-formalizations/blob/dd46c17a2a034d7bfa0df02e7f77834d35592864/lean/LeanFormalizations/PachDeZeeuw/AlgebraicPrelim.lean#L283-L301

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