Functional Analysis

Motivation

A norm measures the size of a vector. The triangle inequality says that adding two vectors cannot increase their size beyond the sum of their sizes. The Hlawka constant problem asks for a quantitative comparison between the deficit in a three-vector triangle inequality and the sum of the deficits in the three two-vector inequalities. For operator norms, the comparison constant must work in every matrix dimension. Audenaert and Kittaneh state this question in Section 8.2, Problem 7 of Problems and Conjectures in Matrix and Operator Inequalities.

This mission concerns the diagonal, or commuting, case. For a complex diagonal matrix, its Schatten p-norm equals the coordinate p-norm of its diagonal. An exact answer in this setting identifies a concrete extremal family while preserving the requirement that the constant work in every finite dimension. It does not settle the sharp constant for arbitrary noncommuting matrices.

The foundation mission formalizes the cyclic formula for real exponents at least 256. The accepted cutoff-32 theorem, recorded on 16 October 2026, lowers that threshold. The present source is Yuxuan Xu's AI-assisted research preprint, which supplies a computer-assisted argument extending the formula to all real exponents at least 21. The preprint has not undergone independent analytic review. Its new interval has numerical verification reports but no Lean proof.

Setting

For a real exponent p greater than one and a finite complex vector x, define the coordinate p-norm by

$$N_p(x)=\left(\sum_i |x_i|^p\right)^{1/p}.$$

For three vectors x, y, and z in the same dimension, set

$$S=N_p(x)+N_p(y)+N_p(z),\qquad T=N_p(x+y+z),$$ $$P=N_p(x+y)+N_p(x+z)+N_p(y+z),\qquad G=2S-P.$$

The quantity S minus T is the triple deficit. The quantity G is the sum of the three pair deficits and is nonnegative by the triangle inequality. A real number C is a uniform Hlawka constant when

$$S-T\le C G$$

for all triples and all finite complex dimensions. No equal-norm or nonzero-vector restriction is part of this property.

The candidate sharp constant is specified by an explicit scalar formula. For a real parameter t in the closed interval from one half to two, let

$$A_p(t)=(t^p+2)^{1/p},\qquad B_p(t)=(2|1-t|^p+2^p)^{1/p},$$ $$R_p(t)=\frac{3A_p(t)-3^{1/p}|2-t|}{6A_p(t)-3B_p(t)},\qquad K_p=\sup_{1/2\le t\le2}R_p(t).$$

The ratio comes from the cyclic triple (-t,1,1), (1,-t,1), and (1,1,-t). In the exponent range of the mission its denominator is positive, and continuity makes the supremum an attained maximum. The mission imports the campaign's existing definitions of these quantities.

Formalization targets

The goal is Theorem 1.1 of the source preprint, in the campaign's exact statement format:

$$\forall p\in\mathbb R,\quad 21\le p\ \Longrightarrow\ K_p=\min\{C\in\mathbb R:\ \forall n\in\mathbb N,\ S-T\le C G\text{ on }\mathbb C^n\}.$$

Here the minimum notation includes both admissibility and leastness; existence of an admissible constant is part of the conclusion. The theorem does not assume that certificate validation, localization, or convexity already holds. It does not assert that 21 is the smallest possible exponent threshold.

Four supporting targets follow the source's two finite windows. Equation (7) and Table 1 give, on each full real interval, the scalar inequalities

$$cp<K_p\le p/2,\qquad E_p(q)<K_p,\qquad E_p(q)=\frac{1-q}{2\left(1-((1+q^p)/2)^{1/p}\right)}.$$

Window I is [21,26], with c=273/625 and q=1011/2500. Window II is [26,32], with c=443/1000 and q=197/500. Two further targets are the unconditional real three-dimensional Hlawka inequalities on these respective windows, as concluded in Section 7 of the source. The previously proved tail for p at least 32 is included as a referenced theorem, preserving its published identity and attribution.

Significance

The proposed result would extend the known formalized range of the exact diagonal constant from p at least 32 to p at least 21. It would give one constant simultaneously for all complex dimensions and for all real exponents in that range, rather than separate statements at selected integer exponents. The cyclic witnesses also explain the obstruction to decreasing the constant itself.

Formalizing this source means closing the gap between its analytic argument and its finite computations. The release replay report records exact rational linear-dual replay and directed interval checks. Those reports support the paper's computer-assisted claim; they are not kernel-checked proofs of the mission's open statements. A completed mission must establish those statements in the platform's ordinary proof system.

Difficulty

The least constant is defined through a special three-dimensional family, but admissibility quantifies over arbitrary triples in arbitrary dimensions. Unequal singleton norms and degenerate triples are included. Arguments that verify only the cyclic family establish a lower bound and leave the main admissibility assertion unresolved.

The source also requires inequalities uniform in a continuously varying real exponent. Pointwise numerical optimization and dense sampling cannot establish such interval statements. Its localized convexity estimates retain norm bounds and linear coordinate-sum constraints; each retained constraint must genuinely follow from the preceding localization argument, and the averaging domain must remain convex. In particular, retaining a norm-sum equality as if it defined a convex domain would not justify the required averaging step. These issues are part of the formalization target, not additional assumptions supplied to solvers.

Formalization scope

