Prove2Me

Constants have polynomial-curve order zero

Proved
OAI.PiExponent.FormalInterpolation.polynomialCurveOrder_algebraMap

by Ethan Cheung Wang · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-geometryformal-interpolation

For a nonzero complex constant bb, every polynomial curve place evaluates ord⁡ν(b‾)=0\operatorname{ord}_\nu(\overline{b})=0. Consequently the positive and pole finsums of a nonzero constant vanish.

Preamble
import Definitions.Def_OAI_PiExponent_WeightedIdealCurveCriterion

open OAI.PiExponent.FormalInterpolation
Formal statement
theorem OAI.PiExponent.FormalInterpolation.polynomialCurveOrder_algebraMap
    {E : Type} [Field E] [Algebra Complex E]
    (nu : PolynomialCurvePlace E) {b : Complex} (hb : b ≠ 0) :
    polynomialCurveOrder nu (algebraMap Complex E b) = 0 := by sorry
Source
Mission d7ce6393 FormalInterpolation AG chain; definition of PolynomialCurvePlace

View graph