OAI.ThreeTorus.StageState.exists_step: intermediate lemma from OpenAI, A smooth three-torus diffeomorphism with simple Lebesgue spectrum

Proved

OAI.ThreeTorus.StageState.exists_step

by dbenbenn · Oct 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

openai-math

An intermediate lemma of the split of OpenAI's proof of OAI.ThreeTorus.simple_lebesgue_spectrum, carved from OpenAI's openai/math development for this platform. The statement and its proof are OpenAI's (OpenAI, A smooth three-torus diffeomorphism with simple Lebesgue spectrum, OpenAI Math Release, September 23, 2026, result family 144, github.com/openai/math, Apache License 2.0); in Lean it is the declaration OAI.ThreeTorus.StageState.exists_step of lean/OAI/Dynamics/ThreeTorus/ThreeTorus/Stages.lean at commit adc7f12, ported to Lean 4.33.1 and Mathlib 0df444a.

The statement, as published (namespace OAI.ThreeTorus.StageState, with open Set Function Filter MeasureTheory, open scoped Topology BigOperators ComplexConjugate):

theorem exists_step (s : StageState) (h : PhysicalTest) (Q : PhysicalJetData)
    {ε η κ ζ : ℝ} (hε : 0 < ε) (hη : 0 < η) (hκ : 0 < κ) (hζ : 0 < ζ) :
    ∃ t : StageState, ∃ c : ℤ →₀ ℂ,
      t.δ < κ ∧ Q.Close ζ s.frame s.V t.frame t.V ∧
      dist s.vec t.vec < ε ∧ dist h.vec (t.laurent c) < Real.sqrt (2*s.δ)+η

Definitions. The statement is written with OAI.ThreeTorus.PhysicalJetData, OAI.ThreeTorus.PhysicalTest, OAI.ThreeTorus.StageState, OAI.ThreeTorus.TripleTorus, OAI.ThreeTorus.tripleVolume, OAI.ThreeTorus.PhysicalJetData.Close, OAI.ThreeTorus.PhysicalTest.vec, OAI.ThreeTorus.StageState.L2, OAI.ThreeTorus.StageState.laurent and OAI.ThreeTorus.StageState.vec (definitions bundle OAIQ13Tt000 of this split).

Used by. The proof of OAI.ThreeTorus.exists_physical_basis of this split imports it.

Preamble

import Mathlib
import Definitions.Def_OAIQ13Tt000

Formal statement

section

attribute [-instance] _root_.OAI.ThreeTorus.PhysicalTest.instNonempty _root_.OAI.ThreeTorus.PhysicalTest.instSecondCountableTopology _root_.OAI.ThreeTorus.PhysicalTest.instTopologicalSpace _root_.OAI.ThreeTorus.StageState.instTopologicalSpace _root_.OAI.ThreeTorus.tripleVolume_regular
set_option linter.all false
set_option linter.unusedVariables false
set_option linter.unusedTactic false
set_option linter.unreachableTactic false

namespace OAI

section

noncomputable section
open Set Function Filter MeasureTheory
open scoped Topology BigOperators ComplexConjugate
namespace ThreeTorus

namespace StageState
theorem exists_step (s : StageState) (h : PhysicalTest) (Q : PhysicalJetData)
    {ε η κ ζ : ℝ} (hε : 0 < ε) (hη : 0 < η) (hκ : 0 < κ) (hζ : 0 < ζ) :
    ∃ t : StageState, ∃ c : ℤ →₀ ℂ,
      t.δ < κ ∧ Q.Close ζ s.frame s.V t.frame t.V ∧
      dist s.vec t.vec < ε ∧ dist h.vec (t.laurent c) < Real.sqrt (2*s.δ)+η := by
  sorry

end StageState
end ThreeTorus
end
end

end OAI
end

Source

OpenAI, A smooth three-torus diffeomorphism with simple Lebesgue spectrum, OpenAI Math Release, September 23, 2026, https://github.com/openai/math (result family 144; paper: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-smooth-three-torus-diffeomorphism-with-simple-Lebesgue-spectrum-September-23-2026/paper.pdf; Apache License 2.0); Lean: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Dynamics/ThreeTorus/ThreeTorus/Stages.lean (declaration OAI.ThreeTorus.StageState.exists_step)

View graph