Prove2Me

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

Proved
OAI.PiExponent.FormalInterpolation.finsum_max_polynomialCurveOrder_eq_finrank

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

algebraic-geometryformal-interpolation

Under the same hypotheses as the pole-mass companion, the finsum of max⁡(ord⁡ν(x),0)\max(\operatorname{ord}_\nu(x),0) over polynomial curve places equals [E:C(x)][E:\mathbb{C}(x)]. Together with the pole identity this yields ∑max⁡(ord⁡,0)=∑max⁡(−ord⁡,0)\sum \max(\operatorname{ord},0)=\sum \max(-\operatorname{ord},0) for transcendental elements.

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_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_ord_sub_algebraMap_eq_finrank_of_isAlgClosed with a=0

View graph