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

Proved

OAI.ThreeTorus.exists_physical_basis

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.exists_physical_basis of lean/OAI/Dynamics/ThreeTorus/ThreeTorus/PhysicalBasis.lean at commit adc7f12, ported to Lean 4.33.1 and Mathlib 0df444a.

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

theorem exists_physical_basis : ∃ D : SmoothDynamics, ∃ f : PhysicalL2,
    f ∈ physicalMeanZero ∧ (∀ᵐ x ∂tripleVolume, (f x).im=0) ∧
    Orthonormal ℂ (D.orbit f) ∧
    (Submodule.span ℂ (Set.range (D.orbit f))).topologicalClosure=physicalMeanZero

Definitions. The statement is written with OAI.ThreeTorus.PhysicalL2, OAI.ThreeTorus.SmoothDynamics, OAI.ThreeTorus.TripleTorus, OAI.ThreeTorus.physicalMeanZero, OAI.ThreeTorus.tripleVolume and OAI.ThreeTorus.SmoothDynamics.orbit (definitions bundle OAIQ13Tt000 of this split).

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

Preamble

import Mathlib
import Definitions.Def_OAIQ13Tt000

Formal statement

section

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

theorem exists_physical_basis : ∃ D : SmoothDynamics, ∃ f : PhysicalL2,
    f ∈ physicalMeanZero ∧ (∀ᵐ x ∂tripleVolume, (f x).im=0) ∧
    Orthonormal ℂ (D.orbit f) ∧
    (Submodule.span ℂ (Set.range (D.orbit f))).topologicalClosure=physicalMeanZero := by
  sorry

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/PhysicalBasis.lean (declaration OAI.ThreeTorus.exists_physical_basis)

View graph