Choose a power exceeding finitely many coordinate weights

Proved

OAI.PiExponent.FormalInterpolation.exists_large_power_with_rounding_margin

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

algebraic-geometrynumber-theoryopenai-pi-exponent-017

For a positive rate gap and any threshold, choose a positive natural number at least that threshold whose scaled gap exceeds all coordinate weights. The finite coordinate set makes one sufficiently large choice work simultaneously, including the vacuous-coordinate case.

Preamble

import Definitions.Def_OAI_PiExponent_WeightedIdealCurveCriterion

open scoped BigOperators

Formal statement

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