OAI.Heisenberg.dynamics_converges: intermediate lemma from OpenAI, Spontaneous magnetization in the quantum Heisenberg ferromagnet

Proved

OAI.Heisenberg.dynamics_converges

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

openai-math

An intermediate lemma of the split of OpenAI's proof of OAI.Heisenberg.spontaneous_magnetization, carved from OpenAI's openai/math development for this platform. The statement and its proof are OpenAI's (OpenAI, Spontaneous magnetization in the quantum Heisenberg ferromagnet, OpenAI Math Release, September 24, 2026, result family 271, github.com/openai/math, Apache License 2.0); in Lean it is the declaration OAI.Heisenberg.dynamics_converges of lean/OAI/MathematicalPhysics/Heisenberg/ThermodynamicDynamics.lean at commit adc7f12, ported to Lean 4.33.1 and Mathlib 0df444a.

The statement, as published (namespace OAI.Heisenberg, with open scoped ComplexConjugate ENNReal Classical, open scoped ComplexConjugate BigOperators):

theorem dynamics_converges (d ℓ : ℕ) : DynamicsConverges d ℓ

Definitions. The statement is written with OAI.Heisenberg.DynamicsConverges (the published bundle Def_Heisenberg).

Used by. The proofs of OAI.Heisenberg.cubeBoundary_error, OAI.Heisenberg.finiteDynamics_deep_uniform, OAI.Heisenberg.spontaneous_magnetization and OAI.Heisenberg.state_limit_locallyUniform of this split import it.

Preamble

import Mathlib
import Definitions.Def_Heisenberg

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

noncomputable section
open scoped ComplexConjugate ENNReal Classical
open scoped ComplexConjugate BigOperators

namespace Heisenberg

theorem dynamics_converges (d ℓ : ℕ) : DynamicsConverges d ℓ := by
  sorry

end Heisenberg

open Filter Topology Metric
open scoped NNReal

open scoped NNReal
end

end OAI
end

Source

OpenAI, Spontaneous magnetization in the quantum Heisenberg ferromagnet, OpenAI Math Release, September 24, 2026, https://github.com/openai/math (result family 271; paper: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Spontaneous-magnetization-in-the-quantum-Heisenberg-ferromagnet-September-24-2026/paper.pdf; Apache License 2.0); Lean: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/MathematicalPhysics/Heisenberg/ThermodynamicDynamics.lean (declaration OAI.Heisenberg.dynamics_converges)

View graph