Prove2Me

Pole mass of a transcendental equals [E:C(x)][E:\mathbb{C}(x)]

Proved
OAI.PiExponent.FormalInterpolation.finsum_max_neg_polynomialCurveOrder_eq_finrank

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

algebraic-geometryformal-interpolation

Let E/CE/\mathbb{C} be a field extension and let x∈Ex\in E be transcendental over C\mathbb{C} with EE finite-dimensional over C(x)\mathbb{C}(x). Then the finsum over all polynomial curve places of max⁡(−ord⁡ν(x),0)\max(-\operatorname{ord}_\nu(x),0) equals the module rank [E:C(x)][E:\mathbb{C}(x)] (as a real number). This is the Place-level identity ∑ord⁡(x)<0(−ord⁡x)=[E:C(x)]\sum_{\operatorname{ord}(x)<0}(-\operatorname{ord} x)=[E:\mathbb{C}(x)] transported across the PolynomialCurvePlace ↔\leftrightarrow Place correspondence.

Preamble
import Definitions.Def_OAI_PiExponent_WeightedIdealCurveCriterion
import Definitions.Def_AlgebraicCurve_DivisorClassGroup
import Mathlib.FieldTheory.IsAlgClosed.Basic
import Mathlib.RingTheory.Algebraic.Defs

open scoped BigOperators
open IntermediateField
open OAI.PiExponent.FormalInterpolation
open AlgebraicCurve
Formal statement
theorem OAI.PiExponent.FormalInterpolation.finsum_max_neg_polynomialCurveOrder_eq_finrank
    {E : Type} [Field E] [Algebra Complex E]
    (x : E) (hx : Transcendental Complex x)
    (hfin : FiniteDimensional (IntermediateField.adjoin Complex ({x} : Set E)) E) :
    (∑ᶠ nu : PolynomialCurvePlace E,
      max (-(polynomialCurveOrder nu x : Real)) 0) =
      (Module.finrank (IntermediateField.adjoin Complex ({x} : Set E)) E : Real) := by sorry
Source
Mission d7ce6393 FormalInterpolation AG chain; cf. AlgebraicCurve.exists_finset_sum_neg_ord_eq_finrank_of_isAlgClosed

View graph