The environment is Mathlib commit 0df444a360eaa60ab8c11dca51a86af692955474, using Lean v4.33.1. The goal uses Fin n → ℂ, real p, the existing lpNorm, cyclicConstant, and HasHlawkaConstant, and IsLeast over real constants. Natural-number dimensions include zero. In dimension zero all coordinate norms vanish, so the inequality is harmless; triples containing zero vectors remain included in positive dimensions. All quantities must retain their foundation definitions.

The four new milestone declarations use the same scalar and coordinate definitions, including the existing scalarEnvelope. They introduce no replacement norm and no axiom saying that an external Python execution is correct. The source package contains exact certificates, two arithmetic implementations, and explicit remainder estimates for its rational interval backend. Those implementations share the mathematical model and are not independent end-to-end proofs. Independent analytic review remains pending.

Contributions may reuse the existing dimension reduction, complex transfer, cyclic sharpness, and cutoff-32 results when their hypotheses match the target range. Formalization of the new scalar bounds, exact linear-dual implications, interval arithmetic soundness, and real three-dimensional admissibility is welcome. Proof details and the proposed dependency order are available in the source paper and the milestone descriptions. The declarations uploaded with this proposal are statements to prove, with the standard by sorry placeholders; compiling them checks well-formedness only.

Selected references

• Yuxuan Xu (徐宇轩), School of Computer Science, Wuhan University, A computer-assisted sharp diagonal Hlawka inequality for real exponents p ≥ 21, research preprint, v1 (2026). PDF, LaTeX, certificates and code. AI assistance is disclosed in the paper.
• K. M. R. Audenaert and F. Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, arXiv:1201.5232v3 (2012), Section 8.2, Problem 7. Source.
• D.-Ş. Marinescu and C. P. Niculescu, A survey of the Hornich–Hlawka inequality, arXiv:2407.03278 (2024). Source.
• Ezzeri Esa / savarin and contributors, Dimension-independent Hlawka constants for Schatten norms, Lean source repository (2026). Repository.
• Prove2Me contributors, including @bwdaugherty, Sharp diagonal Hlawka constant: cutoff 32 (2026). Accepted theorem, campaign. Exact source identifiers and hashes are preserved in the paper repository's provenance record.

Motivation

A metric space is plastic if every nonexpansive bijection of it onto itself is an isometry. Every totally bounded metric space is plastic (Freudenthal–Hurewicz 1936; the term is from Naimpally–Piotrowski–Wingler 2006), and Cascales, Kadets, Orihuela and Wingler (2016) asked whether the closed unit ball of every real Banach space is plastic. The answer is known to be yes for strictly convex spaces (CKOW 2016), for ℓ₁ and ℓ₁-sums of strictly convex spaces (Kadets–Zavarzina 2016, 2018), for finite ℓ∞-sums of strictly convex spaces (Haller–Leo–Zavarzina 2022 for two summands; Kurik 2025 under an extra hypothesis), and for c and for c₀ under continuity of the inverse (Leo 2022), among others; it is open for L¹[0,1] and C[0,1].

A recurring step in these proofs is to show that the map preserves the unit sphere and then that a sphere-preserving map is linear. The published versions of the second step assume homogeneity on rays, or oddness, in addition to sphere preservation (CKOW 2016, Lemma 2.5; Zavarzina 2018, Corollary 2.6; Kadets–Zavarzina 2018, Lemma 2.9). This mission formalizes a version that needs only sphere preservation, together with a strengthening in which surjectivity onto the ball is replaced by coverage of the target sphere. The results come from an unpublished research project on the plasticity problem.

Setting

