Round weighted exponents within the margin

Proved

OAI.PiExponent.FormalInterpolation.rounding_exponents_with_margin

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

algebraic-geometrynumber-theoryopenai-pi-exponent-017

Round each positive weighted threshold upward to a natural exponent. The strict margin ensures that the rounded weighted exponent remains within the upper bound.

Preamble

import Definitions.Def_OAI_PiExponent_WeightedIdealCurveCriterion

open scoped BigOperators
open OAI.PiExponent.FormalInterpolation

Formal statement

theorem OAI.PiExponent.FormalInterpolation.rounding_exponents_with_margin
    {d : Nat} (w : Fin d → Rat) (hw : ∀ i, 0 < (w i : Real))
    (c a : Rat) (hc : 0 < c) (hca : c < a)
    (k : Nat) (hk : 0 < k)
    (hmargin : ∀ i, (k : Real) * ((a - c : Rat) : Real) > (w i : Real)) :
    ∃ b : Fin d → Nat,
      (∀ i, 0 < b i) ∧
      (∀ i, (k : Real) * (c : Real) < (w i : Real) * (b i : Real)) ∧
      (∀ i, (w i : Real) * (b i : Real) ≤ (k : Real) * (a : 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