The old high-order MVI lower-bound exponent is larger than $T^{-p}$

Proved

RybinAI2026.P03.old_lower_exponent_refuted

by wenxinzhang · Aug 31, 2026 · Mathlib c5ea003 (Lean v4.30.0)

optimizationoracle-complexityvariational-inequalities

For every integer oracle order $p\ge2$ and iteration count $T\ge2$ , the reciprocal $p$ th-power rate is strictly smaller than the formerly proposed reciprocal $(p+1)/2$ -power rate:

(T^{-1})^p < (T^{-1})^{(p+1)/2}.

This is the elementary exponent comparison used when relating the 2026 $T^{-p}$ upper rate to the old conjectured exponent.

Preamble

import Mathlib

Formal statement

namespace RybinAI2026.P03

/-- For every oracle order `p ≥ 2` and iteration count `T ≥ 2`, the reciprocal `p`th-power
rate is strictly smaller than the formerly conjectured reciprocal `(p+1)/2`-power rate.  This
is the elementary exponent comparison behind the 2026 upper-bound refutation. -/
theorem old_lower_exponent_refuted
    (p T : ℕ) (hp : 2 ≤ p) (hT : 2 ≤ T) :
    ((T : ℝ)⁻¹) ^ (p : ℝ) <
      ((T : ℝ)⁻¹) ^ (((p : ℝ) + 1) / 2) := by
  sorry

end RybinAI2026.P03

Source

CUHK-Shenzhen AI Math Problem 3, https://rybindmitry.github.io/problems/3.html; the

T^{-p}

upper bound is from Chen--Zhang--Wang--Liu--Chen--Zhang, https://arxiv.org/abs/2608.08463 (2026). This node formalizes only the exact elementary exponent comparison.

View graph

The old high-order MVI lower-bound exponent is larger than T−pT^{-p}T−p

The old high-order MVI lower-bound exponent is larger than $T^{-p}$