Prove2Me

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

Proved
OAI.MarkovSuperreflexivity.finiteTriangularObstruction_of_hasEquivalentUCNorm

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.finiteTriangularObstruction_of_hasEquivalentUCNorm of lean/OAI/Analysis/MarkovType/MarkovType/StructuralL2Estimates.lean at commit adc7f12, ported to Lean 4.33.1 and Mathlib 0df444a.

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

theorem finiteTriangularObstruction_of_hasEquivalentUCNorm
    (h : HasEquivalentUCNorm X) : FiniteTriangularObstruction 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.exists_power_smooth_equivalentNorm 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
variable {X : Type u} [NormedAddCommGroup X] [NormedSpace ℝ X]

theorem finiteTriangularObstruction_of_hasEquivalentUCNorm
    (h : HasEquivalentUCNorm X) : FiniteTriangularObstruction 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/StructuralL2Estimates.lean (declaration OAI.MarkovSuperreflexivity.finiteTriangularObstruction_of_hasEquivalentUCNorm)

View graph