Bounded representatives yield a family of monic relations

Proved

OAI.PiExponent.FormalInterpolation.bounded_representatives_to_monic_relations

by Eyal1990 · Oct 20, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-geometrynumber-theoryopenai-pi-exponent-017

For a family of exponents whose weighted degrees strictly exceed k c, bounded representatives modulo I^k give a family of ideal elements with the required strict support bounds.

Preamble

import Definitions.Def_OAI_PiExponent_WeightedIdealCurveCriterion

open scoped BigOperators
open OAI.PiExponent.FormalInterpolation

Formal statement

theorem OAI.PiExponent.FormalInterpolation.bounded_representatives_to_monic_relations
    {d : Nat} (I : Ideal (MvPolynomial (Fin d) Complex))
    (w : Fin d → Rat) (c : Rat) (k : Nat)
    (hrep : ∀ P : MvPolynomial (Fin d) Complex,
      ∃ R : MvPolynomial (Fin d) Complex,
        P - R ∈ I ^ k ∧
        ∀ v ∈ R.support,
          (∑ j, (w j : Real) * (v j : Real)) ≤ (k : Real) * (c : Real))
    (b : Fin d → Nat)
    (hlower : ∀ i, (k : Real) * (c : Real) < (w i : Real) * (b i : Real)) :
    ∃ F : Fin d → MvPolynomial (Fin d) Complex,
      (∀ i, F i ∈ I ^ k) ∧
      (∀ i, ∀ v ∈ (MvPolynomial.X i ^ b i - F i).support,
        (∑ j, (w j : Real) * (v j : Real)) < (w i : Real) * (b i : Real)) := by sorry

Source

Reduction obligation for OAI.PiExponent.FormalInterpolation.weightedIdealCurveBound_eventual_quotient_representatives (globalInterpolation pillar; weighted compactification / ampleness / Serre vanishing / ordinary Rees recovery argument), split at the interface between the geometric weighted-monic-relations output of the curve criterion and the algebraic weighted division step. (geometric step: curve criterion -> weighted monic relations)

View graph