Nontrivial Markov Type Forces Superreflexivity

Formalization

• OpenAI math release, Lean scope notes for result 327: Markov type characterizes superreflexivity (lean/docs/327.md, 2026). Describes the formalized statement, which is that a real Banach space (including the zero space) has nontrivial Markov type exactly when it admits an equivalent uniformly convex norm, together with consequences for uniformly smooth renormings and reflexivity of finitely representable spaces. [family-level]
• OpenAI math release, lean/OAI/Analysis/MarkovType/Main.lean (Lean 4 source, 2026). Contains the release's Lean theorem OAI.MarkovSuperreflexivity.hasNontrivialMarkovType_iff_hasEquivalentUCNorm and both of its directions, including a separate Markov type 2 corollary. [family-level]
• OpenAI math release, lean/ComparatorChallenges/MarkovType.lean (Lean 4 comparator statement, 2026). Gives the self-contained statement of the main equivalence with sorry, together with definitions of finite reversible chains, Markov type and equivalent uniformly convex norms. [family-level]

Possibly relevant literature (found by the agent, not checked)

• M. Mendel and A. Naor, Scaled Enflo type is equivalent to Rademacher type (arXiv:math/0506215; Bull. London Math. Soc. 39 (2007)). Connects metric type notions to Rademacher type for Banach spaces, which bears on the paper's remark that Rademacher type alone does not force superreflexivity.
• J. Ding, J. R. Lee and Y. Peres, Markov type and threshold embeddings (arXiv:1208.6088, 2012). Proves that threshold embeddings into p-uniformly smooth spaces give Markov type p, which extends the Naor–Peres–Schramm–Sheffield input used for the converse direction.
• M. I. Ostrovskii, Metric characterizations of superreflexivity in terms of word hyperbolic groups and finite graphs (arXiv:1312.4627; Anal. Geom. Metr. Spaces 2 (2014)). Gives another metric characterization of superreflexivity alongside the tree and diamond characterizations listed in the paper's introduction.
• M. I. Ostrovskii and B. Randrianantoanina, A characterization of superreflexivity through embeddings of lamplighter groups (arXiv:1807.06692; Proc. Amer. Math. Soc. 147 (2019)). Finite lamplighter groups give another family of metric test spaces for superreflexivity, relevant to the Ribe-program context in which the paper places its characterization.

Digests and expositions

• Latent Seminar, Markov type and superreflexivity (6 October 2026). Outlines the ordered-norm construction, reversible chart transport and finite lattice lift used in the manuscript, and states that it does not independently verify the complete proof. [family-level]
• Open Mathematics Courses / Claude Opus 5.5, Markov type and superreflexivity (undated). A five-lesson exposition of the manuscript with proofs and exercises that treats the James–Enflo theorem as a named hypothesis and describes its checking as AI self-checking with independent review incomplete. [AI-generated per source] [family-level]