Superreflexivity from nontrivial Markov type

Superreflexivity from nontrivial Markov type

OpenAI's claim

OpenAI presents the following claims relevant to this question, with manuscript numbers following paper order in Sources. In manuscript 1 (family 327; 2026-09-23), the asserted result is that Markov type with exponent $p>1$ on a real Banach space forces superreflexivity and hence the existence of an equivalent uniformly smooth norm.

Mathematical statement of the claimed result

Manuscript 1.

A real Banach space $X$ has Markov type $p$ with constant $K$ if every finite stationary reversible chain $(Z_t)$, map $f$ of its state space into $X$, and integer $t\ge1$ satisfy \[ \mathbb E\|f(Z_t)-f(Z_0)\|^p\le K^pt\,\mathbb E\|f(Z_1)-f(Z_0)\|^p. \] The asserted implication is \[ (\exists p>1,K<\infty:\ X\text{ has Markov type }p) \Longrightarrow X\text{ admits an equivalent uniformly convex norm}. \] The conclusion is superreflexivity and imposes no separability or finite-dimensionality assumption.

Outline of the argument

For manuscript 1 (family 327; 2026-09-23), a nonsuperreflexive space supplies a finitely represented spreading norm where adjacent equal-sign coefficients merge contractively. Reversible finite charts encode ordered motion with two separated levels, producing a walk that violates any nontrivial Markov-type bound.

Formal verification

For manuscript 1 (family 327; 2026-09-23), OpenAI lists Lean statements for this assertion: Markov type with exponent $p>1$ on a real Banach space forces superreflexivity and hence the existence of an equivalent uniformly smooth norm.

The central assertion is within the documented formal scope; the additional applications retain their own scope limits.

The linked family Comparator checks are MarkovType.lean.

Their named declarations include OAI.MarkovSuperreflexivity.hasNontrivialMarkovType_iff_hasEquivalentUCNorm.

This site has not executed the Lean code. Described statement coverage is not an independent proof check.

Status caveat

The manuscripts were produced by an internal OpenAI model. OpenAI cautions that results without formalization can contain mistakes. This site has not independently checked the proofs; the label records the scope of OpenAI's claim.

Sources

• OpenAI, Nontrivial Markov Type Forces Superreflexivity, 2026-09-23; citation key OAI:Nontrivial-Markov-Type-Forces-Superreflexivity-September-23-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main.
• Family 327: Lean scope.
• Comparator MarkovType.json.
• Comparator MarkovType.lean.
• OpenAI catalogue entry.