Uniform additive constant from eventual weighted surjectivity

Proved

OAI.PiExponent.FormalInterpolation.asymptotic_representatives_of_eventual_weighted_surjectivity

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

If weighted sections of radius n(rho+eps) eventually surject onto R/I^n, then a single additive Nat constant C upgrades the bound to all n, by absorbing small n via I^N ⊆ I^n and C = ceil(N(rho+eps)).

Preamble

import Mathlib.Algebra.MvPolynomial.Basic
import Mathlib.Data.Complex.Basic
import Mathlib.RingTheory.Ideal.Operations

open scoped BigOperators

Formal statement

theorem OAI.PiExponent.FormalInterpolation.asymptotic_representatives_of_eventual_weighted_surjectivity
    {d : Nat} (I : Ideal (MvPolynomial (Fin d) Complex))
    (w : Fin d → Rat)
    (rho : Rat) (hrho : 0 ≤ rho) (eps : Real) (heps : 0 < eps)
    (heventual : ∃ N : Nat, ∀ n : Nat, N ≤ n →
      ∀ p : MvPolynomial (Fin d) Complex,
        ∃ q : MvPolynomial (Fin d) Complex,
          p - q ∈ I ^ n ∧
          ∀ a ∈ q.support,
            ∑ i, (w i : Real) * (a i : Real) ≤
              (n : Real) * ((rho : Real) + eps)) :
    ∃ C : Nat, ∀ n : Nat, ∀ p : MvPolynomial (Fin d) Complex,
        ∃ q : MvPolynomial (Fin d) Complex,
          p - q ∈ I ^ n ∧
          ∀ a ∈ q.support,
            ∑ i, (w i : Real) * (a i : Real) ≤
              (n : Real) * ((rho : Real) + eps) + (C : Real) := by sorry

Source

Elementary ideal-power absorption: for n < N use a representative modulo I^N ⊆ I^n of weight ≤ N(rho+eps), absorbed into the additive constant ceil(N(rho+eps)).

View graph