Asymptotic midpoint uniform convexity and diamond distortion

Asymptotic midpoint uniform convexity and diamond distortion concerns whether a Banach space whose norm gains length when opposite far-out directions are tested together must admit an equivalent asymptotically uniformly convex norm, and whether a reflexive space without such a norm must contain the countably branching diamond graphs with bounded distortion. Seven manuscripts in OpenAI's public mathematics collection, all dated 27 September 2026, claim a separable reflexive space with an asymptotically midpoint uniformly convex norm and no equivalent asymptotically uniformly convex norm, in which the diamonds have unbounded distortion, together with companion examples. The collection's Lean formalization covers the headline theorem and main statements of the companions.

Background

As recounted in the headline manuscript's introduction:
- Two asymptotic moduli. A norm is asymptotically uniformly convex, AUC, if every step of fixed size in a sufficiently far-out direction increases the norm by a definite amount; it is asymptotically midpoint uniformly convex, AMUC, if the average over a step and its opposite does. Dilworth, Kutzarova, Randrianarivony, Revalski and Zhivkov introduced AMUC, constructed an AMUC norm on ℓ₂ that is not AUC, and asked whether the two properties agree up to renorming. Baudier answered this negatively in 2026, using the Kadets–Werner modification of the Bourgain–Rosenthal space.
- Diamond graphs. The countably branching diamonds are obtained from one edge by repeatedly replacing every edge with countably many two-edge paths. Baudier, Causey, Dilworth, Kutzarova, Randrianarivony, Schlumprecht and Zhang proved that an equivalent AMUC norm prevents uniformly bounded embeddings of these diamonds, and that for reflexive spaces with unconditional asymptotic structure failure of AUC renormability implies such embeddings. Swift and Perreau extended the embedding side under unconditional asymptotic structure, and Basset, Lancien and Procházka and Malthaner obtained further obstructions. The reflexive question without such structure is recorded as Problem 39 in a book by Baudier and Lancien.
- James tree spaces. For the classical binary James tree space, Girardi proved that both the coordinate predual and the full dual are AUC.

The original results

Headline claim, 27 September 2026. The main theorem of Asymptotic midpoint uniform convexity and unbounded diamond distortion in a reflexive tree space concerns the dual X of a James-type segment space on a forest of countably branching trees with unbounded finite heights. It states that X is infinite-dimensional, separable and reflexive, has no equivalent AUC norm, and satisfies the averaged midpoint modulus bound (1 + t²/12)^1/2 − 1 for every t > 0, and that every embedding of the depth-k countably branching diamond into X has distortion no smaller than (1 + k/12)^1/2. It states that this answers the reflexive diamond question negatively.
Companions, 27 September 2026. Midpoint lenses in segment spaces bounds the tail of a displacement in a symmetric midpoint lens by 2(R² − ‖x‖²)^1/2; Distortion of countably branching diamonds from midpoint and tree energies improves the diamond bound to 1 + k/4 ≤ D²; Exact asymptotic moduli in a Daugavet subspace of L1 computes both moduli exactly in a class of subspaces of L₁ with the Daugavet property; and Midpoint convexity from bounded tree potentials and path costs, Independent products in real L1: asymptotic midpoint convexity without AUC renormings and Midpoint convexity from two recursive potentials give further AMUC spaces without equivalent AUC norms, some of them non-reflexive.
Scope, as stated: the headline manuscript does not claim the first separation of the two properties, which it credits to Baudier; its constants are not claimed optimal, and no upper bound on diamond distortion is claimed.
Method, as described: along one root path a sum of coordinate functionals has norm one, while the next coordinate increment is a weakly null unit vector; a hypothetical AUC norm would force repeated multiplicative gains along such a path, which arbitrarily high finite trees contradict. The midpoint estimate adds one correction at the first exit vertices from a finite ancestral set, whose evaluations cancel when the two endpoint norms are averaged, and gives a lower bound in terms of head and tail norms. The infinitely many middle vertices of a diamond supply separated approximate midpoints, which turn this estimate into a loss in squared stretch at every replacement.
Sources. Commit adc7f12 of the openai/math repository: the headline manuscript and the companions on midpoint lenses, on diamond distortion, on a Daugavet subspace of L₁, on bounded tree potentials, on independent products and on recursive potentials.
Formalization. The scope note lists seven Comparator statements, one per manuscript. It states that the Lean development proves the headline theorem for the full dual of the segment space, the lens tail estimate, the unconditional all-pairs bound 1 + k/4 ≤ D², the exact Daugavet moduli with a constructed example, and the main statements of the three further constructions. It also states that some further graph deductions assume 22 companion inputs, which the diamond bounds do not need, and that general-forest and auxiliary results keep their stated support and span hypotheses.

Public follow-up work

Date	Work	Relation	Public claim	Public status (checked 31 October 2026)
2026-10-06	Asymptotic midpoint convexity and tree constructions, an article of the Latent Seminar blog at lowrank.github.io	Reading, exposition	Explains family 331: removing finitely many directions; a reflexive segment-space example; midpoint lenses and a sharper diamond bound; why no equivalent AUC norm exists; exact moduli in a Daugavet subspace of L₁; bounded potentials and independent products; two recursive potentials.	Blog article; it states that its review covers statements, introductions and selected proof mechanisms and is not an independent verification of the complete proofs, and that the scope note's coverage is not blanket verification of every statement in the seven papers. Read on 31 October 2026.
2026-10-08	MathVet, a GitHub review of openai/math, tables at repository commit `c76f1e4` of 14 October 2026	Review, fidelity of the formal statements	Rates this family "full": the headline challenge states, without conditions, the reflexivity, the failure of AUC for every equivalent norm, the midpoint modulus bound and the diamond bound; the other six challenges are companion results. It lists the hand-built asymptotic moduli and the diamond and distortion definitions as definitions to check, and records sandboxed Comparator passes for all seven challenges on 8 October 2026.	Review repository. Read on 31 October 2026.
2026-10-10	cert-machine, openai/math lane K, runs 38040214623 and 38051470892	Verification, two kernels	Records all seven challenges of this family as certified: Lean's default kernel and the nanoda kernel both accept each solution. C. Toledo's report lists the lane's results.	Repository. The runs concern the formalized statements only.
2026-10-10 to 2026-10-14	con-leche development journal, task #348	Verification, second kernel	In its run over all Comparator challenges of the collection at commit `fd4aeeb`, the journal's table of exceptions lists none of the seven challenges of this family, so all seven were accepted by con-leche and by Lean's official kernel.	Development journal.
2026-10-18	AI Proved What?, episode 331 Midpoints aren't enough? Reflexive spaces and diamonds, remade version of 23 October 2026	Reading, exposition	Video explainer of the seven preprints, 225 pages. It recalls the 2016 renorming question, the 2017 diamond obstruction, Problem 39 of a 2025 book, whose authors suspected a positive answer, and Baudier's negative answer to the renorming question on 18 September 2026 in a non-reflexive space, with a proof that his note says was generated by an OpenAI model. It states that the preprints do not claim the first separation, optimal constants or any upper bound on diamond distortion.	Episode status, last checked 30 October 2026: posted as preprints, not revised; under expert review, not yet; peer reviewed, not yet; checked in Lean, the headline theorem in full plus the companions' main statements, in seven checks and about 49,000 lines that the site did not run; it reports that three outside projects re-ran the checks and accepted them, and that it found no specialist comment or reported error. The site states that it is made with Anthropic's Claude. Read on 31 October 2026.

Notes

The background summarizes the headline manuscript's own account of earlier work.
The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.