Prove2Me

OAI.MarkovSuperreflexivity.hasEquivalentUCNorm_of_finiteTriangularObstruction: intermediate lemma from OpenAI, Nontrivial Markov Type Forces Superreflexivity

Proved
OAI.MarkovSuperreflexivity.hasEquivalentUCNorm_of_finiteTriangularObstruction

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.MarkovSuperreflexivity.hasNontrivialMarkovType_iff_hasEquivalentUCNorm, carved from OpenAI's openai/math development for this platform. The statement and its proof are OpenAI's (OpenAI, Nontrivial Markov Type Forces Superreflexivity, OpenAI Math Release, September 23, 2026, result family 327, github.com/openai/math, Apache License 2.0); in Lean it is the declaration OAI.MarkovSuperreflexivity.hasEquivalentUCNorm_of_finiteTriangularObstruction of lean/OAI/Analysis/MarkovType/MarkovType/JamesEnflo.lean at commit adc7f12, ported to Lean 4.33.1 and Mathlib 0df444a.

The statement, as published (namespace OAI.MarkovSuperreflexivity):

theorem hasEquivalentUCNorm_of_finiteTriangularObstruction
    (h : FiniteTriangularObstruction X) : HasEquivalentUCNorm X

Definitions. The statement is written with OAI.MarkovSuperreflexivity.FiniteTriangularObstruction (definitions bundle OAISMk000 of this split); OAI.MarkovSuperreflexivity.HasEquivalentUCNorm (the published bundle Def_MarkovType).

Used by. The proof of OAI.MarkovSuperreflexivity.hasNontrivialMarkovType_iff_hasEquivalentUCNorm of this split imports it.

Preamble
import Mathlib
import Lean.Elab.Tactic.Omega
import Definitions.Def_MarkovType
import Definitions.Def_OAISMk000
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

namespace MarkovSuperreflexivity

universe u v
variable {X : Type u} [NormedAddCommGroup X] [NormedSpace ℝ X]
variable {Y : Type v} [NormedAddCommGroup Y] [NormedSpace ℝ Y]

theorem hasEquivalentUCNorm_of_finiteTriangularObstruction
    (h : FiniteTriangularObstruction X) : HasEquivalentUCNorm X := by
  sorry

end MarkovSuperreflexivity

end OAI
end
Source
OpenAI, Nontrivial Markov Type Forces Superreflexivity, OpenAI Math Release, September 23, 2026, https://github.com/openai/math (result family 327; paper: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Nontrivial-Markov-Type-Forces-Superreflexivity-September-23-2026/paper.pdf; Apache License 2.0); Lean: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Analysis/MarkovType/MarkovType/JamesEnflo.lean (declaration OAI.MarkovSuperreflexivity.hasEquivalentUCNorm_of_finiteTriangularObstruction)

View graph