OAI Math

Motivation: isometries of unit spheres

The Mazur–Ulam theorem (1932) says that every surjective isometry between real normed spaces is affine. The whole space is not always available, though: often only distances between unit vectors are known. Tingley's problem (1987) asks whether the metric of the unit sphere alone already determines the linear structure, that is, whether every surjective isometry between the unit spheres of two real Banach spaces extends to a real-linear isometry of the spaces (Tingley 1987). The question has been studied for almost four decades, mostly class by class: for sequence spaces, $L^p$ spaces, operator algebras and two-dimensional spaces. Nearly all known positive results depend on the structure of the particular spaces involved.

Timeline

• 1932 — Mazur and Ulam: surjective isometries between real normed spaces are affine.
• 1972 — Mankiewicz extends isometries between convex sets with nonempty interior. A unit sphere has empty interior, so this does not apply.
• 1987 — Tingley poses the problem and shows that surjective isometries between spheres of finite-dimensional spaces preserve antipodal points (Tingley 1987).
• 1994 — Wang treats spheres of $C_0(\Omega)$-type spaces (Wang 1994).
• 2003 — Ding handles $\ell^p(\Gamma)$-type spaces, $p>1$, $p\ne 2$ (Ding 2003).
• 2011 — Cheng and Dong formulate the Mazur–Ulam property (sphere isometries from a given space into an arbitrary target extend linearly) (Cheng–Dong 2011).
• 2012 — Tan proves the Mazur–Ulam property for real $L^p(\mu)$, $1<p<\infty$, $p\neq 2$ (Tan 2012).
• 2014 — Tanaka: sphere isometries preserve maximal convex subsets of the sphere (Tanaka 2014).
• 2018 — Fernández-Polo and Peralta (von Neumann algebras, JMAA 2018); Mori (preduals, JMAA 2018).
• 2020 — Mori and Ozawa: Mazur–Ulam property for unital $C^*$-algebras and real von Neumann algebras (Studia Math. 2020).
• 2022 — Banakh: every two-dimensional real Banach space has the Mazur–Ulam property (Banakh 2022).
• 2025–2026 — Further class results: Schreier spaces (Fakhoury 2025); Haagerup noncommutative $L_p$ and Schatten classes (Huang–Zhu, arXiv:2608.30131; arXiv:2607.11244).
• 2026 — An OpenAI preprint, A positive solution to Tingley's problem (OpenAI Math Release, September 23, 2026), claims the general affirmative answer for all real Banach spaces. It has not been peer reviewed, and the claim has not been formally verified.

Setting

Let $X$ and $Y$ be real Banach spaces, both nonzero. The unit sphere is $S_X=\{x\in X:\|x\|=1\}$ with the metric inherited from $X$. A map $f:S_X\to S_Y$ is an isometry if $\|f(x)-f(y)\|=\|x-y\|$ for all $x,y\in S_X$, and it is surjective if every point of $S_Y$ is attained.

Any linear extension of $f$ is forced to be the radial extension

$$T(0)=0,\qquad T(x)=\|x\|\,f\!\left(\frac{x}{\|x\|}\right)\quad(x\neq 0).$$

In Lean, UnitSphere X is the subtype $\{x : X \mid \|x\|=1\}$ and normalize x hx is $x/\|x\|$ as an element of it.

Formalization targets

Goal: Tingley's problem (Theorem 1.1)

For nonzero real Banach spaces $X,Y$ and every surjective isometry $f:S_X\to S_Y$ there is a surjective real-linear isometry $T:X\to Y$ such that

$$T|_{S_X}=f,\qquad T(0)=0,\qquad T(x)=\|x\|\,f\!\left(\tfrac{x}{\|x\|}\right)\ (x\neq0),$$

and $T$ is the only real-linear map $X\to Y$ that agrees with $f$ on $S_X$. This is the full statement of Theorem 1.1 of the source. The goal is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. An affirmative answer turns a forty-year class-by-class programme into a single theorem: the metric of the unit sphere of any real Banach space determines the space up to linear isometry. Every space then has the Mazur–Ulam property in the sense of Cheng and Dong, with no separability, reflexivity, smoothness or strict convexity assumptions. For complex Banach spaces viewed as real spaces the conclusion is real-linearity only; complex-linearity is not claimed.

