# Markov type characterizes superreflexivity > Proves that a Banach space with nontrivial Markov type is superreflexive, answering a question of Naor. Plain-English explainer, Lean status and sources. Canonical: https://closedform.nishachay.tech/e/openai-math-2026-327/ Last updated: 2026-10-14 **Proves that a Banach space with nontrivial Markov type is superreflexive, answering a question of Naor.** **Trust:** Formal proof listed · **Papers:** 1 · **First paper:** September 23, 2026 · **Field:** Functional analysis · **Entry:** 327 *Explained by AI.* Drafted by one AI model and checked sentence by sentence against the paper by a different one. Spot a mistake? Report an error. Markov type measures how far a random walk can drift when its positions are mapped into a space of vectors. Superreflexivity means the space has an equivalent norm with round, uniformly curved balls. It was known that superreflexive spaces have nontrivial Markov type. This paper proves the converse for real Banach spaces, and Lean checks the result. So nontrivial Markov type and superreflexivity are the same property. ## At a glance - **First step:** 2012 (Assaf Naor, who asked the question in his survey of the Ribe program) - **Significance:** Major. It completes a metric characterization of superreflexivity that the Ribe program had left open, with a Lean check. - **Trust:** Formal proof listed - **Field:** Functional analysis (1 paper) ## The explanation Flip a fair coin and step one unit left or right on the number line. After 100 steps, the average squared distance from the start is exactly 100. So a typical walker is only about 10 units away, not 100. Random walks in straight-line spaces drift like the square root of time. Markov type turns this into a test for a space of vectors. A Banach space is a space of vectors with a norm, a rule for length, in which limits behave well. Take a Markov chain, a random walk on finitely many states that moves by fixed chances. Call it stationary and reversible if it looks the same run forward or backward. Map its states to vectors by any function f. Look at the p-th power of the distance moved, averaged over the walk. The space has Markov type p with constant K if, after t steps, this average is at most K^p times t times the one-step average. Keith Ball introduced this idea to study how maps extend between spaces[1]. A Banach space is superreflexive if it has an equivalent norm that is uniformly convex. Uniformly convex means the midpoint of two far-apart unit vectors is clearly shorter than one. Bourgain showed earlier that such spaces are exactly those that cannot hold large binary trees with small distortion[2]. Naor, Peres, Schramm and Sheffield showed that suitably smooth norms give Markov type[3]. So every superreflexive space has nontrivial Markov type, meaning Markov type for some p above 1. Naor asked whether the converse holds[4]. One obstacle is that a weaker test fails. Rademacher type, which controls sums with random signs, does not force superreflexivity[5]. The paper proves the converse: every real Banach space with Markov type p for some p above 1 is superreflexive[6]. The proof argues by contradiction[7]. If the space is not superreflexive, it builds a special norm on finite lists of numbers. In that norm, adding neighbouring entries together never makes a list longer[8]. For each time n, it then builds a reversible walk whose steps all have length 1. With chance at least 3/20, the sum of its first n steps has length at least n/24[9]. The 3/20 comes from 1/4 minus 1/10. The walk reaches a reduced length of at least n/4 with chance at least 1/4. It fails a technical condition with chance at most 1/10[10]. Then dividing n/4 by 6 gives n/24. Here is why that breaks Markov type 2. The average squared length after n steps is at least 3/20 times (n/24) squared. For n = 384,000, n/24 is 16,000. Then 3/20 times 16,000 squared is 38,400,000, which is 100 times n. Markov type 2 says, roughly, that this average stays below K squared times n. Here K squared would have to be at least n divided by 3,840. As n grows, no fixed K works. How sure is this? Lean, a computer proof checker, has a formal statement of the full result. It says nontrivial Markov type holds exactly when the space has an equivalent uniformly convex norm. So the paper proves this, as far as the Lean statement matches the paper. No specialist review is published. **What it doesn't show.** This does not cover general metric spaces. The theorem is stated for real Banach spaces only. ## Where it came from This result comes from an unreleased OpenAI model, published in the openai/math release on 6 October 2026. ## Hype check Major and Lean-checked. It settles Naor's question for real Banach spaces, not for general metric spaces. No specialist review is published. ## Words used - **Banach space:** A space of vectors with a length rule, called a norm, in which limits of sequences behave well. - **Norm:** A rule that gives each vector a length, with the usual triangle rule. - **Markov chain:** A random walk on a set of states where each move depends only on the current state. - **Stationary and reversible:** A chain whose statistics stay the same over time and look the same run backward. - **Markov type:** A bound saying a walk mapped into the space drifts no faster than a fixed power law in time. - **Uniformly convex:** A norm where the midpoint of two far-apart unit vectors is shorter than 1 by a fixed margin. - **Superreflexive:** A Banach space that has an equivalent uniformly convex norm. - **Rademacher type:** A bound on the length of sums of vectors with independent random plus or minus signs. ## The original paper - [Nontrivial Markov Type Forces Superreflexivity](https://github.com/openai/math/blob/main/preprints/Nontrivial-Markov-Type-Forces-Superreflexivity-September-23-2026/paper.pdf) - September 23, 2026 · Formal proof listed - [Lean notes](https://github.com/openai/math/blob/main/lean/docs/327.md) ## Quoted lines from the paper (10) [1] From [Nontrivial Markov Type Forces Superreflexivity](https://github.com/openai/math/blob/main/preprints/Nontrivial-Markov-Type-Forces-Superreflexivity-September-23-2026/paper.pdf): > Ball introduced Markov type to study Lipschitz extension from metric spaces. [2] From [Nontrivial Markov Type Forces Superreflexivity](https://github.com/openai/math/blob/main/preprints/Nontrivial-Markov-Type-Forces-Superreflexivity-September-23-2026/paper.pdf): > Bourgain characterized it by the distortion of finite complete binary trees; finite diamonds provide another metric test. [3] From [Nontrivial Markov Type Forces Superreflexivity](https://github.com/openai/math/blob/main/preprints/Nontrivial-Markov-Type-Forces-Superreflexivity-September-23-2026/paper.pdf): > Naor, Peres, Schramm, and Sheffield showed that uniform smoothness of power type $p$ implies Markov type $p$ for $1 Pisier's power-type renorming theorem therefore gives nontrivial Markov type to every superreflexive space; Markov type is invariant under equivalent norms. Naor asked whether a Banach space could have nontrivial Markov type without an equivalent uniformly smooth norm. [5] From [Nontrivial Markov Type Forces Superreflexivity](https://github.com/openai/math/blob/main/preprints/Nontrivial-Markov-Type-Forces-Superreflexivity-September-23-2026/paper.pdf): > Ordinary Rademacher type, which controls sums with independent random signs, does not suffice for this conclusion: James constructed nonreflexive spaces of Rademacher type $2$. [6] From [Nontrivial Markov Type Forces Superreflexivity](https://github.com/openai/math/blob/main/preprints/Nontrivial-Markov-Type-Forces-Superreflexivity-September-23-2026/paper.pdf): > Every real Banach space with Markov type $p$ for at least one $p>1$ is superreflexive. [7] From [Nontrivial Markov Type Forces Superreflexivity](https://github.com/openai/math/blob/main/preprints/Nontrivial-Markov-Type-Forces-Superreflexivity-September-23-2026/paper.pdf): > We argue by contradiction. [8] From [Nontrivial Markov Type Forces Superreflexivity](https://github.com/openai/math/blob/main/preprints/Nontrivial-Markov-Type-Forces-Superreflexivity-September-23-2026/paper.pdf): > From it we construct a spreading norm $N$ on finite sequences for which summing consecutive entries is contractive. [9] From [Nontrivial Markov Type Forces Superreflexivity](https://github.com/openai/math/blob/main/preprints/Nontrivial-Markov-Type-Forces-Superreflexivity-September-23-2026/paper.pdf): > For each time $n$, the central task is a finite reversible walk with unit edge labels, changing sign under reversal, whose sum has norm at least $n/24$ with probability at least $3/20$. Before normalization, the labels are sums of signed differences of standard basis vectors in finite coefficient sequences. [10] From [Nontrivial Markov Type Forces Superreflexivity](https://github.com/openai/math/blob/main/preprints/Nontrivial-Markov-Type-Forces-Superreflexivity-September-23-2026/paper.pdf): > With probability at least $1/4-1/10=3/20$, all steps are good and $\ell\geq n/4$. ## Other sources - [openai/math, Lean scope note for family 327](https://github.com/openai/math/blob/main/lean/docs/327.md): “The formalized result proves that a real Banach space has nontrivial Markov type exactly when it admits an equivalent uniformly convex norm, hence exactly when it is superreflexive.” - [openai/math release notes (2026): model provenance and review status](https://github.com/openai/math/blob/main/README.md): “manuscripts and supporting proof artifacts produced by an internal OpenAI model” ## Related - [Metric Markov cotype of ℓ 1 and Hilbert-space Lipschitz extension](https://closedform.nishachay.tech/e/openai-math-2026-332/) - Functional analysis - [The geometric phase diagram, diffusion, and spectra of random planar maps](https://closedform.nishachay.tech/e/openai-math-2026-211/) - Probability and statistical mechanics - [Reflexive midpoint convexity and diamond distortion](https://closedform.nishachay.tech/e/openai-math-2026-331/) - Functional analysis - [Critical SK autocorrelation processes and dynamics across the temperature transition](https://closedform.nishachay.tech/e/openai-math-2026-227/) - Probability and statistical mechanics - [The cotype–cotype conjecture under the approximation property](https://closedform.nishachay.tech/e/openai-math-2026-326/) - Functional analysis - [Functional analysis](https://closedform.nishachay.tech/science/mathematics/functional-analysis/) - Field · 11 results - [Open since the 2010s](https://closedform.nishachay.tech/open-since/2010s/) - Era · 31 results - [Lean-checked results](https://closedform.nishachay.tech/trust/lean-checked/) - Trust · 242 results - [Report an error](https://github.com/nishachay/closed-form/issues/new?template=report-error.yml&labels=entry-error&title=%5Bentry%20327%5D%20)