Constructing the window from a small rational parameter

Proved

OAI.PiExponent.window_from_small_parameter

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

Given nu>2 and a positive rational q below the stated bound, the explicit choices theta=(1−q)^2, A=1−q−((nu−2)/(8nu))q, and eta=((nu−2)/(8nu))q satisfy all window inequalities, including strict determinant slack. The q<1/4 bound keeps the parameters in range; the second bound supplies the strict slack.

Preamble

import Mathlib.Data.Real.Basic
import Mathlib.Data.Rat.Cast.Order

Formal statement

theorem OAI.PiExponent.window_from_small_parameter (nu : ℝ) (hnu : 2 < nu)
    (q : ℚ) (hqpos : 0 < (q : ℝ))
    (hqsmall : (q : ℝ) < min (1 / 4 : ℝ) (3 * (nu - 2) / (4 * (nu - 1)))) :
    ∃ (theta : ℚ) (A eta : ℝ),
      theta = (1 - q) ^ 2 ∧
      A = 1 - (q : ℝ) - ((nu - 2) / (8 * nu)) * (q : ℝ) ∧
      eta = ((nu - 2) / (8 * nu)) * (q : ℝ) ∧
      0 < theta ∧ theta < 1 ∧
      0 < A ∧ A < 1 ∧ 0 < eta ∧ eta < 1 ∧
      A ^ 2 < (theta : ℝ) ∧
      0 < nu * (A * (1 - eta) - (theta : ℝ)) -
        (1 - (theta : ℝ)) := by sorry

Source

https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/PiExponent.lean

View graph