$X$ and $Y$ are real Banach spaces, $B_X=\{x\in X:\|x\|\le1\}$ and $S_X=\{x\in X:\|x\|=1\}$. A map $F\colon B_X\to B_Y$ is nonexpansive if $\|F(x)-F(x')\|\le\|x-x'\|$ for all $x,x'\in B_X$. In Lean a map of balls is a function F : X → Y on the whole space, constrained on the ball by Set.MapsTo, Set.SurjOn and LipschitzOnWith 1; its values outside $B_X$ play no role.

Target

The goal and its milestones, from the most special tool to the strongest statement:

$$\text{(A01)}\quad H\colon B_X\to B_X \text{ nonexpansive},\ \|a+H(a)\|=2\ \ \forall a\in S_X\ \Longrightarrow\ H=\mathrm{id}_{B_X}.$$ $$\text{(A01, quantitative)}\quad H\colon B_X\to B_X\ (1+\varepsilon)\text{-Lipschitz},\ \|a+H(a)\|=2\ \ \forall a\in S_X\ \Longrightarrow\ \sup_{x\in B_X}\|H(x)-x\|\le\min\{2,4\varepsilon^{1/3}\}.$$ $$\text{(U10)}\quad F\colon B_X\to B_Y \text{ nonexpansive and onto},\ F(S_X)\subseteq S_Y\ \Longrightarrow\ F=T|_{B_X}\ \text{for a surjective linear isometry } T\colon X\to Y.$$ $$\text{(U16, goal)}\quad F\colon B_X\to B_Y \text{ nonexpansive},\ F(S_X)\subseteq S_Y\subseteq F(B_X)\ \Longrightarrow\ F=T|_{B_X}\ \text{for a surjective linear isometry } T.$$

In U10 and U16, $X$ and $Y$ are nonzero.

Significance

The result. U10 reduces the plasticity problem in every real Banach space to sphere preservation, and U16 to coverage of the target sphere by the image of the sphere; the reductions hold between two different spaces, which matters because the plasticity problem is equivalent to its two-space form (Kurik 2025, Theorem 3.1). They also show that sphere preservation, preservation of every norm, and being an isometry are equivalent for nonexpansive surjections of unit balls.

Formalizing it. The proofs exist only in the project's own notes and have been checked by AI referees and partly by the author; a machine-checked proof is the independent confirmation sought. Mathlib has no theory of nonexpansive or averaged maps, so the development will contribute uniform asymptotic regularity of averaged nonexpansive maps (Borzdyński–Wiśnicki; Goebel–Kirk 1990, Theorem 9.4), U16 needs the Bishop–Phelps theorem, which Mathlib also lacks, and the quantitative form of A01 needs the sharp rate of Cominetti, Soto and Vaisman for averaged maps (arXiv:1206.4195, Theorem 1); it is not needed for U10 or U16.

Difficulty

No injectivity, oddness, homogeneity, smoothness or continuity of an inverse is assumed, so none of the standard routes to linearity applies: Mazur–Ulam needs an isometry, and the published sphere-preservation lemmas need homogeneity on rays. In U16 the map need not even be onto the ball.

Formalization scope

Real scalars; arbitrary (not necessarily separable) Banach spaces, with CompleteSpace and, in U10 and U16, Nontrivial. The conclusion of U10 and U16 is a LinearIsometryEquiv agreeing with F on the closed unit ball, so it includes surjectivity of the linear map. A01 concludes Set.EqOn H id on the closed unit ball. Statements are not to be weakened by adding injectivity, continuity of an inverse, or finite dimension. Published inputs (Goebel–Kirk, Bishop–Phelps, Banach's fixed-point theorem from Mathlib) may be added as separate cards and imported by proof sketches.

Selected references

• B. Cascales, V. Kadets, J. Orihuela, E. J. Wingler, Plasticity of the unit ball of a strictly convex Banach space, RACSAM 110 (2016), 723–727.
• S. A. Naimpally, Z. Piotrowski, E. J. Wingler, Plasticity in metric spaces, J. Math. Anal. Appl. 313 (2006), 38–48.
• O. Zavarzina, Non-expansive bijections between unit balls of Banach spaces, Ann. Funct. Anal. 9 (2018), arXiv:1704.06961.
• V. Kadets, O. Zavarzina, Nonexpansive bijections to the unit ball of the ℓ₁-sum of strictly convex Banach spaces, Bull. Aust. Math. Soc. 97 (2018), arXiv:1711.00262.
• N. Leo, Plasticity of the unit ball of c and c₀, J. Math. Anal. Appl. 507 (2022), arXiv:2106.06276.
• R. Haller, N. Leo, O. Zavarzina, Two new examples of Banach spaces with a plastic unit ball, Acta Comment. Univ. Tartu. Math. 26 (2022), arXiv:2111.10122.
• K. A. Kurik, Conditional plasticity of the unit ball of the ℓ∞-sum of finitely many strictly convex Banach spaces, J. Math. Anal. Appl. 541 (2025), arXiv:2403.09245.
• H. Freudenthal, W. Hurewicz, Dehnungen, Verkürzungen, Isometrien, Fund. Math. 26 (1936), 120–122.
• S. Borzdyński, A. Wiśnicki, arXiv:1511.04069, Proposition 2.2, Lemma 3.1, Theorem 3.3.
• K. Goebel, W. A. Kirk, Topics in Metric Fixed Point Theory, Cambridge University Press, 1990, Theorem 9.4.
• E. Bishop, R. R. Phelps, A proof that every Banach space is subreflexive, Bull. Amer. Math. Soc. 67 (1961), 97–98.

The Hlawka inequality for Schatten $p$-norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. The question is how large a comparison constant is needed to make this inequality hold.

This mission asks whether the best possible constant for complex diagonal matrices, already proved in Lean for every real $p\ge62$, also holds for every real $p\ge50$. This is an open problem: no proof is known, and the technique that reached 62 cannot go further. The constant is the one from the foundation mission: the largest comparison constant required by the cyclic family of three $3\times3$ diagonal matrices. Because the cutoff-62 mission already covers every $p\ge62$, the new work is the range from 50 to 62.

The cutoff came down from 256 to 62 across nine missions. The step from 90 to 80 used a weighted pair-curvature and confinement estimate introduced by moona3k, and further refinement pushed it from 80 through 70 to 62. The confinement method is now exhausted: at $p=61$, every confinement radius whose tangent model stays positive already makes the budget-7 box factor larger than 1. Reaching 50 requires a fundamentally new idea. The goal theorem below gives the exact statement.

This is an entry in the sharp diagonal Hlawka campaign, which asks for the smallest cutoff at which the same formula holds. Any proof for a cutoff of 50 or lower also settles this mission.

The broader question of optimal constants for Schatten norms appears in Audenaert and Kittaneh's Problem 7. Extending the sharp diagonal constant to general matrices is a separate challenge.

References

• K. M. R. Audenaert and F. Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, arXiv preprint, 2012, §8.2, Problem 7. arXiv:1201.5232
• Ezzeri Esa, Hlawka–Schatten inequalities: sharp diagonal construction, Lean source repository, 2026, revision 79aa498bfcf7b22bd91d771fb32ec278e2d4704b. Source library
• Ezzeri Esa and project contributors, The cyclic bound for every real p ≥ 90, research note with appendices and exact certificates, 2026. Research note

Established results on Prove2Me

• The accepted sharp diagonal bound for every real p ≥ 62.
• The accepted real coordinate bound for every real p ≥ 62.
• The accepted diagonal Schatten norm identity.

Motivation

Quantum mechanics represents the states of a system by unit vectors (normed rays) of a complex Hilbert space $\mathcal H$ and its observables by self-adjoint operators on $\mathcal H$. The most important observables — position, momentum, energy — are unbounded. A. Heathcote's paper Unbounded Operators and the Incompleteness of Quantum Mechanics (Philosophy of Science 57, 1990, 523–534) draws attention to a mathematical fact that is routinely glossed over in physical texts: an unbounded self-adjoint operator cannot be defined on all of $\mathcal H$, and there are concrete normalized wave functions on which the position and momentum operators do not act at all. The paper uses this to argue that the standard postulates of quantum mechanics are, in a precise sense, incomplete.

This mission isolates the mathematical content of that argument, which is a clean and checkable piece of functional analysis on $L^2(\mathbb R)$.

Setting

Let $\mathcal H$ be a complex Hilbert space. A (partially defined) linear operator $A$ has a domain $D(A)\subseteq\mathcal H$; it is bounded if there is $k\in\mathbb R$ with $\|A\psi\|\le k\|\psi\|$ for all $\psi\in D(A)$, and unbounded otherwise. It is self-adjoint if it equals its Hilbert adjoint, $A=A^*$, which includes $D(A)=D(A^*)$.

On $\mathcal H=L^2(\mathbb R)$:

1. The position operator acts by $(Q\psi)(x)=x\,\psi(x)$ on

$$D(Q)=\Big\{\psi\in L^2(\mathbb R): \int_{\mathbb R}x^2|\psi(x)|^2\,dx<\infty\Big\}\qquad\text{(eq. (3))}.$$

2. The momentum operator $P\psi=\hbar i^{-1}\,d\psi/dx$ has, in the paper's description, domain $D(P)$ consisting of the absolutely continuous functions in $L^2(\mathbb R)$.
3. Heathcote's wave function (eq. (4)) is

$$\psi(x)=\begin{cases}x^{-1}, & x\ge 1,\\ 0, & x<1.\end{cases}$$

Formalization targets

Goal

There is a unit vector of $L^2(\mathbb R)$, namely the class of $\psi$, lying in neither domain:

$$\exists\,\varphi\in L^2(\mathbb R):\quad \varphi=\psi\ \text{a.e.},\qquad \|\varphi\|=1,\qquad \varphi\notin D(Q),\qquad \varphi\notin D(P).$$

Milestones

1. Hellinger–Toeplitz (p. 2, footnote 1): a symmetric operator defined on all of a Hilbert space is bounded (an existing platform theorem).
2. Unbounded self-adjoint operators (p. 2, footnote 2): if $A=A^*$ is unbounded then $D(A)$ is dense and $D(A)\neq\mathcal H$.
3. Normalization (p. 5): $\psi\in L^2(\mathbb R)$ and $\int|\psi|^2=\int_1^\infty x^{-2}dx=1$.
4. Not in $D(Q)$ (p. 5): $\int x^2|\psi(x)|^2dx=\infty$.
5. Not in $D(P)$ (pp. 5–6): no a.e.-representative of $\psi$ is absolutely continuous on every compact interval.
6. Infinite position expectation (p. 9): $\int|x|\,|\psi(x)|^2dx=\int_1^\infty x^{-1}dx=\infty$.

Significance

The result. The goal shows that the two postulates "every normed ray is a state" and "observables are self-adjoint operators" force the existence of states on which the position operator (and, independently, the momentum operator) is undefined. Milestone 5 is what the paper uses to separate this phenomenon from the canonical commutation relations: the failure of $\psi\in D(Q)$ is not explained by $\psi$ being "sharp in momentum", because $\psi$ is not even in $D(P)$. Milestone 6 records the physical reading: the mean position of this normalized state is infinite.

Formalizing it. The individual facts are standard and elementary; none of them is new. What the mission produces is a machine-checked version of the paper's argument stated against the actual $L^2$ space and Mathlib's notion of unbounded operators and adjoints, with the domain conventions made explicit.

Difficulty

The calculus is easy; the subtleties are in the bookkeeping. Elements of $L^2(\mathbb R)$ are almost-everywhere classes, so "$\psi$ is discontinuous at $1$" does not by itself show $\psi\notin D(P)$: one must rule out every a.e.-modification of $\psi$ being absolutely continuous. Similarly, the Hellinger–Toeplitz argument gives $D(A)\neq\mathcal H$ but not density, which comes from the adjoint being a genuine operator.

Formalization scope

• Operators are Mathlib's partially defined linear maps H →ₗ.[ℂ] H; self-adjointness is IsSelfAdjoint with respect to the adjoint A†, over a complex complete inner product space.
• $L^2(\mathbb R)$ is Lp ℂ 2 volume on ℝ; $D(Q)$ and $D(P)$ are subsets of it. Integrals of non-negative quantities are Lebesgue integrals valued in $[0,\infty]$, so "$=\infty$" is literal and not a junk value.
• $D(P)$ follows the paper (absolutely continuous elements, i.e. having a representative absolutely continuous on every $[a,b]$) and omits the standard requirement $\psi'\in L^2$. This set contains the standard domain, so non-membership is a stronger statement.
• The paper's further claim that $\psi\notin D(H)$ for a Hamiltonian $H=P^2/2m+V$ is stated there without proof and for an unspecified potential $V$, and is not included.
• Trivialization is excluded: the goal pins $\varphi$ to the explicit function $\psi$ and requires $\|\varphi\|=1$.

Selected references

• A. Heathcote, Unbounded Operators and the Incompleteness of Quantum Mechanics, Philosophy of Science 57 (1990), 523–534.
• M. Reed and B. Simon, Methods of Modern Mathematical Physics I: Functional Analysis, revised ed., Academic Press, 1980.

Why projection methods for variational inequalities

A variational inequality asks for a point of a convex set at which a vector field points "inward" against every feasible direction. It is the common form of convex minimization (with $F$ a gradient), of saddle-point problems (with $F$ the monotone operator of a convex–concave function), of Nash equilibria of convex games, of complementarity problems and of traffic and economic equilibria. Iterative methods that use only evaluations of $F$ and projections onto the feasible set are the methods of choice when the problem is large, because each step is cheap.

The classical such method, the projected gradient iteration $x_{n+1}=P_C(x_n-\lambda F(x_n))$, does not converge for merely monotone $F$. Korpelevich's extragradient method (1976) does, at the price of two projections and two evaluations of $F$ per step, and it is known to converge R-linearly under strong monotonicity (Tseng 1995, reference [19] of the paper). Popov (1980), Tseng (2000) and Censor–Gibali–Reich (2011) reduced the number of projections or evaluations. Yu. Malitsky's projected reflected gradient method (arXiv:1502.04968, SIAM J. Optim. 25(1), 2015, doi:10.1137/14097238X) uses one projection and one evaluation of $F$ per step, evaluating $F$ at the reflected point $2x_n-x_{n-1}$ instead of at $x_n$. This mission formalizes the paper's second main result: under strong monotonicity the method keeps the R-linear rate of the extragradient method.

Setting

Let $H$ be a real Hilbert space with inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$, let $C\subseteq H$ be closed and convex, and let $F:H\to H$. The metric projection $P_C(z)$ is the unique point of $C$ nearest to $z$. The variational inequality (1.1) is

$$\text{find } x^*\in C\ \text{ such that }\ \langle F(x^*),\,x-x^*\rangle\ \ge\ 0\quad\text{for all } x\in C,$$

with solution set $S$. The paper's standing assumptions for this result are

• (C1) $S\neq\emptyset$;
• (C2*) $F$ is strongly monotone with modulus $m>0$: $\langle F(x)-F(y),x-y\rangle\ge m\|x-y\|^2$ for all $x,y\in H$;
• (C3) $F$ is Lipschitz with constant $L>0$: $\|F(x)-F(y)\|\le L\|x-y\|$ for all $x,y\in H$.

Algorithm 3.1 chooses $x_0=y_0\in H$ and a step $\lambda\in\big(0,(\sqrt2-1)/L\big)$ and iterates

$$x_{n+1}=P_C\big(x_n-\lambda F(y_n)\big),\qquad y_{n+1}=2x_{n+1}-x_n .$$

The Lean development names these objects proj, solSet, IsStronglyMonotoneMap, IsLipschitzMap and IsPRGRun in the namespace ProjReflGrad.Linear.

Formalization targets

Goal: Theorem 3.3 (p. 6)

Under (C1), (C2*), (C3) and $0<\lambda<(\sqrt2-1)/L$, every run of Algorithm 3.1 converges to the solution $z$ of (1.1) at least R-linearly:

$$\exists\,\gamma\in(0,1),\ M>0:\qquad \|x_n-z\|\ \le\ M\gamma^n\quad\text{for all } n\ge0 .$$

The goal fixes neither $\gamma$ nor $M$; the proof produces them from $\lambda$, $L$ and $m$, but the theorem asserts only the shape of the rate.

Milestones

In attack order:

1. Uniqueness (p. 6): under (C2*) the solution set has at most one point.
2. The identity for $\|y_n-z\|^2$ (p. 6, via Lemma 2.5): $\|y_n-z\|^2=2\|x_n-z\|^2-\|x_{n-1}-z\|^2+2\|x_n-x_{n-1}\|^2\ge2\|x_n-z\|^2-\|x_{n-1}-z\|^2$.
3. (3.8) (p. 7): the strong-monotonicity estimate at $y_n$ with a free modulus $m_1\in(0,m]$.
4. (3.2) (p. 4): $\|x_{n+1}-z\|^2\le\|x_n-z\|^2-\|x_{n+1}-x_n\|^2-2\lambda\langle F(y_n),x_{n+1}-z\rangle$.
5. (3.4) (p. 5): $2\lambda\langle F(y_{n-1}),y_n-x_{n+1}\rangle\le\|x_{n+1}-x_n\|^2-\|x_n-y_n\|^2-\|x_{n+1}-y_n\|^2$, $n\ge2$.
6. (3.5) (p. 5): the Lipschitz estimate of $2\lambda\langle F(y_n)-F(y_{n-1}),y_n-x_{n+1}\rangle$.
7. (3.9) (p. 7): the two-step recursion $a_{n+1}+b_{n+1}\le(1-2\alpha)a_n+\alpha a_{n-1}+\beta b_n$ in the iterates, with $\beta=\max\{\lambda L/(1-\sqrt2\lambda L),\tfrac12\}$.
8. Lemma 2.8 (p. 3): a nonnegative pair of sequences satisfying that recursion for all $\alpha\in(0,\alpha_0)$ has $a_n\le\gamma^nM$.

Significance

The result. Theorem 3.3 shows that halving the per-step cost of the extragradient method does not cost the linear rate under strong monotonicity. For strongly monotone problems (strongly convex minimization, strongly convex–strongly concave saddle points, strictly monotone games with a quadratic margin) the method therefore reaches accuracy $\varepsilon$ in $O(\log(1/\varepsilon))$ iterations with one projection each, which matters when projecting onto $C$ dominates the cost. The two-step recursion (3.9) and Lemma 2.8 are also a reusable template: the same mechanism gives linear rates for other methods with a memory of one past iterate.

Formalizing it. The theorem is proved in the paper; nothing here is open. No machine-checked proof of it, or of its lemmas, is on the platform. A formal proof needs the projection inequality in a general real Hilbert space, a careful account of the reflected iterate, and a rigorous version of Lemma 2.8, whose printed proof leaves the range of $n$ and the positivity of $M$ implicit. The deliverable is a checked R-linear rate for a one-projection method in infinite dimension.

Difficulty

The natural first attempt, a contraction $\|x_{n+1}-z\|\le q\|x_n-z\|$ (Q-linear convergence), is not what the paper proves and is not available: the reflected point $y_n$ depends on $x_{n-1}$, so the error at step $n+1$ is controlled only by the errors at steps $n$ and $n-1$, together with auxiliary terms $\|x_n-y_{n-1}\|^2$ and $\langle F(z),x_{n-1}-z\rangle$. Strong monotonicity is applied at $y_n$, not at $x_n$, and $\|y_n-z\|^2$ can be smaller than $\|x_n-z\|^2$; the lower bound $2\|x_n-z\|^2-\|x_{n-1}-z\|^2$ may even be negative. The step range $\lambda<(\sqrt2-1)/L$ is exactly what keeps the coefficients of the Lipschitz error terms below the gain from the projection inequality, and the resulting two-step recursion needs Lemma 2.8, with its choice of $\gamma$ and $\delta$, to yield a geometric bound.

Formalization scope

• $H$ is a general real inner product space, complete where a projection is used ([CompleteSpace H]); it is never specialized to $\mathbb R^n$.
• $P_C$ is defined by choice as a nearest point, returning its argument when none exists; every statement using it assumes $C$ closed, convex and nonempty (through $z\in C$, $C\neq\emptyset$, or (C1)), so the junk value is never reached.
• Runs of Algorithm 3.1 are infinite sequences without the stopping rule; a stopped run continues as a constant sequence. $x_0$ is any point of $H$, as in the paper, so statements that need $x_{n-1}\in C$ are stated for $n\ge2$.
• (C2*) and (C3) are required on all of $H$ with real constants $m>0$, $L>0$ (not LipschitzWith, whose $\mathbb R_{\ge0}$ constant admits $L=0$). (C1) stays in the goal: it is the paper's assumption and its only source of $C\neq\emptyset$.
• R-linear convergence means domination by $M\gamma^n$ with $0<\gamma<1$ and $M>0$; a goal allowing $\gamma=1$, $\gamma=0$ or only an $O(\cdot)$ bound would be a different and weaker (or trivially false) statement and is ruled out. The goal does not mention the auxiliary sequences $a_n,b_n$, the constants $\beta,m_1,\alpha_0$, or Lemma 2.8.
• Departures from the page are recorded in each item's Formalization Note: the ranges $n\ge1$/$n\ge2$, the range $n\ge1$ of (2.1) in Lemma 2.8, the proof's "Lemma 2.1" that means Lemma 2.8, and "$m_1$ arbitrary in $(0,m)$" where the argument uses $(0,m]$.
• The projection theorem (existence and characterization of the nearest point) is the published Proved theorem VectorSpaceOpt.min_distance_convex_set, included as a reference. Contributions welcome: proofs of the milestones in any order; Lemma 2.8 and the identity of milestone 2 are self-contained.

Selected references

• Yu. Malitsky, Projected Reflected Gradient Methods for Monotone Variational Inequalities, SIAM J. Optim. 25(1), 2015. arXiv:1502.04968v1. https://arxiv.org/abs/1502.04968 , https://doi.org/10.1137/14097238X
• G. M. Korpelevich, The extragradient method for finding saddle points and other problems, Ekonomika i Matematicheskie Metody 12, 747–756, 1976.
• P. Tseng, On linear convergence of iterative methods for the variational inequality problem, J. Comput. Appl. Math. 60, 237–252, 1995.
• L. D. Popov, A modification of the Arrow–Hurwicz method for finding saddle points, Math. Notes 28, 845–848, 1980.
• Y. Censor, A. Gibali, S. Reich, The subgradient extragradient method for solving variational inequalities in Hilbert space, J. Optim. Theory Appl. 148, 318–335, 2011.

Motivation

Many problems in optimization, game theory and mechanics come down to a variational inequality: find a point of a convex set at which a given vector field points "inward" against every feasible direction. Constrained convex minimization (where the field is a gradient), saddle-point problems (where it is the gradient of a convex–concave function with one sign flipped), Nash equilibria of convex games and complementarity problems are all of this form. In large-scale and infinite-dimensional settings the methods of choice are projection methods, which use only evaluations of the field and projections onto the feasible set.

The plain projected gradient iteration $x_{n+1}=P_C(x_n-\lambda F(x_n))$ does not converge for merely monotone fields: on a rotation field in the plane it spirals outward for every step size. Korpelevich's extragradient method (1976) repairs this with two field evaluations and two projections per iteration. Later methods (Tseng's forward–backward–forward method, 2000; the subgradient extragradient method of Censor, Gibali and Reich, 2011) reduce the number of projections to one, but still need two evaluations of the field.

Yu. Malitsky's paper (arXiv:1502.04968, SIAM J. Optim. 25(1), 2015, doi:10.1137/14097238X) introduces the projected reflected gradient method, which uses one projection and one field evaluation per iteration, evaluated at a "reflected" point, and proves that it converges weakly under the same assumptions as the extragradient method. This mission formalizes that convergence theorem, Theorem 3.2 of the paper.

Setting

Let $H$ be a real Hilbert space with inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$. Let $C\subseteq H$ be closed and convex, and let $F:H\to H$ be a mapping. For $z\in H$, the metric projection $P_C(z)$ is the unique point of $C$ nearest to $z$ (it exists when $C$ is nonempty). The variational inequality (1.1) asks for $x^*\in C$ with

$$\langle F(x^*),\,x-x^*\rangle\ \ge\ 0\qquad\text{for all }x\in C,$$

and $S$ denotes its solution set. The standing assumptions are:

• (C1) $S$ is nonempty;
• (C2) $F$ is monotone: $\langle F(x)-F(y),x-y\rangle\ge0$ for all $x,y\in H$;
• (C3) $F$ is Lipschitz continuous with a constant $L>0$: $\|F(x)-F(y)\|\le L\|x-y\|$ for all $x,y\in H$.

Algorithm 3.1 (projected reflected gradient method). Fix a step size $\lambda\in\big(0,(\sqrt2-1)/L\big)$ and a starting point $x_0=y_0\in H$, and iterate

$$x_{n+1}=P_C\big(x_n-\lambda F(y_n)\big),\qquad y_{n+1}=2x_{n+1}-x_n .$$

The point $y_{n+1}$ is the reflection of $x_n$ through $x_{n+1}$. A sequence $(x_n)$ converges weakly to $x^*$, written $x_n\rightharpoonup x^*$, if $\langle x_n,v\rangle\to\langle x^*,v\rangle$ for every $v\in H$.

Formalization targets

Goal: Theorem 3.2 (p. 5)

Under (C1)–(C3), for $0<\lambda<(\sqrt2-1)/L$ and every run of Algorithm 3.1 there is $x^*\in S$ with

$$x_n\rightharpoonup x^* .$$

Milestones

In the order the proof uses them:

1. Lemma 2.1 (i), p. 3: $\langle P_Mx-x,\,y-P_Mx\rangle\ge0$ for $y\in M$ (already proved on the platform, referenced).
2. Lemma 2.1 (ii), p. 3: $\|P_Mx-y\|^2\le\|x-y\|^2-\|x-P_Mx\|^2$ for $y\in M$.
3. Lemma 3.1, p. 4: for $z\in S$ and $n\ge2$,

$$\|x_{n+1}-z\|^2\le\|x_n-z\|^2-\big(1-\lambda L(1+\sqrt2)\big)\|x_n-x_{n-1}\|^2+\lambda L\|x_n-y_{n-1}\|^2-\big(1-\sqrt2\lambda L\big)\|x_{n+1}-y_n\|^2-2\lambda\langle F(z),y_n-z\rangle .$$

4. (3.6), p. 5: the descent inequality $a_{n+1}\le a_n-b_n$ with $a_n=\|x_n-z\|^2+\lambda L\|x_n-y_{n-1}\|^2+2\lambda\langle F(z),x_{n-1}-z\rangle$ and $b_n=(1-\lambda L(1+\sqrt2))\|x_n-x_{n-1}\|^2$.
5. Lemma 2.7, p. 3: nonnegative sequences with $a_{n+1}\le a_n-b_n$ have $(a_n)$ bounded and $b_n\to0$.
6. Proof of Theorem 3.2, pp. 5–6: $(x_n)$ is bounded, $\|x_{n+1}-x_n\|\to0$ and $\|x_{n+1}-y_n\|\to0$.
7. Lemma 2.2 (Minty), p. 3: for continuous monotone $F$, $x^*\in S$ iff $x^*\in C$ and $\langle F(y),y-x^*\rangle\ge0$ for all $y\in C$.
8. (3.7), p. 6: every weak cluster point of $(x_n)$ lies in $S$.
9. Proof of Theorem 3.2, p. 6: for each $z\in S$, $\|x_n-z\|^2+2\lambda\langle F(z),x_{n-1}-z\rangle$ converges.
10. Lemma 2.3 (Opial), p. 3: if $x_n\rightharpoonup x$ and $y\ne x$, then $\liminf\|x_n-x\|<\liminf\|x_n-y\|$.

Companion items, not milestones: the defined projection is the metric projection (so runs of Algorithm 3.1 exist from every starting point), Remark 2.1 ($S$ is closed and convex), and the characterization of $S$ as the zeros of the projected residual $r(x,y)=\|y-P_C(x-\lambda F(y))\|+\|x-y\|$ (§3, p. 4).

Significance

The result. Theorem 3.2 shows that a monotone Lipschitz variational inequality in Hilbert space can be solved by an iteration costing one projection and one evaluation of $F$ per step, the minimum for a projection method, with no knowledge beyond the Lipschitz constant. This halves the cost of each iteration relative to the extragradient method when evaluating $F$ is expensive, and keeps the cost of projections at one when projecting onto $C$ is expensive. The method and its analysis became the basis for several later algorithms, including the adaptive variant in §4 of the same paper and the golden ratio algorithm of Malitsky (2020).

Formalizing it. The theorem is proved in the paper; no machine-checked proof is known to exist. The formal development needs, beyond the main argument, a usable library of facts about projections onto closed convex sets in Hilbert space, weak convergence of sequences (boundedness of weakly convergent sequences, weak sequential compactness of bounded sets) and Opial's property. These are reused by every weak-convergence proof for splitting and projection methods, and several companion missions of this series and of related papers rely on the same facts.

Difficulty

The naive Lyapunov function $\|x_n-z\|^2$ is not monotone along the iteration: because $F$ is evaluated at the reflected point $y_n$ rather than at $x_n$, the cross terms do not cancel as they do for the extragradient method. The quantity that does decrease (milestones 3–4) carries extra terms, and the step bound $(\sqrt2-1)/L$ is what the decrease requires. As a consequence, $\|x_n-z\|$ itself is not known to converge, so the standard Opial lemma ("if $\|x_n-z\|$ converges for every $z\in S$ and all weak cluster points lie in $S$, then $x_n$ converges weakly") does not apply directly; the uniqueness of the weak cluster point has to be argued with the perturbed quantity and Opial's inequality. In infinite dimension, the weak cluster point step also needs weak sequential compactness of bounded sets, which is not norm compactness.

Formalization scope

• $H$ is an arbitrary real inner product space with [CompleteSpace H] in every statement that needs completeness; it is never specialised to $\mathbb R^n$, where weak and norm convergence coincide.
• Weak convergence is stated elementarily: $\langle x_n,v\rangle\to\langle x^*,v\rangle$ for every $v\in H$. Subsequences are $x\circ\varphi$ with $\varphi$ strictly increasing.
• The projection $P_C(z)$ is defined by choice as a nearest point, with the junk value $z$ when none exists. Every statement that uses it assumes $C$ closed, convex and nonempty (directly or through $S\ne\emptyset$ or $z\in S$), and a companion item certifies that it is then the metric projection.
• (C2) and (C3) are imposed on all of $H$, as in the paper; $L$ is a real number with $L>0$, and the step range $0<\lambda<(\sqrt2-1)/L$ is strict on both sides.
• Runs of Algorithm 3.1 carry no stopping rule: a run reaching a solution $x_n=y_n\in S$ stays constant, so infinite runs subsume stopped ones. The starting point $x_0$ is any point of $H$, not necessarily in $C$; for this reason Lemma 3.1 and (3.6) are stated for $n\ge2$, which is the range the proof of Theorem 3.2 uses.
• Opial's inequality is stated with liminfs in $[0,\infty]$, where they are always defined.
• A trivializing formalization is ruled out: the goal assumes exactly (C1)–(C3), closedness and convexity of $C$ and the step range, and concludes weak convergence to a point of $S$; it does not assume boundedness of the iterates, a starting point in $C$, finite dimension, or any of the intermediate estimates.

Contributions welcome: proofs of the milestones in any order; general Hilbert-space lemmas (boundedness of weakly convergent sequences via the uniform boundedness principle, weak sequential compactness of bounded sets, Opial's inequality) are useful well beyond this mission.

Selected references

• Yu. Malitsky, Projected reflected gradient methods for monotone variational inequalities, SIAM J. Optim. 25(1) (2015), 502–520. arXiv:1502.04968, doi:10.1137/14097238X
• G. M. Korpelevich, The extragradient method for finding saddle points and other problems, Ekonomika i Matematicheskie Metody 12 (1976), 747–756.
• P. Tseng, A modified forward-backward splitting method for maximal monotone mappings, SIAM J. Control Optim. 38(2) (2000), 431–446. doi:10.1137/S0363012998338806
• Y. Censor, A. Gibali, S. Reich, The subgradient extragradient method for solving variational inequalities in Hilbert space, J. Optim. Theory Appl. 148 (2011), 318–335. doi:10.1007/s10957-010-9757-3
• Z. Opial, Weak convergence of the sequence of successive approximations for nonexpansive mappings, Bull. Amer. Math. Soc. 73 (1967), 591–597. doi:10.1090/S0002-9904-1967-11761-0
• H. H. Bauschke, P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, 2nd ed., Springer, 2017. doi:10.1007/978-3-319-48311-5

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

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