Formalizing it. The claimed proof combines classical tools (supporting functionals, Banach-space ultrapowers, Darbo's fixed-point theorem with the Kuratowski measure of noncompactness, the Mazur–Ulam theorem) with new geometric estimates on aligned chords. A machine-checked proof would certify a result whose proof has not yet been refereed. The Mazur–Ulam theorem itself is already in Mathlib (IsometryEquiv.toRealLinearIsometryEquiv); ultrapowers of Banach spaces and Darbo's theorem are not.

Difficulty

The radial map $T$ preserves norms and preserves distances between points of the same radius. What has to be shown is that it preserves distances between points on different spheres, $\|f(x)-qf(y)\|=\|x-qy\|$ for $0<q<1$, using only distances measured on a single sphere. Once this holds, $T$ is a surjective isometry fixing $0$ and Mazur–Ulam gives linearity. The obvious attempt (extend the isometry to a neighbourhood, or use convex-set extension theorems such as Mankiewicz's) fails because the sphere has empty interior. Structural arguments (smoothness, facial structure, explicit duals) cover only special classes of spaces. In general, the maximal defect $\sup|\|f(x)-qf(y)\|-\|x-qy\||$ need not be attained, and no compactness is available in infinite dimensions.

Formalization scope

• $X$ and $Y$ are arbitrary types with NormedAddCommGroup, NormedSpace ℝ and CompleteSpace, and Nontrivial (the source's "nonzero"). Universe levels are independent, and no separability or dimension hypothesis is imposed.
• The sphere is UnitSphere X := {x // ‖x‖ = 1} with the subtype metric; Isometry f and Function.Surjective f are the hypotheses.
• The conclusion is an existential over X ≃ₗᵢ[ℝ] Y (a bijective real-linear isometry) with the five clauses: agreement on the sphere, $T0=0$, the radial formula, surjectivity, and uniqueness among all X →ₗ[ℝ] Y that agree with $f$ on the sphere. No hypothesis assumes any distance between different radii, so the statement is not trivialized.
• Infrastructure a full development needs: Hahn–Banach supporting functionals, Banach-space ultrapowers (or another attainment device), the Kuratowski measure of noncompactness and Darbo's fixed-point theorem, together with Mathlib's Mazur–Ulam theorem. Ultrapowers and Darbo's theorem would be reusable well beyond this mission.

Selected references

• D. Tingley, Isometries of the unit sphere, Geom. Dedicata 22 (1987), 371–378. https://doi.org/10.1007/BF00147942
• S. Mazur and S. Ulam, Sur les transformations isométriques d'espaces vectoriels normés, C. R. Acad. Sci. Paris 194 (1932), 946–948.
• P. Mankiewicz, On extension of isometries in normed linear spaces, Bull. Acad. Polon. Sci. Sér. Sci. Math. Astronom. Phys. 20 (1972).
• R. S. Wang, Isometries between the unit spheres of $C_0(\Omega)$ type spaces, Acta Math. Sci. 14 (1994), 82–89. https://doi.org/10.1016/S0252-9602(18)30093-6
• G. G. Ding, The isometric extension problem in the unit spheres of $\ell^p(\Gamma)$ $(p>1)$ type spaces, Sci. China Ser. A 46 (2003), 333–338. https://doi.org/10.1360/03ys9035
• L. Cheng and Y. Dong, On a generalized Mazur–Ulam question, J. Math. Anal. Appl. 377 (2011), 464–470. https://doi.org/10.1016/j.jmaa.2010.11.025
• D.-N. Tan, Extension of isometries on the unit sphere of $L^p$ spaces, Acta Math. Sin. (Engl. Ser.) 28 (2012), 1197–1208. https://doi.org/10.1007/s10114-011-0302-6
• R. Tanaka, A further property of spherical isometries, Bull. Aust. Math. Soc. 90 (2014), 304–310. https://doi.org/10.1017/S0004972714000185
• F. J. Fernández-Polo and A. M. Peralta, On the extension of isometries between the unit spheres of von Neumann algebras, J. Math. Anal. Appl. 466 (2018), 127–143. https://doi.org/10.1016/j.jmaa.2018.05.062
• M. Mori, Tingley's problem through the facial structure of operator algebras, J. Math. Anal. Appl. 466 (2018), 1281–1298. https://doi.org/10.1016/j.jmaa.2018.06.050
• M. Mori and N. Ozawa, Mankiewicz's theorem and the Mazur–Ulam property for $C^*$-algebras, Studia Math. 250 (2020), 265–281. https://doi.org/10.4064/sm180727-14-11
• T. Banakh, Every 2-dimensional Banach space has the Mazur–Ulam property, Linear Algebra Appl. 632 (2022), 268–280. https://doi.org/10.1016/j.laa.2021.09.020
• G. Darbo, Punti uniti in trasformazioni a codominio non compatto, Rend. Sem. Mat. Univ. Padova 24 (1955), 84–92.
• OpenAI, A positive solution to Tingley's problem, OpenAI Math Release preprint, September 23, 2026 (Theorem 1.1, p. 1). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-positive-solution-to-Tingleys-problem-September-23-2026/paper.pdf

Motivation

For a square matrix $A$, the spectrum alone does not control the size of $p(A)$: a nonzero nilpotent matrix has spectrum $\{0\}$ yet $\|A\|>0$. The numerical range $W(A)=\{u^*Au:\ \|u\|=1\}$ is a compact convex set containing the spectrum (Toeplitz–Hausdorff), and it does retain enough information. Crouzeix's conjecture (2004) asserts that for every polynomial $p$,

$$\|p(A)\|\le 2\max_{z\in W(A)}|p(z)|,$$

i.e. that $W(A)$ is a $2$-spectral set; the constant $2$ would be optimal. Such bounds are used to estimate matrix functions in numerical linear algebra (for example GMRES convergence through Faber polynomials) and in operator theory. The complete version asks for the same constant when the polynomial has $m\times m$ matrix coefficients, uniformly in $m$; by Paulsen's theorem this is equivalent to similarity of the conformal disk image of $A$ to a contraction with condition number at most $2$.

Background

• 1918–1919 — Toeplitz and Hausdorff prove convexity of the numerical range (Math. Z. 1918, Math. Z. 1919).
• 1972, 1984 — Arveson's dilation theory (Acta Math. 128, 1972) and Paulsen's similarity theorem (Proc. AMS 92, 1984) relate complete contractivity, dilations and similarity.
• 1999 — Delyon and Delyon's positive integral representations (Bull. SMF 1999).
• 2004 — Crouzeix formulates the constant-two question (IEOT 2004); 2007 — he proves a universal complete bound $11.08$ (JFA 2007).
• 2006 — Badea, Crouzeix and Delyon obtain the complete constant $2$ for $2\times2$ matrices (Math. Z. 2006).
• 2017–2018 — Crouzeix and Palencia prove the complete bound $1+\sqrt2$ (SIMAX 2017); Ransford and Schwenninger simplify the argument (SIMAX 2018).
• 2026 — Scalar ($m=1$) constant-two proofs appear in preprints of Jin, Lorist–Schwenninger (arXiv:2608.03841) and Luo; Åhag, Czyż and Virtanen prove the complete inequality for base matrices of order at most three (arXiv:2608.27346).
• September 2026 — Two OpenAI preprints claim the complete inequality in all dimensions: a structural proof via an optimal similarity and a common positive boundary density, extended to all bounded Hilbert-space operators (source), and a direct coefficient proof for matrices (source).

This mission asks for a formal proof of the complete Crouzeix inequality for matrices, with its sharpness, as stated in Theorem 1.1 of an OpenAI preprint dated September 26, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Setting

For $A\in M_n(\mathbb C)$ ($n\ge1$) let $W(A)=\{u^*Au: u\in\mathbb C^n,\ u^*u=1\}$. A matrix polynomial of degree $d$ with coefficient size $m\ge1$ is $P(z)=\sum_{k=0}^dB_kz^k$ with $B_k\in M_m(\mathbb C)$. Its evaluation at $A$ is

$$P[A]=\sum_{k=0}^d A^k\otimes B_k\ \in M_n(\mathbb C)\otimes M_m(\mathbb C),$$

with the base space first. All norms are Euclidean operator norms. For $m=1$ this is the usual $p(A)$.

Formalization targets

Milestone: the inequality (Theorem 1.1, p. 1, first assertion)

For all $n,m\ge1$, $d\ge0$, $A\in M_n(\mathbb C)$ and $B_0,\dots,B_d\in M_m(\mathbb C)$,

$$\Bigl\|\sum_{k=0}^dA^k\otimes B_k\Bigr\|\ \le\ 2\max_{z\in W(A)}\Bigl\|\sum_{k=0}^dB_kz^k\Bigr\| .$$

Milestone: sharpness (Theorem 1.1, p. 1, second assertion)

If the inequality holds with a constant $c$ in place of $2$ for all $n,m,d,A,B$, then $c\ge2$.

Goal: Theorem 1.1 (p. 1)

Both assertions together: the constant $2$ is valid and no smaller universal constant is.

Significance

The result itself. It settles the complete Crouzeix conjecture in its matrix formulation, uniformly in the base dimension $n$, the coefficient size $m$ and the degree, including matrices whose numerical range is a point or a segment. The scalar case $m=1$ had recently been proved by other authors and the complete case was known only for $n\le3$; a scalar argument need not survive matrix amplification because coefficient matrices do not commute. Equivalently, the numerical range is a complete $2$-spectral set for every matrix, which via Paulsen's theorem gives a similarity of condition number at most $2$ making the conformal disk image of $A$ a contraction. A companion OpenAI preprint gives a separate structural proof and extends the bound to all bounded operators on Hilbert spaces.

Formalizing it. The proof uses exterior conformal maps of analytic convex domains, Faber-type coefficients, a positive double-layer kernel, and a $2\times2$ block positivity argument; Section 4 then approximates an arbitrary numerical range by analytic convex domains. A formal proof would provide numerical ranges, Faber polynomials and conformal collars in Lean, all reusable in matrix analysis. No machine-checked proof of any constant-$2$ Crouzeix bound is known.

Difficulty

The naive approach through the spectrum fails for non-normal matrices, and the classical Crouzeix–Palencia method (a positive double-layer potential plus a Cauchy transform of conjugate data) loses a factor and yields $1+\sqrt2$. To reach $2$ in the complete setting, the argument must keep both multiplication orders $FG$ and $GF$ of matrix-valued test functions, since the coefficients do not commute. The preprint chooses a top singular pair $(x,y)$ of $F[A]$, represents three functionals through the resolvent, and must show that the resulting coefficient weights (one on the constant term, one half on the others) match exactly the Fourier weights of the diagonal compressions (Section 2, Proposition 2.2, p. 5; Theorem 3.2, p. 6). Degenerate numerical ranges with empty interior require a separate approximation step (Lemma 4.1, p. 9).

Formalization scope

• Matrices are Matrix (Fin n) (Fin n) ℂ with the L2 operator norm (Matrix.Norms.L2Operator). The numerical range is the set of $\langle x, Ax\rangle$ over unit vectors of EuclideanSpace ℂ (Fin n).
• Coefficients are B : Fin (d+1) → Matrix (Fin m) (Fin m) ℂ; the evaluation is $\sum_k A^k\otimes_{\mathrm{Kron}}B_k$ indexed by Fin n × Fin m, base factor first.
• rangeMaximum A B is the sSup of $\|P(z)\|$ over $W(A)$. Since $n\ge1$, $W(A)$ is nonempty and compact, so this is the true maximum; UniversalBound C quantifies over all $n,m\ge1$, all $d$, all $A$ and $B$.
• The goal OAI.CompleteCrouzeix.main is UniversalBound 2 ∧ ∀ C, UniversalBound C → 2 ≤ C. The two milestones state the same two clauses in the DirectCrouzeix namespace, whose definitions are identical in content.
• No normality, invertibility or nonempty-interior hypothesis is imposed on $A$.

Selected references

• OpenAI, A direct proof of the complete Crouzeix inequality, OpenAI Math Release preprint, September 26, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-direct-proof-of-the-complete-Crouzeix-inequality-September-26-2026/paper.pdf
• OpenAI, The complete Crouzeix theorem: optimal similarity and a common positive boundary representation, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-complete-Crouzeix-theorem-September-23-2026/paper.pdf
• M. Crouzeix, Bounds for analytical functions of matrices, Integral Equations Operator Theory 48 (2004), 461–477. https://doi.org/10.1007/s00020-002-1188-6
• M. Crouzeix, Numerical range and functional calculus in Hilbert space, J. Funct. Anal. 244 (2007), 668–690. https://doi.org/10.1016/j.jfa.2006.10.013
• M. Crouzeix, C. Palencia, The numerical range is a $(1+\sqrt2)$-spectral set, SIAM J. Matrix Anal. Appl. 38 (2017), 649–655. https://doi.org/10.1137/17M1116672
• T. Ransford, F. L. Schwenninger, Remarks on the Crouzeix–Palencia proof that the numerical range is a $(1+\sqrt2)$-spectral set, SIAM J. Matrix Anal. Appl. 39 (2018), 342–345. https://doi.org/10.1137/17M1143757
• C. Badea, M. Crouzeix, B. Delyon, Convex domains and K-spectral sets, Math. Z. 252 (2006), 345–365. https://doi.org/10.1007/s00209-005-0857-y
• B. Delyon, F. Delyon, Generalization of von Neumann's spectral sets and integral representation of operators, Bull. Soc. Math. France 127 (1999), 25–41. https://doi.org/10.24033/bsmf.2340
• E. Lorist, F. L. Schwenninger, A solution to Crouzeix's conjecture, arXiv:2608.03841 (2026). https://arxiv.org/abs/2608.03841v2
• P. Åhag, R. Czyż, J. Virtanen, The complete Crouzeix conjecture in dimension three and the Clouâtre–Ostermann–Ransford conjecture, arXiv:2608.27346 (2026). https://arxiv.org/abs/2608.27346v4
• O. Toeplitz, Das algebraische Analogon zu einem Satze von Fejér, Math. Z. 2 (1918), 187–197. https://doi.org/10.1007/BF01212904
• F. Hausdorff, Der Wertvorrat einer Bilinearform, Math. Z. 3 (1919), 314–316. https://doi.org/10.1007/BF01292610

Motivation

For a square matrix $A$, the spectrum alone does not control the size of $p(A)$: a nonzero nilpotent matrix has spectrum $\{0\}$ yet $\|A\|>0$. The numerical range $W(A)=\{u^*Au:\ \|u\|=1\}$ is a compact convex set containing the spectrum (Toeplitz–Hausdorff), and it does retain enough information. Crouzeix's conjecture (2004) asserts that for every polynomial $p$,

$$\|p(A)\|\le 2\max_{z\in W(A)}|p(z)|,$$

i.e. that $W(A)$ is a $2$-spectral set; the constant $2$ would be optimal. Such bounds are used to estimate matrix functions in numerical linear algebra (for example GMRES convergence through Faber polynomials) and in operator theory. The complete version asks for the same constant when the polynomial has $m\times m$ matrix coefficients, uniformly in $m$; by Paulsen's theorem this is equivalent to similarity of the conformal disk image of $A$ to a contraction with condition number at most $2$.

Background

• 1918–1919 — Toeplitz and Hausdorff prove convexity of the numerical range (Math. Z. 1918, Math. Z. 1919).
• 1972, 1984 — Arveson's dilation theory (Acta Math. 128, 1972) and Paulsen's similarity theorem (Proc. AMS 92, 1984) relate complete contractivity, dilations and similarity.
• 1999 — Delyon and Delyon's positive integral representations (Bull. SMF 1999).
• 2004 — Crouzeix formulates the constant-two question (IEOT 2004); 2007 — he proves a universal complete bound $11.08$ (JFA 2007).
• 2006 — Badea, Crouzeix and Delyon obtain the complete constant $2$ for $2\times2$ matrices (Math. Z. 2006).
• 2017–2018 — Crouzeix and Palencia prove the complete bound $1+\sqrt2$ (SIMAX 2017); Ransford and Schwenninger simplify the argument (SIMAX 2018).
• 2026 — Scalar ($m=1$) constant-two proofs appear in preprints of Jin, Lorist–Schwenninger (arXiv:2608.03841) and Luo; Åhag, Czyż and Virtanen prove the complete inequality for base matrices of order at most three (arXiv:2608.27346).
• September 2026 — Two OpenAI preprints claim the complete inequality in all dimensions: a structural proof via an optimal similarity and a common positive boundary density, extended to all bounded Hilbert-space operators (source), and a direct coefficient proof for matrices (source).

This mission asks for a formal proof of the complete Crouzeix inequality for all bounded operators on complex Hilbert spaces, with its sharpness, as stated in Corollary 6.3 of an OpenAI preprint dated September 23, 2026 (source), together with the preprint's structural theorems as milestones. The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Setting

For $A\in M_n(\mathbb C)$ ($n\ge1$) let $W(A)=\{u^*Au: u\in\mathbb C^n,\ u^*u=1\}$. A matrix polynomial of degree $d$ with coefficient size $m\ge1$ is $P(z)=\sum_{k=0}^dB_kz^k$ with $B_k\in M_m(\mathbb C)$. Its evaluation at $A$ is

$$P[A]=\sum_{k=0}^d A^k\otimes B_k\ \in M_n(\mathbb C)\otimes M_m(\mathbb C),$$

with the base space first. All norms are Euclidean operator norms. For $m=1$ this is the usual $p(A)$.

For a bounded operator $A$ on a complex Hilbert space $\mathcal H\neq\{0\}$, $W(A)=\{\langle x,Ax\rangle:\|x\|=1\}$ and $K=\overline{W(A)}$; $P[A]=\sum_kA^k\otimes B_k$ acts on $\mathcal H\otimes\mathbb C^m$. A bounded open convex $\Omega\subset\mathbb C$ is admissible if its boundary is a regular real-analytic Jordan curve. For such $\Omega\supset W(A)$ ($A$ a matrix) with interior conformal map $f:\Omega\to\mathbb D$, put $T=f(A)$ and

$$\kappa^2=\min\{\tau:\ I\preceq H\preceq\tau I,\ T^*HT\preceq H\ \text{for some } H=H^*\}.$$

Formalization targets

Milestone: geometry of the numerical range (Corollary 6.3, p. 16, first assertion)

For $\mathcal H\neq\{0\}$, $K=\overline{W(A)}$ is compact and convex and contains $\operatorname{spec}(A)$.

Milestone: the zero space (Corollary 6.3, p. 16, case $\mathcal H=\{0\}$)

If $\mathcal H=\{0\}$, the numerical range is empty, every polynomial, holomorphic and rational evaluation is $0$, and the corresponding inequalities read $0\le0$ (with the supremum over the empty set taken to be $0$).

Milestone: optimal metric and common positive representation (Lemma 1.1, Theorems 1.2–1.3, p. 2)

For admissible $\Omega$ conformal coordinates exist; for every $n\ge1$ and $A\in M_n(\mathbb C)$ with $W(A)\subset\Omega$, the problem defining $\kappa^2$ is strictly feasible with attained minimum $1\le\kappa^2\le4$; for a minimizer $H$, $S=H^{1/2}$ satisfies $\|S\|\|S^{-1}\|=\kappa\le2$ and $D=Sf(A)S^{-1}$ is a contraction with $\rho(D)<1$; and one continuous $\Lambda:\mathbb T\to M_n(\mathbb C)$ with $\Lambda\succeq0$, $\int\Lambda\,d\sigma=I$ represents $v[SAS^{-1}]=\int\Lambda(t)\otimes v(G(t))\,d\sigma(t)$ for every $m$ and every $M_m$-valued $v$ holomorphic near $\overline\Omega$, giving $\|v[A]\|\le\kappa\max_{\overline\Omega}\|v\|$.

Milestone: the matrix inequality (Corollary 6.1, p. 15)

For all $n,m\ge1$, $d\ge0$, $A\in M_n(\mathbb C)$, $B_k\in M_m(\mathbb C)$: $\|P[A]\|\le2\max_{W(A)}\|P\|$, and no smaller universal constant works.

Goal: Corollary 6.3 (p. 16)

For every complex Hilbert space $\mathcal H$ (no separability assumption) and $A\in B(\mathcal H)$: if $\mathcal H\neq\{0\}$ then $K$ is compact, convex, contains the spectrum, and for every $m\ge1$

$$\|P[A]\|\le 2\sup_{W(A)}\|P\|=2\max_K\|P\|,\qquad \|F[A]\|\le2\max_K\|F\|,\qquad \|R[A]\|\le 2\max_K\|R\|$$

for matrix polynomials $P$, matrix functions $F$ holomorphic on an open $U\supseteq K$ (holomorphic functional calculus), and matrix rational functions $R$ with poles off $K$; if $\mathcal H=\{0\}$ the degenerate statements above hold; and the constant $2$ is optimal.

Significance

The result itself. It resolves the complete Crouzeix conjecture in its operator formulation, independent of the Hilbert space, the coefficient size and the degree: $\overline{W(A)}$ is a complete $2$-spectral set for every bounded operator. The structural theorems give more than the inequality: an optimal similarity, attained, with condition number at most $2$, and one positive boundary density that represents every matrix-valued analytic evaluation simultaneously. These are the objects predicted abstractly by Paulsen's and Arveson's theorems, constructed here explicitly. A companion OpenAI preprint gives an independent direct proof of the matrix inequality.

Formalizing it. Mathlib has bounded operators, the holomorphic functional calculus is only partially available, and conformal mapping of analytic Jordan domains is absent. A complete development needs the Riemann mapping theorem with boundary extension, semidefinite optimization over Hermitian matrices, Haar integration on the circle, and a finite-compression argument for nonseparable spaces.

Difficulty

Two obstacles stand out. First, the passage from the scalar to the complete inequality: scalar proofs exploit commutativity that fails for matrix coefficients, so a structure valid for every coefficient size at once is needed; here it is the optimal metric chosen before any test function. Proving $\kappa\le2$ for that metric requires an endpoint extremal pair (Proposition 2.2, p. 6) and an ordered density comparison (Lemma 5.1, p. 14). Second, the passage from matrices to arbitrary operators: the numerical range of a compression lies in $W(A)$, but one must show every vector of $\mathcal H\otimes\mathbb C^m$ and its image under $P[A]$ live in a finite-dimensional compression, and treat holomorphic and rational calculi through contour integrals around the closed numerical range.

Formalization scope

• H is any type with InnerProductSpace ℂ H and CompleteSpace H; operators are H →L[ℂ] H. The amplification $\mathcal H\otimes\mathbb C^m$ is the completion of the algebraic tensor product, and $A^k\otimes B_k$ is the completed TensorProduct.mapL.
• supNorm S F = sSup (insert 0 (‖F ·‖ '' S)), so the supremum over an empty set is $0$, matching the convention of Corollary 6.3.
• Holomorphic evaluation is defined by a contour integral over a CalculusContour around $K$ inside $U$; the goal asserts such contours exist and that the evaluation is contour-independent. Rational evaluation inverts aeval A denom; the goal asserts these denominators are units and that the rational evaluation agrees with the holomorphic one.
• SharpConstant is witnessed by a $2\times2$ matrix with $\sup_{W}|P|=1$ and $\|P[A]\|=2$.
• The structural milestone also includes, as an extra conjunct, that the open unit disk is admissible.

Two further published supporting statements are included as items but not milestones: existence of a finite-dimensional compression representing a given vector (a step in the proof of Corollary 6.3) and invertibility of rational denominators (the well-definedness part of the rational calculus).

Selected references

• OpenAI, The complete Crouzeix theorem: optimal similarity and a common positive boundary representation, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-complete-Crouzeix-theorem-September-23-2026/paper.pdf
• OpenAI, A direct proof of the complete Crouzeix inequality, OpenAI Math Release preprint, September 26, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-direct-proof-of-the-complete-Crouzeix-inequality-September-26-2026/paper.pdf
• V. I. Paulsen, Completely bounded homomorphisms of operator algebras, Proc. Amer. Math. Soc. 92 (1984), 225–228.
• W. Arveson, Subalgebras of C-algebras II*, Acta Math. 128 (1972), 271–308.
• M. Crouzeix, Bounds for analytical functions of matrices, Integral Equations Operator Theory 48 (2004), 461–477. https://doi.org/10.1007/s00020-002-1188-6
• M. Crouzeix, Numerical range and functional calculus in Hilbert space, J. Funct. Anal. 244 (2007), 668–690. https://doi.org/10.1016/j.jfa.2006.10.013
• M. Crouzeix, C. Palencia, The numerical range is a $(1+\sqrt2)$-spectral set, SIAM J. Matrix Anal. Appl. 38 (2017), 649–655. https://doi.org/10.1137/17M1116672
• T. Ransford, F. L. Schwenninger, Remarks on the Crouzeix–Palencia proof that the numerical range is a $(1+\sqrt2)$-spectral set, SIAM J. Matrix Anal. Appl. 39 (2018), 342–345. https://doi.org/10.1137/17M1143757
• C. Badea, M. Crouzeix, B. Delyon, Convex domains and K-spectral sets, Math. Z. 252 (2006), 345–365. https://doi.org/10.1007/s00209-005-0857-y
• B. Delyon, F. Delyon, Generalization of von Neumann's spectral sets and integral representation of operators, Bull. Soc. Math. France 127 (1999), 25–41. https://doi.org/10.24033/bsmf.2340
• E. Lorist, F. L. Schwenninger, A solution to Crouzeix's conjecture, arXiv:2608.03841 (2026). https://arxiv.org/abs/2608.03841v2
• P. Åhag, R. Czyż, J. Virtanen, The complete Crouzeix conjecture in dimension three and the Clouâtre–Ostermann–Ransford conjecture, arXiv:2608.27346 (2026). https://arxiv.org/abs/2608.27346v4
• O. Toeplitz, Das algebraische Analogon zu einem Satze von Fejér, Math. Z. 2 (1918), 187–197. https://doi.org/10.1007/BF01212904
• F. Hausdorff, Der Wertvorrat einer Bilinearform, Math. Z. 3 (1919), 314–316. https://doi.org/10.1007/BF01292610

Motivation: the fixed point property in reflexive spaces

A map $F$ is nonexpansive if $\|F(a)-F(b)\|\le\|a-b\|$. Unlike strict contractions, nonexpansive maps need not have fixed points: on a bounded set, existence depends on the geometry of the norm. A Banach space has the fixed point property (FPP) if every nonexpansive self-map of every nonempty closed bounded convex subset has a fixed point. Since the mid-1960s, whether every reflexive Banach space has the FPP in its given norm has been one of the central open questions of metric fixed point theory. Many sufficient geometric conditions are known, but none of them covers all reflexive spaces. In fixed point theory, the question has been listed as unresolved as recently as 2026 (Nourouzi 2026).

Timeline

• 1965 — Browder and Göhde prove the FPP for uniformly convex spaces (Browder 1965; Göhde 1965). Kirk proves it for weakly compact convex sets with normal structure, in particular for closed bounded convex sets with normal structure in reflexive spaces (Kirk 1965).
• 1974–1975 — Bruck's common fixed point theorems for commuting families and compact convex semigroups (Bruck 1974; Bruck 1975).
• 1975–1976 — The Goebel–Karlovitz lemma on approximate fixed point sequences in minimal invariant sets (Goebel 1975; Karlovitz 1976). Karlovitz also shows that a norm on $\ell_2$ without normal structure still has the FPP, so normal structure is not necessary.
• 1981 — Alspach constructs a weakly compact convex subset of $L_1[0,1]$ with a fixed-point-free nonexpansive self-map, so weak compactness alone is insufficient in general Banach spaces (Alspach 1981). Maurey proves the FPP for reflexive subspaces of $L^1$ (Maurey 1981).
• 1985 — Lin proves the weak FPP for spaces with a $1$-unconditional basis (Lin 1985).
• 2006 — García-Falset, Llorens-Fuster and Mazcuñán-Navarro prove the FPP for uniformly nonsquare spaces (JFA 2006); another proof is due to Dowling, Randrianantoanina and Turett (JFA 2008).
• 2009 — Domínguez Benavides shows that every reflexive space admits an equivalent norm with the FPP (JMAA 2009). Changing the norm changes which maps are nonexpansive, so this does not settle the question for the original norm.
• 2019, 2021 — Hanebaly proposes proofs of the original-norm assertion (JP J. Fixed Point Theory Appl. 2019; preprint 2021). Later literature, such as Nourouzi (2026), still treats the question as unresolved.
• 2026 — An OpenAI preprint, Fixed Points of Nonexpansive Maps in Reflexive Banach Spaces (OpenAI Math Release, September 24, 2026), claims a proof for every real reflexive Banach space. It has not been peer reviewed, and the claim has not been formally verified.

Setting

Let $X$ be a real Banach space and $X^{**}$ its continuous bidual. The canonical map $J:X\to X^{**}$, $J(x)(\varphi)=\varphi(x)$, is always a linear isometry, and $X$ is reflexive if $J$ is surjective. A subset $C\subseteq X$ is taken nonempty, closed in the norm topology, bounded and convex. A map $F:C\to C$ is nonexpansive in the given norm of $X$, and a fixed point is a point $a\in C$ with $F(a)=a$.

In Lean, reflexivity is the definition CanonicallyReflexive X, which says that NormedSpace.inclusionInDoubleDual ℝ X is surjective.

Formalization targets

Goal: reflexive spaces have the fixed point property (Theorem 1.1)

$$X \text{ real reflexive Banach},\ C\subseteq X \text{ nonempty, closed, bounded, convex},\ \|F(a)-F(b)\|\le\|a-b\|\ \ \forall a,b\in C \ \Longrightarrow\ \exists\, a\in C:\ F(a)=a.$$

This is exactly Theorem 1.1 of the source. The goal is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. The theorem answers the reflexive-space fixed point problem for the given norm, with no extra geometric assumption (uniform convexity, normal structure, unconditional bases, uniform nonsquareness). With Bruck's 1974 theorem it gives the source's Corollary 1.2: for every commuting family of nonexpansive self-maps of $C$, the common fixed point set is nonempty and is a nonexpansive retract of $C$. Alspach's example shows that reflexivity cannot be weakened to weak compactness of $C$ in an arbitrary Banach space.

Formalizing it. Earlier proposed proofs of the same assertion exist, and the literature has not reached a consensus, so a machine-checked proof would give unusual certainty on a disputed question. The proof relies on the minimal invariant set reduction (Zorn's lemma and weak compactness), the Goebel–Karlovitz lemma, compact semigroups of nonexpansive maps (an Ellis-type idempotent), and a tree construction with weighted telescoping estimates. Mathlib has the bidual, the weak topology, and Banach–Alaoglu, but most of the fixed-point-theoretic layer has to be built.

Difficulty

The classical route reduces a hypothetical counterexample to a minimal invariant weakly compact convex set $K$ of diameter one. By the Goebel–Karlovitz lemma, every approximate fixed point sequence in $K$ is asymptotically diametral. Normal-structure arguments then find a point whose radius is strictly below the diameter. In a general reflexive space there is no such geometric gain, and Karlovitz's example shows that normal structure is not necessary for the conclusion. Alspach's $L_1$ example shows that compactness of $C$ and nonexpansiveness alone cannot produce the contradiction: the proof has to use reflexivity of the whole space (weak compactness of the unit ball of $\overline{\operatorname{span}}(K-K)$), not just of the domain. A further obstacle is that $F$ is nonlinear, so convex combinations of approximate fixed points are not mapped to convex combinations of their images.

Formalization scope

• $X$ is any real normed space with CompleteSpace X, and reflexivity is surjectivity of NormedSpace.inclusionInDoubleDual ℝ X (the continuous bidual). Completeness also follows from reflexivity, so including it is harmless. The scalar field is $\mathbb R$; complex spaces enter as real spaces.
• $C$ is a Set X with Nonempty, IsClosed (norm topology), Bornology.IsBounded and Convex ℝ. $F$ is a function on the subtype C → C, and nonexpansiveness is stated in the original norm of $X$, not in an equivalent norm.
• The conclusion is the existence of a fixed point ∃ a : C, F a = a. Every hypothesis is satisfiable, so the statement is not vacuous: a trivial $C$ is excluded only by nonemptiness, as in the source.
• Infrastructure needed: the minimal invariant set reduction, the Goebel–Karlovitz lemma, compact right-topological semigroups of maps and idempotents (Ellis), and weak compactness in reflexive spaces. These would serve other fixed-point formalizations, for example Kirk's and Browder–Göhde's theorems, which are not formalized in Mathlib.

Selected references

• F. E. Browder, Nonexpansive nonlinear operators in a Banach space, Proc. Natl. Acad. Sci. USA 54 (1965), 1041–1044. https://doi.org/10.1073/pnas.54.4.1041
• D. Göhde, Zum Prinzip der kontraktiven Abbildung, Math. Nachr. 30 (1965), 251–258. https://doi.org/10.1002/mana.19650300312
• W. A. Kirk, A fixed point theorem for mappings which do not increase distances, Amer. Math. Monthly 72 (1965), 1004–1006. https://doi.org/10.2307/2313345
• R. E. Bruck, Jr., A common fixed point theorem for a commuting family of nonexpansive mappings, Pacific J. Math. 53 (1974), 59–71. https://msp.org/pjm/1974/53-1/pjm-v53-n1-p05-p.pdf
• K. Goebel, On the structure of minimal invariant sets for nonexpansive mappings, Ann. Univ. Mariae Curie-Skłodowska Sect. A 29 (1975), 73–77. https://www.bc.umcs.pl/Content/31033/PDF/czas4050_29_1975_9.pdf
• L. A. Karlovitz, Existence of fixed points of nonexpansive mappings in a space without normal structure, Pacific J. Math. 66 (1976), 153–159. https://doi.org/10.2140/pjm.1976.66.153
• D. E. Alspach, A fixed point free nonexpansive map, Proc. Amer. Math. Soc. 82 (1981), 423–424. https://doi.org/10.2307/2043954
• B. Maurey, Points fixes des contractions de certains faiblement compacts de $L^1$, Séminaire d'analyse fonctionnelle (1980–1981), Exposé VIII. https://www.numdam.org/item/SAF_1980-1981____A8_0/
• P.-K. Lin, Unconditional bases and fixed points of nonexpansive mappings, Pacific J. Math. 116 (1985), 69–76. https://doi.org/10.2140/pjm.1985.116.69
• J. García-Falset, E. Llorens-Fuster and E. M. Mazcuñán-Navarro, Uniformly nonsquare Banach spaces have the fixed point property for nonexpansive mappings, J. Funct. Anal. 233 (2006), 494–514. https://doi.org/10.1016/j.jfa.2005.09.002
• T. Domínguez Benavides, A renorming of some nonseparable Banach spaces with the Fixed Point Property, J. Math. Anal. Appl. 350 (2009), 525–530. https://doi.org/10.1016/j.jmaa.2008.02.049
• K. Nourouzi, Reflexivity of Hilbert $K(H)$-modules and fixed-point property for nonexpansive mappings, J. Math. 2026, Article ID 6311273. https://doi.org/10.1155/jom/6311273
• OpenAI, Fixed Points of Nonexpansive Maps in Reflexive Banach Spaces, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 1). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Fixed-Points-of-Nonexpansive-Maps-in-Reflexive-Banach-Spaces-September-24-2026/paper.pdf

Motivation

Covering numbers measure the size of a set at a given scale: $N(A,B)$ is the least number of translates of $B$ needed to cover $A$. Their logarithms, the metric entropy, appear across approximation theory, operator theory (entropy numbers of compact operators), probability (Dudley's bound) and learning theory. A basic question in asymptotic geometric analysis is how metric entropy behaves under duality: if $K$ is hard to cover by $L$, is the polar body $L^\circ$ equally hard to cover by $K^\circ$? The duality conjecture for metric entropy, originating in Pietsch's 1972 work on operator ideals, predicts that the two quantities agree up to universal constants, independently of the dimension.

Timeline

• 1972. Pietsch formulates the duality problem for entropy numbers of operators.
• 1987. König and Milman compare the $n$-th roots of the two covering numbers, which on the logarithmic scale allows an additive error proportional to $n$ (doi:10.1007/BFb0078138).
• 1989. Bourgain, Pajor, Szarek and Tomczak-Jaegermann prove entropy-number comparisons under geometric and regularity assumptions, with rank-dependent losses (doi:10.1007/BFb0090048).
• 2004. Artstein, Milman and Szarek prove the conjecture when one body is a Euclidean ball (hence an ellipsoid) (doi:10.4007/annals.2004.159.1313); Artstein, Milman, Szarek and Tomczak-Jaegermann prove universal duality for convexified packing and state the dimension-free conjecture as Conjecture 1 (doi:10.1007/s00039-004-0486-3).
• 2007. E. Milman obtains a comparison for arbitrary symmetric bodies with logarithmic losses in scale and entropy (doi:10.1007/s00020-006-1479-4).
• 2022. Hu, Peale and Reingold relate dual covering numbers to sample complexity in learning theory (PMLR v167).

The source of this mission is an OpenAI preprint dated September 24, 2026, which disproves the dimension-free conjecture.

Setting

Work in $\mathbb R^n$ with the standard pairing $\langle x,y\rangle=\sum_i x_iy_i$. A convex body is a compact convex set with nonempty interior; it is origin-symmetric if $K=-K$. Its polar is

$$K^\circ=\{y\in\mathbb R^n:\ \langle x,y\rangle\le1\ \text{for all }x\in K\}.$$

For bounded $A$ and a body $B$, the covering number $N(A,B)$ is the least $M$ such that $A\subseteq\bigcup_{j=1}^M(c_j+B)$ for some $c_1,\dots,c_M\in\mathbb R^n$ (centres need not lie in $A$). Logarithms are natural. Let $L=[-1,1]^n$ be the cube; its polar $L^\circ$ is the cross-polytope.

The duality conjecture asks for absolute constants $a,b\ge1$ such that, for every $n$ and all origin-symmetric convex bodies $K,L\subset\mathbb R^n$,

$$\frac1b\log N(L^\circ,aK^\circ)\ \le\ \log N(K,L)\ \le\ b\log N(L^\circ,a^{-1}K^\circ).$$

Formalization targets

Goal: Theorem 1.1

For every $a,b\ge1$ there are $n\ge1$ and an origin-symmetric convex body $K\subset\mathbb R^n$ such that, with $L=[-1,1]^n$,

$$\log N(K,L)\ >\ b\,\log N\bigl(L^\circ,\ a^{-1}K^\circ\bigr).$$

The Lean statement OAI.MetricEntropyDuality.exists_entropy_duality_counterexample_with_covers is open on the platform.

Significance

The theorem shows that the upper inequality of the conjecture fails for every proposed pair of constants, so the two-sided conjecture has a negative answer, even when one body is a cube. It also separates ordinary covering entropy from convexified-packing entropy, for which Artstein–Milman–Szarek–Tomczak-Jaegermann proved universal duality (Corollary 5.1 of the source). Dimension-dependent results (König–Milman, E. Milman) remain compatible with the counterexample, which shows that some dependence on dimension or structure is unavoidable.

The result is stated in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. The counterexample is explicit and finite-dimensional, which makes a full formalization realistic.

Difficulty

The known positive cases (Euclidean balls, ellipsoids, bounded K-convexity) suggest the conjecture is true, and the obvious candidate bodies, products and cubes, satisfy it. A counterexample needs a body whose primal entropy against the cube is large while the polar side is small; the paper reduces this to a finite matrix with entries in $[0,1]$ whose rows are pairwise $1$-separated in the sup norm while the absolutely convex hull of its columns admits a small uniform approximation list. Producing such matrices requires partition structures over finite fields with uniform control over all row coordinates, and the entropy gap must beat every fixed $b$ after the scale change $a^{-1}$.

Formalization scope

• Space: RealSpace (Fin n) = Fin n → ℝ with pairing the standard dot product; cube is $[-1,1]^n$; polar K uses $\le1$.
• Covers A B centers means every $x\in A$ has some centre $c_j$ with $x-c_j\in B$; coveringNumber is the sInf of the admissible $M$. The statement includes Coverable side conditions, which only certify that both infima are over nonempty sets.
• IsSymmetricConvexBody = compact, convex, $x\in K\iff -x\in K$, nonempty interior.
• The scale enters as a⁻¹ • polar K; logs are Real.log of natural numbers cast to reals.

A complete development needs support functions and polarity, elementary covering-number bounds, finite-field polynomial zero bounds (Schwartz–Zippel), and the matrix-to-body conversion. The covering-number and polarity layer is reusable for other convex-geometry missions. Contributions formalizing Lemma 2.1 (matrix-to-body conversion), Proposition 3.2 (uniform compression) and Proposition 4.3 (partitions with separated rows) are welcome.

Selected references

• OpenAI, Counterexamples to the duality conjecture for metric entropy, preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Counterexamples-to-the-duality-conjecture-for-metric-entropy-September-24-2026/main.pdf
• S. Artstein, V. Milman, S. J. Szarek, Duality of metric entropy, Ann. of Math., 2004. https://doi.org/10.4007/annals.2004.159.1313
• S. Artstein, V. Milman, S. Szarek, N. Tomczak-Jaegermann, On convexified packing and entropy duality, Geom. Funct. Anal., 2004. https://doi.org/10.1007/s00039-004-0486-3
• H. König, V. D. Milman, On the covering numbers of convex bodies, GAFA Seminar, 1987. https://doi.org/10.1007/BFb0078138
• J. Bourgain, A. Pajor, S. J. Szarek, N. Tomczak-Jaegermann, On the duality problem for entropy numbers of operators, GAFA Seminar, 1989. https://doi.org/10.1007/BFb0090048
• E. Milman, A remark on two duality relations, Integral Equations Operator Theory, 2007. https://doi.org/10.1007/s00020-006-1479-4
• J. T. Schwartz, Fast probabilistic algorithms for verification of polynomial identities, J. ACM, 1980. https://doi.org/10.1145/322217.322225

Motivation

Uniform convexity of a norm says that the midpoint of two far-apart points of the unit sphere lies strictly inside the ball. In infinite dimensions there is an asymptotic version: one only asks for a gain in directions that lie far out, that is, inside some closed subspace of finite codimension. Asymptotic uniform convexity and its relatives control the large-scale geometry of a Banach space, and in particular which infinite graphs can be embedded into the space with bounded distortion.

Two such properties are compared here. Asymptotic uniform convexity (AUC) demands a gain in every far-out direction separately; asymptotic midpoint uniform convexity (AMUC), introduced by Dilworth, Kutzarova, Randrianarivony, Revalski and Zhivkov (2016), only asks for a gain when a direction and its opposite are tested together. Every AUC norm is AMUC. The question is how far apart the two notions are, both up to renorming and in terms of metric embeddings of the countably branching diamond graphs $D_k$.

Timeline

• 1974. James introduces the square-sum norm over disjoint segments of a tree (the James tree space) (doi:10.1090/S0002-9904-1974-13580-9).
• 2001. Girardi proves that the coordinate predual and the full dual of the binary James tree space are AUC (doi:10.4064/sm147-2-2).
• 2004 and 2009. Lee and Naor obtain quantitative $L_p$ distortion bounds for finite binary diamonds; Johnson and Schechtman relate diamond embeddings to super-reflexivity (doi:10.1007/s00039-004-0473-8, doi:10.1142/S1793525309000114).
• 2016. Dilworth et al. define AMUC and construct an AMUC norm on $\ell_2$ that is not AUC (doi:10.1016/j.jmaa.2015.11.061).
• 2017. Baudier, Causey, Dilworth, Kutzarova, Randrianarivony, Schlumprecht and Zhang show that an equivalent AMUC norm prevents uniform embeddings of the countably branching diamonds, and that for reflexive spaces with unconditional asymptotic structure, failure of AUC renormability forces uniform diamond embeddings (arXiv:1612.01984).
• 2018 and 2021. Swift extends the embedding construction to countably branching bundle graphs under the same hypotheses (arXiv:1710.00877); Perreau treats duals of separable spaces with weak-star unconditional asymptotic structure (arXiv:2104.10494).
• 2025. Baudier and Lancien record, as Problem 39 of their monograph, whether the diamond implication holds for general reflexive spaces (arXiv:2512.00817).
• 2026. Baudier shows that AMUC renormability does not imply AUC renormability, using the Kadets–Werner modification of the Bourgain–Rosenthal space, which is not reflexive (arXiv:2609.21283).

The source of this mission, an OpenAI preprint dated September 27, 2026, gives a reflexive example that separates the two notions and answers the reflexive diamond question negatively.

Setting

All spaces are real. For a Banach space $Y$ with norm $N$, let $\operatorname{cof}(Y)$ be the closed subspaces of finite codimension. For $t>0$,

$$\overline\delta_N(t)=\inf_{N(x)=1}\ \sup_{F\in\operatorname{cof}(Y)}\ \inf_{y\in F,\ N(y)=1}\bigl(N(x+ty)-1\bigr),$$ $$\widehat\delta_N(t)=\inf_{N(x)=1}\ \sup_{F\in\operatorname{cof}(Y)}\ \inf_{y\in F,\ N(y)=1}\Bigl(\tfrac{N(x+ty)+N(x-ty)}{2}-1\Bigr).$$

$N$ is AUC if $\overline\delta_N(t)>0$ for every $t>0$, and AMUC if $\widehat\delta_N(t)>0$ for every $t>0$. A norm $N$ is equivalent to $\|\cdot\|$ if $a\|x\|\le N(x)\le b\|x\|$ for some $0<a\le b$.

The forest. For $h\ge1$ let $T_h=\mathbb N^{\le h}$ be the rooted tree of words of length at most $h$, ordered by extension. The forest $\mathcal F$ is the disjoint union of one copy of $T_h$ for every $h\ge1$. A segment is an interval $[a,b]$ of an ancestral chain. For a finitely supported $u:\mathcal F\to\mathbb R$,

$$\rho(u)=\sup\Bigl\{\Bigl(\sum_{i=1}^m u(S_i)^2\Bigr)^{1/2} : S_1,\dots,S_m\ \text{pairwise disjoint segments}\Bigr\},\qquad u(S)=\sum_{v\in S}u(v).$$

Let $J$ be the completion and $X=J^*$ with the dual norm.

Diamonds. $D_0$ is one edge; $D_{k+1}$ replaces every edge of $D_k$ by countably many internally disjoint two-edge paths. With the shortest-path metric $d_k$, a map $f:D_k\to X$ has distortion at most $C$ if some scale $s>0$ gives $s\,d_k(u,v)\le\|f(u)-f(v)\|\le Cs\,d_k(u,v)$ for all $u,v$.

Formalization targets

Goal: Theorem 1.1

$$X\ \text{is infinite dimensional, separable and reflexive, and admits no equivalent AUC norm;}$$ $$\widehat\delta_X(t)\ \ge\ \sqrt{1+t^2/12}-1\quad(t>0);$$ $$\text{every embedding of }D_k\text{ into }X\text{ has distortion}\ \ge\ \sqrt{1+k/12}\quad(k\ge0).$$

The Lean statement OAI.ForestSpace.main_theorem is the conjunction of these six clauses. It is open on the platform.

Significance

The theorem separates AMUC from AUC renormability inside the reflexive class, which Baudier's 2026 example (non-reflexive) does not. Because AMUC is a property of the given norm while the diamond obstruction is invariant under renorming, the theorem also shows that, for general reflexive spaces, failure of AUC renormability does not force the countably branching diamonds to embed uniformly. This answers Problem 39 of Baudier–Lancien negatively and shows that the unconditional asymptotic structure hypothesis in the 2017 embedding theorem cannot simply be dropped. The quantitative modulus and distortion bounds are explicit, not merely positivity statements.

The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. A formal proof would certify the full construction, including reflexivity of $J^*$ for a non-locally-finite forest and the square-sum distortion recursion.

Difficulty

Two points are delicate. First, reflexivity: the classical James tree space is not reflexive, and here reflexivity comes from using trees of finite but unbounded height together with countable branching; the full dual $J^*$, not the coordinate completion, is the space. Second, the midpoint estimate: a segment test may cross from a finite ancestral set to its complement, and simply adding norming tests for the two parts produces uncontrolled positive cross terms. Non-renormability, by contrast, must be proved for every equivalent norm at once, so it cannot be read off from any computation with the given norm.

Formalization scope

• The space is FullDual Vertex := StrongDual ℝ (J Vertex), where J V is the UniformSpace.Completion of TestVector V (finitely supported functions with norm rho). Vertex packs a height $h\ge1$ and a word in $\mathbb N^*$ of length $\le h$; the order is equality of heights plus prefix order.
• Segments are finite order-convex chains (IsSegment); the empty segment is allowed and contributes zero.
• Reflexive is surjectivity of the canonical map NormedSpace.inclusionInDoubleDual, not an abstract isomorphism with the bidual.
• EquivalentNorm E α β stores a Seminorm with explicit constants $0<\alpha\le\beta$; the lower bound makes it a norm. The non-renormability clause quantifies over all such structures.
• aucModulus and averageModulus take the inf/sup/inf order above, with sInf/sSup over real sets; for an infinite-dimensional space these sets are nonempty and bounded, so the Lean defaults are not triggered.
• Diamond.diamond k iterates the edge replacement starting from one edge; distances are SimpleGraph.dist of the undirected graph, and EmbeddingBound is the scaled bi-Lipschitz condition above.

A complete development needs the James-type segment norm, its completion and dual, coordinate projections onto ancestral sets, and graph distances on the diamonds. The segment-norm and diamond infrastructure is shared with the other missions of this family. Contributions formalizing Lemma 2.1 (structure and reflexivity), Lemma 3.2 (bounded trees exclude AUC renorming), Lemma 4.1 (paired head–tail estimate) and Lemma 5.1 (lens lemma) are welcome.

Selected references

• OpenAI, Asymptotic midpoint uniform convexity and unbounded diamond distortion in a reflexive tree space, preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Asymptotic-midpoint-uniform-convexity-and-unbounded-diamond-distortion-in-a-reflexive-tree-space-September-27-2026/manuscript.pdf
• S. J. Dilworth, D. Kutzarova, N. L. Randrianarivony, J. P. Revalski, N. V. Zhivkov, Lenses and asymptotic midpoint uniform convexity, J. Math. Anal. Appl., 2016. https://doi.org/10.1016/j.jmaa.2015.11.061
• F. Baudier, R. Causey, S. Dilworth, D. Kutzarova, N. L. Randrianarivony, T. Schlumprecht, S. Zhang, On the geometry of the countably branching diamond graphs, J. Funct. Anal., 2017. https://arxiv.org/abs/1612.01984
• F. P. Baudier, G. Lancien, Asymptotic and nonlinear geometries of Banach spaces and their interactions, Cours Spécialisés, SMF, 2026. https://arxiv.org/abs/2512.00817
• F. P. Baudier, The Kadets–Werner modification of Bourgain–Rosenthal space is asymptotically midpoint uniformly convex, preprint, 2026. https://arxiv.org/abs/2609.21283
• R. C. James, A separable somewhat reflexive Banach space with nonseparable dual, Bull. Amer. Math. Soc., 1974. https://doi.org/10.1090/S0002-9904-1974-13580-9
• M. Girardi, The dual of the James tree space is asymptotically uniformly convex, Studia Math., 2001. https://doi.org/10.4064/sm147-2-2
• A. Swift, A coding of bundle graphs and their embeddings into Banach spaces, Mathematika, 2018. https://arxiv.org/abs/1710.00877
• Y. Perreau, On the embeddability of countably branching bundle graphs into dual spaces, preprint, 2021. https://arxiv.org/abs/2104.10494

Motivation

In a uniformly convex space, if $x$ is nearly as long as $R$ and both $x+y$ and $x-y$ have length at most $R$, then the displacement $y$ must be short. The set of such displacements,

$$\mathcal L(x,R)=\{y:\ \|x+y\|\le R,\ \|x-y\|\le R\},$$

is a symmetric lens. In infinite dimensions the right question is asymptotic: is $y$ short after discarding finitely many directions? Dilworth, Kutzarova, Randrianarivony, Revalski and Zhivkov (2016) characterized asymptotic midpoint uniform convexity (AMUC) through the measure of noncompactness of such lenses. AMUC is the property that, together with asymptotic uniform convexity (AUC), governs which countably branching graphs embed into a Banach space with bounded distortion.

This mission asks for an explicit lens estimate in two James-type tree spaces, with a bound depending only on the squared-radius deficit $R^2-\|x\|^2$ of the center and holding for every displacement simultaneously after one finite set of coordinates is removed.

Timeline

• 1974. James introduces the square-sum norm over disjoint segments of a tree (doi:10.1090/S0002-9904-1974-13580-9).
• 1985. Ghoussoub and Maurey study $G_\delta$-embeddings in Hilbert space (doi:10.1016/0022-1236(85)90039-4); the coordinate predual $B_\infty$ used here is the Ghoussoub–Maurey–Schachermayer construction as presented by Banakh (2000).
• 2001. Girardi proves AUC of the canonical predual and of the full dual of the binary James tree space (doi:10.4064/sm147-2-2).
• 2016. Dilworth et al. introduce AMUC and characterize it by lenses (doi:10.1016/j.jmaa.2015.11.061).
• 2017. Baudier, Causey, Dilworth, Kutzarova, Randrianarivony, Schlumprecht and Zhang show that an equivalent AMUC norm prevents uniform embeddings of countably branching diamonds (arXiv:1612.01984).
• 2021. Perreau asks whether the canonical predual of the countably branching James tree space is AMUC (Question 6 of arXiv:2104.10494).
• 2026. Baudier shows that AMUC does not imply AUC renormability, via the Kadets–Werner modification of the Bourgain–Rosenthal space (arXiv:2609.21283).

The source of this mission is an OpenAI preprint dated September 27, 2026.

Setting

All scalars are real.

Finite-height forest. For $h\ge1$ let $T_h=\mathbb N^{\le h}$ be the tree of words of length at most $h$, ordered by extension (the root is the empty word). The forest $\mathcal F$ is the disjoint union of one copy $\{h\}\times T_h$ for each $h\ge1$. Write $a\preceq b$ if $a$ is an ancestor of $b$ in the same component. A segment is a nonempty interval $[a,b]=\{v: a\preceq v\preceq b\}$. For finitely supported $u$ put $u(S)=\sum_{v\in S}u(v)$ and

$$\rho(u)=\sup\Bigl\{\Bigl(\sum_{i=1}^m u(S_i)^2\Bigr)^{1/2}:\ S_1,\dots,S_m\ \text{pairwise disjoint segments}\Bigr\}.$$

Let $J$ be the completion of $(c_{00}(\mathcal F),\rho)$ and $X=J^*$ with the dual norm. Coordinate evaluation gives functionals $e_v^*\in X$.

Infinite tree. Let $T_\infty=\mathbb N^{<\omega}$ (all finite words, root included), $J_\infty$ the completion for the same norm, and $B_\infty=\overline{\operatorname{span}}\{e_v^*\}\subset J_\infty^*$, closed in the dual norm.

A finite set $H$ of vertices is ancestral if it contains all ancestors of its elements. On either space,

$$P_Hx=\sum_{v\in H}x(e_v)\,e_v^*,\qquad Q_Hx=x-P_Hx.$$

Formalization targets

Goal: Theorem 1.1

For $Y\in\{X,\ B_\infty\}$, every finite ancestral $H$, every $x,y\in Y$ with $x=P_Hx$, and every $R\ge0$ with $\|x+y\|\le R$ and $\|x-y\|\le R$,

$$\|Q_Hy\|\ \le\ 2\sqrt{R^2-\|x\|^2}.$$

The Lean statement OAI.SegmentLenses.midpoint_lens_main is the conjunction of the two cases. It is open on the platform. The displacement $y$ may have a nonzero head $P_Hy$; only its tail is controlled.

Significance

The estimate is uniform over the lens: one finite head $H$ controls every admissible displacement, which is exactly what is needed when a single center has infinitely many approximate midpoints. As a consequence (Corollary 7.1 of the source) both given norms are AMUC with $\widehat\delta(t)\ge(\sqrt{1+t^2/4}-1)/2$, while Proposition 9.1 shows that neither space admits an equivalent AUC norm. In particular the infinite-height case answers Perreau's question for the specified real norm on $B_\infty$, and the finite-height forest gives a reflexive space separating AMUC from AUC renormability. A companion preprint uses this theorem to force distortion $D^2\ge1+k/4$ for depth-$k$ countably branching diamonds.

The result is proved only in the OpenAI preprint; it is not peer reviewed and has no machine-checked proof. Formalizing it would certify the cancellation analysis that drives the constant $2$.

Difficulty

The natural attempt is to represent a nearly norming functional for the center as a convex combination of disjoint segment functionals and read off the tail. The obstacle is cancellation: two atoms leaving the head $H$ through the same vertex can have segment sums of opposite sign, and a naive estimate loses all control. The bound must also hold for every displacement with the same $H$, so compactness arguments that choose $H$ after $y$ do not suffice, and an independent radial approach in the source gives only the weaker $(\sqrt2+\sqrt6)\sqrt{R(R-\|x\|)}$.

Formalization scope

• Vertices: ForestVertex is the subtype of pairs $(h,w)$ with $1\le h$ and $|w|\le h$; InfiniteVertex := List ℕ. Ancestry is equality of heights plus List.IsPrefix (resp. prefix only).
• Segments: IsInterval ancestor S asserts $S=[a,b]$ with $a\preceq b$, so segments are nonempty. A test family is a finite set of pairwise disjoint segments, and segmentSeminorm is the supremum of the Euclidean norms of the vectors of segment sums.
• Spaces: X := StrongDual ℝ (UniformSpace.Completion (Test ForestVertex)); BInfinite is the closed span of the coordinate functionals inside the full dual of the infinite-tree completion, carrying the subspace (dual) norm.
• head H x = ∑ v ∈ H, x(e_v) • e_v^* and tail H x = x - head H x; ancestrality is Ancestral.
• Trivialization check: $R\ge0$ is required as in the source, and since $\|x\|\le R$ follows from the lens condition, the square root argument is never negative.

A full development needs the James segment norm, its completion and dual, contractivity of coordinate projections, the $\ell_2$ decomposition of the tail over descendant cones (Lemma 2.2), and the atomic description of finite head balls (Section 4). This infrastructure is shared with the other missions in the same family. Formalizations of Lemma 2.1, Lemma 2.2, Corollary 7.1 and Proposition 9.1 are welcome as supporting results.

Selected references

• OpenAI, Midpoint lenses in segment spaces, preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Midpoint-lenses-in-segment-spaces-September-27-2026/manuscript.pdf
• S. J. Dilworth, D. Kutzarova, N. L. Randrianarivony, J. P. Revalski, N. V. Zhivkov, Lenses and asymptotic midpoint uniform convexity, J. Math. Anal. Appl., 2016. https://doi.org/10.1016/j.jmaa.2015.11.061
• R. C. James, A separable somewhat reflexive Banach space with nonseparable dual, Bull. Amer. Math. Soc., 1974. https://doi.org/10.1090/S0002-9904-1974-13580-9
• M. Girardi, The dual of the James tree space is asymptotically uniformly convex, Studia Math., 2001. https://doi.org/10.4064/sm147-2-2
• Y. Perreau, On the embeddability of countably branching bundle graphs into dual spaces, preprint, 2021. https://arxiv.org/abs/2104.10494
• F. Baudier, R. Causey, S. Dilworth, D. Kutzarova, N. L. Randrianarivony, T. Schlumprecht, S. Zhang, On the geometry of the countably branching diamond graphs, J. Funct. Anal., 2017. https://arxiv.org/abs/1612.01984
• F. P. Baudier, The Kadets–Werner modification of Bourgain–Rosenthal space is asymptotically midpoint uniformly convex, preprint, 2026. https://arxiv.org/abs/2609.21283
• N. Ghoussoub, B. Maurey, $G_\delta$-embeddings in Hilbert space, J. Funct. Anal., 1985. https://doi.org/10.1016/0022-1236(85)90039-4

Motivation

How well can a graph be drawn inside a Banach space without stretching some distances much more than others? The distortion of the best such drawing measures the mismatch between the graph's metric and the geometry of the space. Diamond graphs are a standard test family: each edge is repeatedly replaced by parallel two-edge paths, so the graph contains many "midpoints" between the same two endpoints at every scale. For binary diamonds, bounded distortion in a space is tied to the failure of super-reflexivity (Johnson–Schechtman 2009). For countably branching diamonds, where each edge is replaced by infinitely many paths, the relevant property is asymptotic midpoint uniform convexity (AMUC): an equivalent AMUC norm prevents uniform embeddings (Baudier et al. 2017).

This mission asks for an explicit, quantitative lower bound on the distortion of countably branching diamonds in two specific James-type tree spaces, deduced from a midpoint "lens" estimate for those spaces.

Timeline

• 1974. James introduces the square-sum norm over disjoint tree segments (doi:10.1090/S0002-9904-1974-13580-9).
• 2001. Girardi proves asymptotic uniform convexity of the coordinate predual and dual of the binary James tree space (doi:10.4064/sm147-2-2).
• 2004. Lee and Naor give quantitative lower bounds for binary diamonds in $L_p$, $1<p\le2$, by summing a convexity inequality over levels (doi:10.1007/s00039-004-0473-8).
• 2009. Johnson and Schechtman characterize super-reflexivity by non-embeddability of binary diamonds (doi:10.1142/S1793525309000114).
• 2016. Dilworth, Kutzarova, Randrianarivony, Revalski and Zhivkov introduce AMUC and characterize it via lenses (doi:10.1016/j.jmaa.2015.11.061).
• 2017. Baudier, Causey, Dilworth, Kutzarova, Randrianarivony, Schlumprecht and Zhang prove that an AMUC renorming with power-type modulus $t^p$ forces distortion $\gtrsim k^{1/p}$ for depth-$k$ countably branching diamonds, and prove a converse under unconditional asymptotic structure (arXiv:1612.01984).
• 2018, 2021. Swift and Perreau extend the converse to bundle graphs and dual settings under additional structure (arXiv:1710.00877, arXiv:2104.10494).
• 2025. Malthaner gives a coloring-based proof of the power-type lower bound (arXiv:2310.03257).

The source of this mission is an OpenAI preprint dated September 27, 2026; its lens input comes from the companion OpenAI preprint Midpoint lenses in segment spaces of the same date.

Setting

Diamonds. The normalized diamond $\mathcal D_0$ is one edge of length $1$. $\mathcal D_{k+1}$ replaces every edge of $\mathcal D_k$ by countably many internally disjoint two-edge paths with the same endpoints, each new edge having half the length of its parent. Let $d_k$ be the shortest-path metric. A map $f:\mathcal D_k\to Y$ has distortion at most $D$ if for some scale $s>0$

$$s\,d_k(u,v)\le\|f(u)-f(v)\|\le D\,s\,d_k(u,v)\qquad(u,v\in\mathcal D_k).$$

Tree spaces. Let $\mathcal T=\coprod_{h\ge1}\mathbb N^{\le h}$ (one rooted tree of each finite height, prefix order inside each tree). A segment is the set of vertices between two comparable nodes. For a finitely supported array $a$,

$$\rho(a)=\sup\Bigl\{\Bigl(\sum_{j=1}^m\Bigl|\sum_{s\in S_j}a_s\Bigr|^2\Bigr)^{1/2}:\ S_1,\dots,S_m\ \text{pairwise disjoint segments}\Bigr\}.$$

$J$ is the completion and $X=J^*$ with the dual norm. On $T_\infty=\mathbb N^{<\omega}$ (root included) the same formula defines $J_\infty$, and $B_\infty=\overline{\operatorname{span}}\{e_t^*\}\subset J_\infty^*$ is the closed span of the coordinate functionals.

Formalization targets

Goal: Theorem 1.1

For every $k\ge0$ and every distortion-$D$ embedding of $\mathcal D_k$ into $Y\in\{X,\ B_\infty\}$,

$$D^2\ \ge\ 1+\frac k4.$$

The Lean statement OAI.DiamondDistortion.headline_all_pairs is the conjunction of the two cases. It is open on the platform.

Significance

The bound shows that the countably branching diamonds do not embed with uniformly bounded distortion into either space, with an explicit square-root growth rate. Combined with the companion results that neither space admits an equivalent asymptotically uniformly convex norm, and that the forest dual $X$ is reflexive, it shows that the diamond obstruction can hold in reflexive spaces without AUC renormability, so the unconditional-structure hypotheses in the known converses are doing real work. The constant $1/4$ is obtained by retaining the full quadratic budget of the lens inequality. The paper also gives direct energy proofs (Theorem 5.1, Propositions 4.2–4.3) with weaker constants, and general transfer theorems (Section 7) from lens inequalities to distortion bounds.

The theorem is proved in the OpenAI preprint; it has not been peer reviewed and no machine-checked proof exists. A formalization would certify both the metric deduction and, through its input, the tree-space lens estimate.

Difficulty

The input lens inequality bounds only the tail of a displacement outside a finite head. Turning it into a loss of squared edge stretch at every replacement level requires selecting, among infinitely many middle vertices, two whose head projections nearly coincide, so that their half-difference is a tail vector that still lies in the lens. Doing this simultaneously along a descending chain of edges, with the head growing at each step, and summing the losses without wasting the quadratic budget is where the constant is decided. A binary diamond argument does not transfer, because finitely many midpoints give no near-coincident projections.

Formalization scope

• Diamond.Vertex k and Diamond.Edge k are defined by recursion on the stage, each parent edge receiving new vertices indexed by $\mathbb N$; Diamond.graph k is the undirected replacement graph and Diamond.distance k u v is SimpleGraph.dist divided by $2^k$. Since distortion is scale invariant, the normalization does not affect the statement.
• ForestDual is the full continuous dual of the completion of the finite-height forest James space; InfinitePredual is the norm-closed span of coordinate functionals in the dual of the infinite-tree space, with the subspace norm.
• Segments are nonempty finite intervals of an ancestral partial order; test families are finite and pairwise disjoint.
• The conclusion is stated as $1+k/4\le D^2$, with $s>0$ given and the two-sided bound holding for all pairs $u,v$.

A complete development needs the James segment norm and its dual, coordinate projections onto finite ancestral sets, the companion lens estimate, and graph distances on the countably branching diamonds. This infrastructure is shared with the other missions of this family. Formal proofs of Theorem 7.2 (lens-to-distortion transfer) and Theorem 7.12 (AMUC prevents uniform embeddings) are welcome as reusable components.

Selected references

• OpenAI, Distortion of countably branching diamonds from midpoint and tree energies, preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Diamond-distortion-from-midpoint-and-tree-energies-September-27-2026/manuscript.pdf
• OpenAI, Midpoint lenses in segment spaces, preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Midpoint-lenses-in-segment-spaces-September-27-2026/manuscript.pdf
• F. Baudier, R. Causey, S. Dilworth, D. Kutzarova, N. L. Randrianarivony, T. Schlumprecht, S. Zhang, On the geometry of the countably branching diamond graphs, J. Funct. Anal., 2017. https://arxiv.org/abs/1612.01984
• S. J. Dilworth, D. Kutzarova, N. L. Randrianarivony, J. P. Revalski, N. V. Zhivkov, Lenses and asymptotic midpoint uniform convexity, J. Math. Anal. Appl., 2016. https://doi.org/10.1016/j.jmaa.2015.11.061
• J. R. Lee, A. Naor, Embedding the diamond graph in $L_p$ and dimension reduction in $L_1$, Geom. Funct. Anal., 2004. https://doi.org/10.1007/s00039-004-0473-8
• W. B. Johnson, G. Schechtman, Diamond graphs and super-reflexivity, J. Topol. Anal., 2009. https://doi.org/10.1142/S1793525309000114
• R. Malthaner, On Matoušek-like embedding obstructions of countably branching graphs, J. Math. Anal. Appl., 2025. https://arxiv.org/abs/2310.03257
• R. C. James, A separable somewhat reflexive Banach space with nonseparable dual, Bull. Amer. Math. Soc., 1974. https://doi.org/10.1090/S0002-9904-1974-13580-9
• M. Girardi, The dual of the James tree space is asymptotically uniformly convex, Studia Math., 2001. https://doi.org/10.4064/sm147-2-2

Motivation

A norm is uniformly convex when midpoints of far-apart unit vectors are pushed strictly inside the unit ball. In infinite-dimensional Banach spaces the useful notions are asymptotic: one asks for a gain only in directions taken from a subspace of finite codimension, chosen after the center is fixed. Two such notions are compared here. Asymptotic uniform convexity (AUC) asks for growth of $\|x+ty\|$ in every far-out unit direction $y$; asymptotic midpoint uniform convexity (AMUC) asks only that the average of $\|x+ty\|$ and $\|x-ty\|$ grows. These properties control nonlinear embeddings (for instance of countably branching diamond graphs) and are standard tools in the asymptotic geometry of Banach spaces.

Dilworth, Kutzarova, Randrianarivony, Revalski and Zhivkov (2016) asked whether AMUC and AUC are equivalent up to renorming. Baudier (2026) answered no, using subspaces of $L^1$ whose unit ball is compact in measure and the Daugavet-property example of Kadets and Werner. This mission asks for the exact values of both moduli in that setting.

Timeline

• 1980. Bourgain and Rosenthal construct a subspace of $L^1$ whose unit ball is relatively compact in measure but which fails the Radon–Nikodym property (doi:10.1007/BF02762868).
• 1983. Brézis and Lieb prove their splitting identity for pointwise convergent sequences in $L^p$ (doi:10.1090/S0002-9939-1983-0699419-3).
• 2000. Kadets, Shvidkoy, Sirotkin and Werner give the slice characterization of the Daugavet property (arXiv:math/9709216); Shvydkoy gives its weak-open form (doi:10.1006/jfan.2000.3626).
• 2004. Kadets and Werner refine the Bourgain–Rosenthal construction to obtain a space with the Schur and Daugavet properties (doi:10.1090/S0002-9939-03-07278-2).
• 2016. Dilworth et al. introduce AMUC and ask whether it is equivalent to AUC up to renorming (doi:10.1016/j.jmaa.2015.11.061).
• 2026. Baudier proves AMUC for measure-compact subspaces of $L^1$ and deduces a negative answer via the Kadets–Werner space (arXiv:2609.21283).

The source of this mission is an OpenAI preprint dated September 27, 2026, which computes both moduli exactly.

Setting

All spaces are real. For a Banach space $X$ with norm $N$, let $\operatorname{cof}(X)$ be its closed linear subspaces of finite codimension. For $N(x)=1$ and $t>0$,

$$H_N(x,t)=\sup_{F\in\operatorname{cof}(X)}\ \inf_{\substack{y\in F\\ N(y)\ge1}}\Bigl(\frac{N(x+ty)+N(x-ty)}2-1\Bigr),\qquad D_N(x,t)=\sup_{F\in\operatorname{cof}(X)}\ \inf_{\substack{y\in F\\ N(y)=1}}\bigl(N(x+ty)-1\bigr).$$

The averaged midpoint modulus $\widehat\delta_N(t)$ and the one-sided modulus $\overline\delta_N(t)$ are the infima of $H_N(x,t)$ and $D_N(x,t)$ over unit $x$. $N$ is AUC if $\overline\delta_N(t)>0$ for all $t>0$. A norm $N$ is equivalent to $\|\cdot\|$ if $a\|x\|\le N(x)\le b\|x\|$ with $a,b>0$.

A space has the Daugavet property if $\|I+T\|=1+\|T\|$ for every rank-one bounded operator $T$. On a probability space $(\Omega,\mathbb P)$, convergence in measure is given by the metric

$$d(f,g)=\inf\{a>0:\ \mathbb P(|f-g|>a)<a\}.$$

A set is totally bounded in measure if for each $\varepsilon>0$ it is covered by finitely many $d$-balls of radius $\varepsilon$.

Formalization targets

Goal: Theorem 1.1

Let $E$ be an infinite-dimensional closed subspace of $L^1(\Omega,\mathbb P)$, $\mathbb P$ a probability measure, whose unit ball is totally bounded in measure and whose norm has the Daugavet property. Then for every unit $x\in E$ and $t>0$

$$H_E(x,t)=\max\{t/2,\ t-1\},\qquad D_E(x,t)=\max\{0,\ t-2\},$$

so $\widehat\delta_E(t)=\max\{t/2,t-1\}$ and $\overline\delta_E(t)=\max\{0,t-2\}$, and $E$ admits no equivalent AUC norm. Lean: OAI.ExactModuli.exact_main (open on the platform).

Milestone: Theorem 6.1 (Kadets–Werner construction)

On $([0,1]^{\mathbb N},\lambda^{\mathbb N})$ there is an infinite-dimensional closed subspace $E\subseteq L^1$ whose unit ball is totally bounded in measure and which has the Daugavet slice property. Lean: OAI.ExactModuli.kadets_werner_existence. The proposal also carries OAI.ExactModuli.exact_example, the combination of the two theorems for this space.

Significance

The formulas show how far apart the two moduli can be: the averaged modulus grows linearly from $0$, while the one-sided modulus vanishes on the whole interval $(0,2]$. They refine Baudier's qualitative AMUC statement and linear lower bound into exact curves at every unit center, and the renorming clause shows that no equivalent norm can repair the one-sided modulus. Together with Theorem 6.1, they give a concrete space realizing the separation.

The results are proved in an OpenAI preprint; they have not been peer reviewed, and no machine-checked proof exists. The Daugavet slice characterization, Bourgain's lemma on slices and weak neighborhoods (Lemma 3.2), and the construction itself are reusable pieces of Banach space theory that a formalization would supply.

Difficulty

The lower bound for $H_E$ must hold uniformly over all directions in some finite-codimensional subspace, while the hypothesis only says that the unit ball is compact in a weak metric. A compactness argument along subsequences (Baudier's route via Brézis–Lieb) gives positivity but not the exact constant. The upper bounds need directions in a prescribed finite-codimensional subspace that are almost at distance $2$ from $x$; the Daugavet property supplies such vectors only in weak neighborhoods, and they must then be corrected into the subspace. The renorming clause must handle an arbitrary equivalent norm, for which neither formula is available.

Formalization scope

• Cofinite F is a closed submodule with finite-dimensional quotient. H, D, averagedModulus, oneSidedModulus follow the displayed sup/inf order; H ranges over $N(y)\ge1$, D over $N(y)=1$.
• EquivalentNorm N is a Seminorm with two-sided comparison constants $a,b>0$; AUC N is positivity of oneSidedModulus N t for every $t>0$.
• Daugavet X quantifies over rank-one operators written as ell.smulRight v.
• measureDistance is the metric $d$ on Lp ℝ 1 μ; MeasurePrecompactBall μ E requires finite $\varepsilon$-nets (centers in $L^1$) of the unit ball of $E$; μ is a probability measure.
• kwMeasure is the product of Lebesgue measures on $\mathbb N\to[0,1]$.
• The moduli are real-valued sSup/sInf; for infinite-dimensional $E$ the relevant sets are nonempty and bounded, so the junk values are not used.

A full development needs the Daugavet slice characterization (Lemma 3.1), Bourgain's lemma (Lemma 3.2), the weak-neighborhood diameter-two property (Lemma 3.3), $L^1$ truncation estimates, and the Kadets–Werner iteration (Lemmas 6.2–6.3). Formalizations of these lemmas are welcome.

Selected references

• OpenAI, Exact asymptotic moduli in a Daugavet subspace of $L^1$, preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Exact-asymptotic-moduli-in-a-Daugavet-subspace-of-L1-September-27-2026/manuscript.pdf
• F. P. Baudier, The Kadets–Werner modification of Bourgain–Rosenthal space is asymptotically midpoint uniformly convex, preprint, 2026. https://arxiv.org/abs/2609.21283
• S. J. Dilworth, D. Kutzarova, N. L. Randrianarivony, J. P. Revalski, N. V. Zhivkov, Lenses and asymptotic midpoint uniform convexity, J. Math. Anal. Appl., 2016. https://doi.org/10.1016/j.jmaa.2015.11.061
• V. Kadets, D. Werner, A Banach space with the Schur and the Daugavet property, Proc. Amer. Math. Soc., 2004. https://doi.org/10.1090/S0002-9939-03-07278-2
• J. Bourgain, H. P. Rosenthal, Martingales valued in certain subspaces of $L^1$, Israel J. Math., 1980. https://doi.org/10.1007/BF02762868
• V. M. Kadets, R. V. Shvidkoy, G. G. Sirotkin, D. Werner, Banach spaces with the Daugavet property, Trans. Amer. Math. Soc., 2000. https://arxiv.org/abs/math/9709216
• R. V. Shvydkoy, Geometric aspects of the Daugavet property, J. Funct. Anal., 2000. https://doi.org/10.1006/jfan.2000.3626
• H. Brézis, E. Lieb, A relation between pointwise convergence of functions and convergence of functionals, Proc. Amer. Math. Soc., 1983. https://doi.org/10.1090/S0002-9939-1983-0699419-3