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

Proved

OAI.MarkovSuperreflexivity.MarkovTypeWith.not_coordinatesRepresentable

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

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

theorem MarkovTypeWith.not_coordinatesRepresentable {p K : ℝ}
    (hX : MarkovTypeWith p K X) (hp : 1 < p) (N : OrderedNorm) :
    ¬ CoordinatesRepresentable X N

Definitions. The statement is written with OAI.MarkovSuperreflexivity.CoordinatesRepresentable and OAI.MarkovSuperreflexivity.OrderedNorm (definitions bundle OAISMk000 of this split); OAI.MarkovSuperreflexivity.MarkovTypeWith (the published bundle Def_MarkovType).

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

Preamble

import Mathlib
import Init.Data.List.Count
import Lean.Elab.Tactic.Omega
import Definitions.Def_MarkovType
import Definitions.Def_OAISMk000

Formal statement

section

attribute [-instance] _root_.OAI.MarkovSuperreflexivity.sequenceL2ExponentAtLeastOne
set_option linter.all false
set_option linter.unusedVariables false
set_option linter.unusedTactic false
set_option linter.unreachableTactic false

namespace OAI

noncomputable section

namespace MarkovSuperreflexivity

variable {X : Type*} [NormedAddCommGroup X] [NormedSpace ℝ X]

theorem MarkovTypeWith.not_coordinatesRepresentable {p K : ℝ}
    (hX : MarkovTypeWith p K X) (hp : 1 < p) (N : OrderedNorm) :
    ¬ CoordinatesRepresentable X N := by
  sorry

end MarkovSuperreflexivity

end

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/MarkovObstruction.lean (declaration OAI.MarkovSuperreflexivity.MarkovTypeWith.not_coordinatesRepresentable)

View graph