Functional Analysis

Counterexamples to Connes rigidity, from the OpenAI Ten Proofs formalization. The source already contains machine-checked proofs; this mission organizes its headline result and additional Comparator targets for reuse.

There exist a countable group $\Lambda$ and a sequence of countable groups $(\Gamma_n)_{n\in\mathbb N}$, indexed also at $n=0$, such that all of them are finitely generated and infinite, every conjugacy class $\{xgx^{-1}:x\in G\}$ of a nonidentity element in each such group $G$ is infinite, and every such group has property T. For every $n$, $L(\Gamma_n)$ is isomorphic to $L(\Lambda)$ as specified below, and for every $m,n$, including $m=n$, $L(\Gamma_m)$ is isomorphic to $L(\Gamma_n)$ in the same sense. If $m\ne n$, there is no group isomorphism $\Gamma_m\cong\Gamma_n$, and for every $n$ there is no group isomorphism $\Lambda\cong\Gamma_n$. For each group $G$ concerned, property T means that, for every complete complex inner-product space $H$ and every homomorphism $\pi:G\to U(H)$, if for every finite $K\subseteq G$ and every real $\varepsilon>0$ there is a vector $\xi\in H$ with $\|\xi\|=1$ and $\|\pi(g)\xi-\xi\|<\varepsilon$ for all $g\in K$, then there is a nonzero vector fixed by every $\pi(g)$. Here $L(G)$ is the double commutant, inside the bounded complex-linear operators on $\ell^2(G)$, of the left translations $(\lambda_g f)(h)=f(g^{-1}h)$, and $\tau_G(a)=\langle\delta_1,a\delta_1\rangle$. An asserted isomorphism of these tracial algebras is a complex $*$-algebra equivalence preserving $\tau$ such that both it and its inverse preserve every existing supremum of any set of self-adjoint idempotents, with projection order $q\le p$ defined by $qp=q$.

Additional targets:

• Two nonisomorphic finitely generated property T ICC groups with isomorphic tracial group algebras.

The formalization uses Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Its goal and milestone statements retain the validated source statements and their conventions.

Sources: Lean formalization, E_ConnesRigidity.json.

Planned collection: OAI Ten Proofs (oai-ten-proofs).

Motivation

A metric space is plastic if every nonexpansive bijection of it onto itself is an isometry. The mission "Plasticity: c₀ and c₀₀" proved, among other things, that a nonexpansive bijection from the unit ball of a space between $c_{00}(\Gamma)$ and $c_0(\Gamma)$ onto the unit ball of a space between $c_{00}(\Delta)$ and $c_0(\Delta)$ is a signed permutation of coordinates whenever the target matches signs (card Plasticity.CUB37). A scan of unused hypotheses showed that the first step, the normal form, never uses that the target lies in $c_0(\Delta)$. This mission records the consequence: the target may be any space between $c_{00}(\Delta)$ and $\ell_\infty(\Delta)$, because the existence of such a bijection forces it into $c_0(\Delta)$.

Setting

$X$ is a linear subspace with $c_{00}(\Gamma)\subseteq X\subseteq c_0(\Gamma)$ and $Y$ one with $c_{00}(\Delta)\subseteq Y\subseteq\ell_\infty(\Delta)$, both real with the supremum norm, for arbitrary index sets $\Gamma,\Delta$ (definitions Plasticity_SeqSpace). $F$ is a nonexpansive bijection of the closed unit ball of $X$ onto that of $Y$; nothing is assumed about its inverse.

Target

$$\text{(goal)}\quad X=c_{00}(\Gamma)\ \text{or}\ Y\ \text{realizes all sign patterns}\ \Longrightarrow\ F(x)_{\sigma n}=\alpha_nx_n\ \text{for a bijection}\ \sigma\ \text{and signs}\ \alpha_n=\pm1.$$ $$\text{(milestone)}\quad Y\subseteq c_0(\Delta).$$

Significance

The milestone excludes nonexpansive bijections onto balls that the usual extreme-point argument cannot reach: for $Y=c_0\oplus\mathbb R(1,0,1,0,\dots)$ the ball has no extreme points, yet no ball between $c_{00}$ and $c_0$ is mapped onto it by a nonexpansive bijection. The goal is the card Plasticity.CUB37 without its target hypothesis.

Formalization scope

The normal form for targets inside $\ell_\infty(\Delta)$ is a separate card (Plasticity.SeqSpace.exists_signed_permutation_inward), the proof of Plasticity.CUB37.normal_form with the unused hypothesis removed; the goal then imports the Proved card Plasticity.CUB37.

Selected references

• N. Leo, Plasticity of the unit ball of $c$ and $c_0$, J. Math. Anal. Appl. 507 (2022), arXiv:2106.06276.
• 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.

Motivation

A metric space is plastic if every nonexpansive bijection of it onto itself is an isometry; Cascales, Kadets, Orihuela and Wingler (2016) asked whether the closed unit ball of every real Banach space is plastic. The mission "Plasticity: unit spheres covered by finite-dimensional faces" proved that a nonexpansive bijection $F$ between unit balls carries every finite-dimensional face of the target ball back onto a face of the same dimension (card Plasticity.Faces.matchesFace_of_finiteDimensional, stated for normed spaces), and that $F$ is a linear isometry whenever the target sphere is covered by finite-dimensional faces, for Banach spaces. That covering theorem was proved through a sphere-preservation theorem whose proof needs completeness. This mission removes completeness from the covering theorem and its plasticity corollary, by the ending that Angosto, Kadets and Zavarzina (2019) used for polyhedral faces.

Setting

$X$ and $Y$ are real normed spaces, not necessarily complete, with closed unit balls $B_X,B_Y$ and unit spheres $S_X,S_Y$. A sphere face of $B_Y$ is a nonempty convex set $C\subseteq S_Y$ that is an extreme subset of $B_Y$ (definitions Plasticity_Faces). $F\colon B_X\to B_Y$ is a nonexpansive bijection; nothing is assumed about the continuity of $F^{-1}$.

Target

$$\text{(goal)}\quad S_Y\ \text{covered by finite-dimensional sphere faces}\ \Longrightarrow\ F\ \text{is the restriction of a surjective linear isometry}\ X\to Y.$$ $$\text{(plasticity)}\quad S_X\ \text{covered by finite-dimensional sphere faces}\ \Longrightarrow\ B_X\ \text{is plastic}.$$

Significance

The result. Completeness plays no role in the mechanism: the face theorem already holds for normed spaces, and the ending needs only the geometry of planes and the Mazur–Ulam theorem. The steps are: $F$ maps $S_X$ into $S_Y$; by induction on the face dimension, $F$ is isometric on each scaled preimage face along chords that end at boundary points where it is already homogeneous (Zavarzina's Lemma 2.5, proved here by differentiating one inequality at a point of a plane where the norm is differentiable along a line, which Rademacher's theorem supplies), and two points of a face at equal distances from all its boundary points coincide, so $F$ is homogeneous on every ray; then $F$ is an isometry of the balls, and its homogeneous extension is linear by Mazur–Ulam.

Formalizing it. The face theorem is a Proved card in the earlier mission; this mission adds the ending, so that the statements are machine-checked in their natural generality.

Formalization scope

Real scalars; the face theorem Plasticity.Faces.matchesFace_of_finiteDimensional and the basic facts Plasticity.BallMap.* are imported Proved cards. New inputs are separate cards: Zavarzina's isometry lemma for homogeneous points (Plasticity.BallMap.norm_map_sub_map_eq_of_map_smul, using Rademacher's theorem from Mathlib for the density of smooth points), two elementary facts about relative boundaries of bounded sets, and homogeneity on preimage faces (Plasticity.Faces.map_smul_of_map_mem_face). Statements are not to be weakened by assuming completeness, continuity of the inverse or a bound on the face dimensions.

Selected references

• C. Angosto, V. Kadets, O. Zavarzina, Non-expansive bijections, uniformities and polyhedral faces, J. Math. Anal. Appl. 471 (2019), arXiv:1808.08534.
• O. Zavarzina, Non-expansive bijections between unit balls of Banach spaces, Ann. Funct. Anal. 9 (2018), arXiv:1704.06961.
• 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. Mazur, S. Ulam, Sur les transformations isométriques d'espaces vectoriels normés, C. R. Acad. Sci. Paris 194 (1932), 946–948.

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), and Cascales, Kadets, Orihuela and Wingler (2016) asked whether the closed unit ball of every real Banach space is plastic. They proved it for strictly convex spaces, whose unit sphere consists of one-point faces. Angosto, Kadets and Zavarzina (2019) proved it, in the stronger two-space form, when the unit sphere is a union of finite-dimensional polyhedral extreme subsets: then every nonexpansive bijection from the unit ball of any Banach space onto that ball is an isometry. This mission formalizes a theorem that removes the polyhedrality: it suffices that every point of the sphere lies in some finite-dimensional face, of any shape, for instance a round disc. The results come from an unpublished research project on the plasticity problem.

Setting

$X$ and $Y$ are real normed spaces with closed unit balls $B_X,B_Y$ and unit spheres $S_X,S_Y$; the covering and plasticity forms assume them complete. A sphere face of $B_Y$ is a nonempty convex set $C\subseteq S_Y$ that is an extreme subset of $B_Y$: if a point of $C$ lies in the open segment between two points of $B_Y$, both points lie in $C$. Its dimension is that of its affine hull; $\partial C$ and $\operatorname{ext}C$ are its relative boundary and its extreme points. $F\colon B_X\to B_Y$ is a nonexpansive bijection; nothing is assumed about the continuity of $F^{-1}$.

Target

$$\text{(F17)}\quad C\ \text{a finite-dimensional sphere face of}\ B_Y\ \Longrightarrow\ D=F^{-1}(C)\ \text{is a compact sphere face of}\ B_X\ \text{with}\ \dim D=\dim C,$$ $$F^{-1}(-C)=-D,\quad F^{-1}(\partial C)=\partial D,\quad F^{-1}(\operatorname{ext}C)=\operatorname{ext}D,\quad F(tD)=tC\ (0\le t\le1).$$ $$\text{(F17, covering form; goal)}\quad X,Y\ \text{Banach},\ S_Y\ \text{covered by finite-dimensional sphere faces}\ \Longrightarrow\ F\ \text{is the restriction of a surjective linear isometry}\ X\to Y.$$ $$\text{(F17, plasticity)}\quad X\ \text{Banach},\ S_X\ \text{covered by finite-dimensional sphere faces}\ \Longrightarrow\ B_X\ \text{is plastic}.$$

Significance

The result. For a polytope face, the relative boundary is a finite union of smaller polytopes, so an induction on dimension keeps the preimage of the boundary compact; this is the step of Angosto–Kadets–Zavarzina that needs polyhedrality. For a curved face the boundary has a continuum of extreme points, and the inverse map, not known to be continuous, could a priori scatter their preimages. The new step traps the whole boundary preimage in one compact face: the preimage of a relative-interior point is shown to lie strictly between any boundary preimage and another one, by following a path across the scaled boundary, which the induction hypothesis covers exactly. Spaces such as $\ell_p$-sums of a Euclidean space with a three-dimensional space whose ball is a cylinder have only finite-dimensional faces, some of them discs, and are covered by the new theorem but not by the polyhedral one or by strict convexity.

Formalizing it. The proofs exist only in the project's notes and were checked by AI referees; a machine-checked proof is the independent confirmation sought. The covering form ends with the project's theorem that a nonexpansive surjection between unit balls mapping the sphere into the sphere is linear, already formalized (card Plasticity.U10); this is the only step that uses completeness.

Difficulty

No regularity of the inverse map, no strict convexity, polyhedrality or separability is assumed, the face theorem does not assume completeness, and the faces may have any finite dimension. The topology needed is classical but absent from Mathlib: invariance of domain and of dimension, and the impossibility of retracting a ball onto its boundary sphere.

Formalization scope

Real scalars. Faces are expressed with Mathlib's IsExtreme, dimensions as Module.finrank ℝ (vectorSpan ℝ C), relative boundaries as intrinsicFrontier ℝ C (definitions Plasticity_Faces). A ball map is a function F : X → Y constrained on the closed unit ball by Set.BijOn and LipschitzOnWith 1; the preimage of $C$ is closedBall 0 1 ∩ F ⁻¹' C. The plasticity form uses HasPlasticUnitBall (definitions Plasticity_Basic). Statements are not to be weakened by assuming continuity of the inverse, polyhedrality or a bound on the face dimensions. Published inputs (the basic facts of Zavarzina's Theorem 2.3, invariance of dimension, no retraction) are separate cards.

Selected references

• C. Angosto, V. Kadets, O. Zavarzina, Non-expansive bijections, uniformities and polyhedral faces, J. Math. Anal. Appl. 471 (2019), arXiv:1808.08534.
• 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.
• O. Zavarzina, Non-expansive bijections between unit balls of Banach spaces, Ann. Funct. Anal. 9 (2018), arXiv:1704.06961.
• H. Freudenthal, W. Hurewicz, Dehnungen, Verkürzungen, Isometrien, Fund. Math. 26 (1936), 120–122.
• L. E. J. Brouwer, Beweis der Invarianz des n-dimensionalen Gebiets, Math. Ann. 71 (1912).

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), and Cascales, Kadets, Orihuela and Wingler (2016) asked whether the closed unit ball of every real Banach space is plastic. For the sequence space c₀, Leo (2022) proved plasticity of the unit ball of c and, for c₀, under the extra hypothesis that the inverse map is continuous, reducing the general case to a normal form in which the map acts inwardly on each coordinate. This mission formalizes a proof that removes the continuity hypothesis, for c₀(Γ) and c₀₀(Γ) over arbitrary index sets and for nonexpansive bijections between the balls of two spaces sandwiched between c₀₀ and c₀. The results come from an unpublished research project on the plasticity problem.

Setting

For a set $\Gamma$, $\ell_\infty(\Gamma)$ is the space of bounded real functions on $\Gamma$ with the norm $\|x\|=\sup_{i\in\Gamma}|x_i|$; $c_0(\Gamma)$ consists of the $x$ with $\{i:|x_i|\ge\varepsilon\}$ finite for every $\varepsilon>0$, and $c_{00}(\Gamma)$ of the finitely supported $x$. A space between $c_{00}(\Gamma)$ and $c_0(\Gamma)$ is a linear subspace $X$ with $c_{00}(\Gamma)\subseteq X\subseteq c_0(\Gamma)$, with the supremum norm; its closed unit ball is $B_X$. A subspace $Y\subseteq\ell_\infty(\Delta)$ realizes all sign patterns if for every countable $C\subseteq\Delta$ and all signs $\varepsilon_d=\pm1$ ($d\in C$) some $v\in Y$ has $\varepsilon_dv_d>0$ on $C$; $c_0(\Delta)$ does. A signed coordinate bijection is a map $x\mapsto y$ with $y_{\sigma(n)}=\alpha_nx_n$ for a bijection $\sigma\colon\Gamma\to\Delta$ and signs $\alpha_n=\pm1$.

Target

$$\text{(CUB37)}\quad F\colon B_X\to B_Y\ \text{a nonexpansive bijection},\ X=c_{00}(\Gamma)\ \text{or}\ Y\ \text{realizes all sign patterns}\ \Longrightarrow\ F\ \text{is the restriction of a signed coordinate bijection.}$$ $$\text{(CUB35)}\quad \text{the closed unit ball of } c_{00}(\Gamma) \text{ is plastic, for every set } \Gamma.$$ $$\text{(CUB36, goal)}\quad \text{the closed unit ball of } c_0(\Gamma) \text{ is plastic, for every set } \Gamma.$$

Significance

The result. Leo's work reduced plasticity of the unit ball of c₀ to excluding the collapse of a coordinate in a normal form; the unit sphere of c₀ is neither strictly convex nor made of compact faces, and the argument here is the base case of the project's results on c₀-sums of finite-dimensional blocks. The two-space statement CUB37 also shows that for an infinite index set Δ no nonexpansive bijection maps the ball of c₀₀(Γ) onto the ball of c₀(Δ).

Formalizing it. The proofs exist only in the project's notes and were checked by AI referees; a machine-checked proof is the independent confirmation sought. The development needs two classical topological inputs that Mathlib lacks: the theorem of Freudenthal and Hurewicz that a nonexpansive bijection of a compact metric space is an isometry, and a form of invariance of domain in every finite dimension (from Brouwer's fixed-point theorem).

Difficulty

The ball of c₀ is not compact and its unit sphere has large flat faces, so the classical arguments (compactness, strict convexity, smoothness of the norm) do not apply, and no regularity of the inverse map is assumed. The difficulty is concentrated in excluding that the normal form sends a nonzero coordinate to zero.

Formalization scope

Real scalars, arbitrary index sets (no countability or nonemptiness assumed). $\ell_\infty(\Gamma)$ is Mathlib's lp (fun _ : Γ => ℝ) ⊤; $c_0(\Gamma)$ and $c_{00}(\Gamma)$ are submodules of it (definitions Plasticity_SeqSpace), and a ball map is a function on $\ell_\infty(\Gamma)$ constrained on ballIn X by Set.BijOn and LipschitzOnWith 1. CUB35 and CUB36 use HasPlasticUnitBall (definitions Plasticity_Basic) for the submodule types, whose norm is the supremum norm inherited from $\ell_\infty$. Statements are not to be weakened by assuming continuity of the inverse or countable Γ. Published inputs (Freudenthal–Hurewicz, Brouwer or invariance of domain) 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.
• H. Freudenthal, W. Hurewicz, Dehnungen, Verkürzungen, Isometrien, Fund. Math. 26 (1936), 120–122.
• N. Leo, Plasticity of the unit ball of c and c₀, J. Math. Anal. Appl. 507 (2022), arXiv:2106.06276.
• O. Zavarzina, Non-expansive bijections between unit balls of Banach spaces, Ann. Funct. Anal. 9 (2018), arXiv:1704.06961.
• L. E. J. Brouwer, Beweis der Invarianz des n-dimensionalen Gebiets, Math. Ann. 71 (1912).

Motivation

A bounded linear operator $u : E \to F$ between Banach spaces is Fredholm if its kernel is finite-dimensional and its range is closed and of finite codimension. Its index

$$\operatorname{ind} u = \dim \operatorname{Ker} u - \dim \operatorname{Coker} u, \qquad \operatorname{Coker} u = F/\operatorname{Im} u,$$

is an integer that survives deformation: it does not change under small perturbations or under compact perturbations, and it is additive under composition. These properties make Fredholm operators the setting for index theorems. Elliptic differential operators on compact manifolds, Toeplitz operators, linearized Cauchy–Riemann operators in symplectic topology, and the linearizations of nonlinear Fredholm maps in transversality arguments (Sard–Smale) all rest on them. Atkinson's theorem characterizes Fredholm operators as those invertible modulo compact operators. For endomorphisms this says that the image in the Calkin algebra $\mathcal{L}(E)/\mathcal{K}(E)$ is invertible.

This mission formalizes the abstract theory on Banach spaces over $\mathbb{R}$ or $\mathbb{C}$, following N. Bourbaki, Théories spectrales, Chapitre III, §§ 3–5 (Springer, 2023). It builds on Mathlib's ContinuousLinearMap.IsFredholm, which already provides the definition and its equivalent descriptions on topological vector spaces. It adds the index and the results listed below.

Setting

$\mathbb{K}$ is $\mathbb{R}$ or $\mathbb{C}$. $E$, $F$, $G$ are Banach spaces over $\mathbb{K}$, and $\mathcal{L}(E;F)$ is the Banach space of bounded linear maps with the operator norm.

• Fredholm operator. $u \in \mathcal{L}(E;F)$ is Fredholm if $\operatorname{Ker} u$ is finite-dimensional and topologically complemented, $\operatorname{Im} u$ is closed and of finite codimension, and $u$ is a strict map (it induces a homeomorphism $E/\operatorname{Ker} u \to \operatorname{Im} u$). On Banach spaces this agrees with Bourbaki's Définition 1 (TS III.41): $u$ has a quasi-inverse $v \in \mathcal{L}(F;E)$, i.e. $1_E - v\circ u$ and $1_F - u\circ v$ have finite rank.
• Index. $\operatorname{ind} u = \dim \operatorname{Ker} u - \dim (F/\operatorname{Im} u) \in \mathbb{Z}$. Bourbaki (TS III.43, formula (1)) uses the opposite sign; this mission uses the sign above, which is the usual one in analysis and geometry.
• Compact operator. $h \in \mathcal{L}(E;F)$ is compact if it maps some neighbourhood of $0$ into a compact set (Mathlib's IsCompactOperator).

Formalization targets

Goal: Atkinson's theorem

$u \in \mathcal{L}(E;F)$ is Fredholm if and only if there is $v \in \mathcal{L}(F;E)$ such that $1_E - v\circ u$ and $1_F - u\circ v$ are compact (Bourbaki III, §5, Corollaire 1, TS III.74).

Milestones

1. Finite codimension gives closed range. If $F/\operatorname{Im} u$ is finite-dimensional, then $\operatorname{Im} u$ is closed and $u$ is strict (§3, Lemme 6, TS III.52).
2. Fredholm criterion. $u$ is Fredholm if and only if $\operatorname{Ker} u$ and $F/\operatorname{Im} u$ are finite-dimensional (§3, Proposition 11, TS III.52).
3. Composition. If $u : E \to F$ and $v : F \to G$ are Fredholm, so is $v\circ u$ (§3, Remarque 2, TS III.41).
4. Additivity of the index. $\operatorname{ind}(v\circ u) = \operatorname{ind} v + \operatorname{ind} u$ (§3, formula (2), TS III.43).
5. Restriction to subspaces of finite codimension. For closed subspaces $E_1 \subset E$, $F_1 \subset F$ of finite codimension with $u(E_1) \subset F_1$, $u$ is Fredholm if and only if its restriction $u_1 : E_1 \to F_1$ is, and then $\operatorname{ind} u - \operatorname{ind} u_1 = \operatorname{codim} E_1 - \operatorname{codim} F_1$ (§3, Proposition 3, TS III.44).
6. Index zero. A Fredholm operator of index $0$ that is injective or surjective is an isomorphism (§3, n° 3, TS III.44).
7. Openness and local constancy. The Fredholm operators form an open subset of $\mathcal{L}(E;F)$, and the index is locally constant on it (§4, Théorème 1, TS III.58).
8. Compact perturbation, kernel side. If $\operatorname{Ker} u$ is finite-dimensional, $\operatorname{Im} u$ is closed and $h$ is compact, then $\operatorname{Ker}(u+h)$ is finite-dimensional and $\operatorname{Im}(u+h)$ is closed (§5, Théorème 1, TS III.72).
9. Compact perturbation, cokernel side. If $\operatorname{Im} u$ has finite codimension and $h$ is compact, then $\operatorname{Im}(u+h)$ is closed and of finite codimension (§5, Théorème 2, TS III.73).
10. Compact perturbation of Fredholm operators. If $u$ is Fredholm and $h$ is compact, then $u+h$ is Fredholm and $\operatorname{ind}(u+h) = \operatorname{ind} u$ (§5, Théorème 3, TS III.73).
11. Index-zero characterization. $u$ is Fredholm of index $0$ if and only if $u$ is the sum of an isomorphism $E \to F$ and a finite-rank operator, if and only if it is the sum of an isomorphism and a compact operator (§5, Corollaire 2, TS III.74).

Significance

The result. Atkinson's theorem identifies the Fredholm operators with the units modulo the compact ideal. Together with the stability of the index under compact and small perturbations, it is the abstract input of every Fredholm index computation. Examples are the Fredholm alternative for integral equations, the index of Toeplitz operators, and the index of elliptic and Cauchy–Riemann operators on compact or punctured surfaces.

Formalizing it. Mathlib defines Fredholm operators on topological vector spaces (ContinuousLinearMap.IsFredholm) and proves that four descriptions agree (isFredholm_tfae). It has no index, no statement about compositions, and no perturbation theory. Its documentation lists the Banach-space criterion (milestone 2) and the restriction statement (milestone 5) as not yet formalized. The library built here is intended for reuse by any later index computation.

Difficulty

The statements combine linear algebra and topology. The index is a difference of dimensions of a subspace and a quotient space, and every statement about it carries a Fredholm hypothesis, since Module.finrank is $0$ on infinite-dimensional spaces. Openness and local constancy are statements about the operator-norm topology on $\mathcal{L}(E;F)$, and the perturbation statements involve operators that are compact but not necessarily of finite rank. The completeness hypotheses are part of the statements: over incomplete normed spaces, a range of finite codimension need not be closed.

Formalization scope

• Namespace FredholmBanach. The definition module FredholmBanach_Setting defines only index. Fredholm operators are Mathlib's ContinuousLinearMap.IsFredholm and compact operators are Mathlib's IsCompactOperator.
• Field and spaces. [RCLike 𝕜], [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E], and likewise for F and G. Bourbaki states several results for locally convex or Fréchet spaces; this mission specializes all of them to Banach spaces.
• Index. index u = finrank 𝕜 u.ker - finrank 𝕜 (F ⧸ u.range) in ℤ. Module.finrank is $0$ on infinite-dimensional spaces, so index is meaningful only for Fredholm u. Every statement about it assumes u.IsFredholm.
• Subspaces and quotients. The codimension of a subspace $E_1$ is finrank 𝕜 (E ⧸ E₁), and "finite codimension" is FiniteDimensional 𝕜 (E ⧸ E₁). The restriction in milestone 5 is ContinuousLinearMap.restrict.
• Isomorphisms are E ≃L[𝕜] F. "Finite rank" is FiniteDimensional 𝕜 (u - e).range.

Contributions welcome: reusable general-purpose lemmas about bounded and compact operators between Banach spaces.

Selected references

• N. Bourbaki, Théories spectrales, Chapitres III à V, Springer (2023), Chapitre III, §§ 3–5. https://doi.org/10.1007/978-3-031-19505-1
• F. V. Atkinson, The normal solubility of linear equations in normed spaces, Mat. Sb. (N.S.) 28(70):1 (1951), 3–14 (in Russian), MR0042059. https://mathnet.ru/eng/sm5589
• T. Kato, Perturbation Theory for Linear Operators, Springer (1995 reprint of the 2nd ed.). https://doi.org/10.1007/978-3-642-66282-9
• D. McDuff, D. Salamon, J-holomorphic Curves and Symplectic Topology, 2nd ed., AMS Colloquium Publications 52 (2012). https://doi.org/10.1090/coll/052

Motivation

Let $S : S^1 \to \mathbb{R}^{2n\times 2n}$ be a loop of symmetric matrices. The asymptotic operator

$$A_S = -J_0\,\partial_t - S(t)$$

acts on loops $S^1 \to \mathbb{R}^{2n}$. It appears wherever a pseudoholomorphic curve approaches a periodic orbit. Near a puncture, a finite-energy curve in a symplectization converges to a Reeb orbit, and in a trivialization along that orbit the linearized Reeb flow is $\Psi' = J_0 S \Psi$. The operator $A_S$ is the Hessian of the action functional at that orbit. The rate of approach and the winding of the curve around the orbit come from its eigenfunctions (Hofer–Wysocki–Zehnder 1995). In Floer theory the operator $-J_0\partial_t - S$ is the Hessian of the symplectic action at a $1$-periodic orbit, and the gradient-flow operator $\partial_s + A_{S(s)}$ is the linearized Floer operator (Robbin–Salamon 1995).

The operator links functional analysis to the linear algebra of stage I. $A_S$ is nondegenerate, i.e. $0$ is not an eigenvalue, exactly when the time-one map $\Psi(1)$ of the linearized flow has no eigenvalue $1$. Then $\Psi|_{[0,1]}$ lies in $\mathrm{SP}(n)$ and has a Conley–Zehnder index. The Fredholm index formula for Cauchy–Riemann operators on punctured surfaces is written in terms of the Conley–Zehnder indices of the asymptotic operators at the punctures (Wendl, Lectures on SFT, Lecture 3).

This is stage II of a series that formalizes the Fredholm theory of linearized Cauchy–Riemann operators. Stage I (Conley–Zehnder Index I: Axiomatic Characterization on Paths of Symplectic Matrices) characterizes the Conley–Zehnder index on $\mathrm{SP}(n)$. This stage sets up the spectral theory of asymptotic operators: the operator itself, self-adjointness, discrete spectrum, compact resolvent, and the dictionary between the kernel of $A_S$ and the time-one map. Later stages are the Fredholm theory of $\partial_s + A_{S(s)}$ in Banach spaces, elliptic regularity for $\bar\partial$, and the index formula.

Setting

$S^1 = \mathbb{R}/\mathbb{Z}$ with its Haar probability measure. $\mathbb{R}^{2n}$ has coordinates $(q,p)$ and the Euclidean inner product, and

$$J_0 = \begin{pmatrix} 0 & -\mathrm{Id}\\ \mathrm{Id} & 0\end{pmatrix}.$$

$S : S^1 \to \mathbb{R}^{2n\times 2n}$ is continuous with $S(t)^{\mathsf T} = S(t)$ for every $t$.

• Fourier coefficients. For $f \in L^2(S^1,\mathbb{R}^{2n})$ and $k \in \mathbb{Z}$, $\hat f_k = \int_{S^1} e^{-2\pi i k t} f(t)\,dt \in \mathbb{C}^{2n}$.
• Domain. $W^{1,2}(S^1,\mathbb{R}^{2n})$ is the set of $f \in L^2$ with $\sum_{k\in\mathbb{Z}} (1+k^2)\,|\hat f_k|^2 < \infty$.
• The operator. For $f \in W^{1,2}$, $A_S f = g$ means $\hat g_k = -2\pi i k\,J_0 \hat f_k - (Sf)^\wedge_k$ for every $k$, i.e. $g = -J_0 f' - S f$ with the derivative taken in $L^2$. This is Wendl's (3.4) with period $1$.
• Fundamental solution. $\Psi : \mathbb{R} \to \mathbb{R}^{2n\times2n}$ with $\Psi(0) = \mathrm{Id}$ and $\Psi'(t) = J_0 S(t)\Psi(t)$. These are the solutions of $(-J_0\partial_t - S)\Psi = 0$. For constant $S$, $\Psi(t) = \exp(tJ_0S)$ is the path in the signature property of stage I.

Formalization targets

Goal: spectral theory of the asymptotic operator

For every continuous loop $S$ of symmetric matrices:

1. $A_S$ with domain $W^{1,2}$ is self-adjoint on $L^2(S^1,\mathbb{R}^{2n})$;
2. $L^2(S^1,\mathbb{R}^{2n})$ has an orthonormal basis of eigenvectors of $A_S$ lying in $W^{1,2}$; the eigenvalues are real, each has finite multiplicity, and they accumulate only at $\pm\infty$;
3. $\ker A_S \cong \ker(\Psi(1) - \mathrm{Id})$, where $\Psi$ is the fundamental solution.

Milestones

1. Well-defined operator. Exactly one partially defined linear map on $L^2$ has graph $\{(f, A_S f)\}$.
2. Domain. The domain of $A_S$ is $W^{1,2}$, and it is dense in $L^2$.
3. Symmetry. $\langle A_S f, g\rangle = \langle f, A_S g\rangle$ for $f, g \in W^{1,2}$.
4. Self-adjointness.
5. Discrete spectrum. An orthonormal eigenbasis exists, with eigenvalues of finite multiplicity tending to $\pm\infty$.
6. Compact resolvent. If $\mu \in \mathbb{R}$ is not an eigenvalue, $A_S - \mu : W^{1,2} \to L^2$ is bijective and its inverse is a compact operator on $L^2$.
7. Unbounded spectrum. For $n \geq 1$ there are eigenvalues of both signs with arbitrarily large absolute value.
8. The unperturbed operator. The eigenvalues of $-J_0\partial_t$ are exactly $2\pi k$, $k\in\mathbb{Z}$, and each eigenspace has dimension $2n$.
9. Fundamental solution. $\Psi$ exists and is unique for every continuous loop $S$.
10. Symplecticity. If $S$ is symmetric, $\Psi(t) \in \mathrm{Sp}(2n)$ for every $t$.
11. Kernel. $\ker A_S \cong \ker(\Psi(1) - \mathrm{Id})$.
12. Nondegeneracy. $0$ is not an eigenvalue of $A_S$ if and only if $\Psi|_{[0,1]} \in \mathrm{SP}(n)$.

Significance

The result. These are the analytic facts that every use of asymptotic operators relies on. Self-adjointness and the discrete spectrum define the eigenvalue branches and the spectral flow. The compact resolvent makes $A_S - \mu$ Fredholm of index $0$ for every real $\mu$, and the weighted Sobolev spaces of the later Fredholm theory are chosen with weights avoiding the spectrum. The kernel dictionary identifies nondegenerate asymptotic operators with the paths of stage I. It is the bridge through which Conley–Zehnder indices enter the index formula.

Formalizing it. All results here are classical. Mathlib has partially defined linear maps and their adjoints, the Fourier basis of $L^2$ on the circle, and compact operators. It has no Sobolev spaces on the circle, no unbounded operator with discrete spectrum beyond trivial cases, and no first-order differential operator treated as an unbounded operator. This stage builds the first such example. The same pattern applies to other first-order elliptic operators on $S^1$, and the library is reusable for spectral flow and for Floer-type operators.

Difficulty

$A_S$ is unbounded and not defined on all of $L^2$, so self-adjointness is a statement about the domain of the adjoint, not a symmetry identity. The spectral statements concern the resolvent of a first-order differential operator with non-constant coefficients, as an operator on $L^2$. The kernel dictionary relates $L^2$ classes, defined through Fourier coefficients, to classical solutions of a linear ODE. The statements about $\Psi$ concern linear ODEs whose coefficients are only continuous.

Formalization scope

• Namespace AsymptoticOperator; all definitions are in AsymptoticOperator_Setting, which imports stage I's ConleyZehnder_Setting (for Mat n, J₀, IsSymplectic and SP).
• The circle is UnitAddCircle ($\mathbb{R}/\mathbb{Z}$) with AddCircle.haarAddCircle. $L^2(S^1,\mathbb{R}^{2n})$ is Lp (EuclideanSpace ℝ (Fin n ⊕ Fin n)) 2 haarAddCircle, a real Hilbert space.
• Fourier coefficients are Mathlib's fourierCoeff, applied to the componentwise complexification $\mathbb{R}^{2n} \to \mathbb{C}^{2n}$. $J_0$ and $S(t)$ act on $\mathbb{C}^{2n}$ through the real-to-complex coercion.
• The operator is a LinearPMap, defined by choice as the map whose graph is the set of pairs $(f, g)$ satisfying the coefficient identity. The fallback is $0$, and milestone 1 makes it unreachable. Self-adjointness is Mathlib's IsSelfAdjoint for LinearPMap, and symmetry is IsFormalAdjoint.
• Eigenspaces are kernels of $A_S - \mu$ on the domain. The discrete spectrum is stated as a HilbertBasis of eigenvectors whose eigenvalues tend to $\infty$ in absolute value along the cofinite filter. This covers $n = 0$, where $L^2 = 0$.
• Regularity of $S$. Wendl assumes $S$ smooth; Hofer–Wysocki–Zehnder (§3, (35)) take $S$ continuous, as here. HWZ state self-adjointness, compact resolvent and discreteness of the spectrum for $n = 1$; this mission states them for all $n$.
• Sign conventions follow Wendl §3.2: $A_S = -J_0\partial_t - S$ and $\Psi' = J_0S\Psi$.

Contributions welcome: reusable lemmas on Sobolev spaces of vector-valued functions on the circle (Fourier characterization, continuity of $W^{1,2}$ functions), on unbounded self-adjoint operators with compact resolvent, and on linear ODEs with continuous periodic coefficients.

Selected references

• C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, Lecture 3 (§§3.2–3.4). https://arxiv.org/abs/1612.01009
• H. Hofer, K. Wysocki, E. Zehnder, Properties of pseudoholomorphic curves in symplectisations II: Embedding controls and algebraic invariants, Geom. Funct. Anal. 5 (1995), 270–328. https://doi.org/10.1007/BF01895669
• J. Robbin, D. Salamon, The spectral flow and the Maslov index, Bull. London Math. Soc. 27 (1995), 1–33. https://doi.org/10.1112/blms/27.1.1
• D. Salamon, Lectures on Floer homology, in: Symplectic Geometry and Topology, IAS/Park City Math. Ser. 7, AMS (1999), 143–229. https://doi.org/10.1090/pcms/007/05
• J. Gutt, Generalized Conley–Zehnder index, Ann. Fac. Sci. Toulouse Math. (6) 23 (2014), 907–932. https://doi.org/10.5802/afst.1430

Motivation: comparing quantum processes

A quantum channel describes a physical process that transforms a quantum state into another state. Comparing two channels means comparing their possible outputs, including outputs obtained when the input is entangled with a reference system. This distinction matters in quantum information: an experiment can retain a reference while sending the other part of an entangled state through an unknown process. The resulting measure of distinguishability should account for that experiment.

For states, several divergence measures approach relative entropy when their order parameter approaches one. For channels, optimization over inputs and arbitrarily many channel uses introduces an additional question: does this continuity survive those optimizations? Jinzhao Wang and Yuxiang Yang answer that question for the regularized, stabilized sandwiched Rényi divergence in Continuity of Regularized Channel Rényi Divergences, arXiv:2609.28635v1, Theorem 1. This mission contributes the completed result and its supporting formal infrastructure.

Setting: states, references, and repeated uses

Let $H$ and $K$ be nonzero finite-dimensional complex Hilbert spaces. A density operator is a positive operator with trace one. Two channels $N,M:\mathcal L(H)\to\mathcal L(K)$ are completely positive, trace-preserving linear maps with the same input and output spaces.

The relative entropy $D(\rho\Vert\sigma)$ compares density operators $\rho$ and $\sigma$. The sandwiched Rényi divergence $\widetilde D_\alpha(\rho\Vert\sigma)$ is an order-dependent comparison, defined for $\alpha\ge\tfrac12$, $\alpha\ne1$. The state, channel, and regularized divergences are measured in bits. Operator-level analytic lemmas may use natural logarithms; the state wrappers divide by $\log 2$. Singular states are allowed; the support conventions retain infinite values rather than assigning a finite substitute. These are the state quantities in the paper's equations (1.2)–(1.3).

The stabilized channel divergence optimizes the state divergence over normalized pure inputs on $H\otimes R$, where $R$ is a copy of $H$. The channel acts on $H$ and the identity acts on $R$. Writing $\psi=|\psi\rangle\langle\psi|$, the convention is

$$\mathbb D(N\Vert M)=\sup_{\|\psi\|=1} \mathbb D\bigl((N\otimes\operatorname{id}_R)(\psi) \Vert(M\otimes\operatorname{id}_R)(\psi)\bigr),$$

where $\mathbb D$ denotes either state divergence. The paper places the reference first; the formalization places it second and proves the tensor-factor convention agrees. A block of $n$ uses employs $N^{\otimes n},M^{\otimes n}$ and a reference copy of $H^{\otimes n}$. Its pure input may be entangled across every use. Equation (1.4) specifies this stabilization.

Formalization targets

The regularized divergences are defined independently as positive-block suprema:

$$\widetilde D_\alpha^{\mathrm{reg}}(N\Vert M) =\sup_{n\ge1}\frac{\widetilde D_\alpha(N^{\otimes n}\Vert M^{\otimes n})}{n}, \qquad D^{\mathrm{reg}}(N\Vert M) =\sup_{n\ge1}\frac{D(N^{\otimes n}\Vert M^{\otimes n})}{n}.$$

Two supporting targets establish that these definitions are the actual asymptotic limits in equation (1.5). For every fixed $\alpha\ge\tfrac12$, $\alpha\ne1$,

$$\lim_{n\to\infty}\frac{\widetilde D_\alpha(N^{\otimes n}\Vert M^{\otimes n})}{n} =\widetilde D_\alpha^{\mathrm{reg}}(N\Vert M),$$

and

$$\lim_{n\to\infty}\frac{D(N^{\otimes n}\Vert M^{\otimes n})}{n} =D^{\mathrm{reg}}(N\Vert M).$$

The main goal is Theorem 1:

$$\lim_{\alpha\to1,\,\alpha\ne1} \widetilde D_\alpha^{\mathrm{reg}}(N\Vert M) =D^{\mathrm{reg}}(N\Vert M).$$

This is convergence from both sides. Each target includes infinite divergence. The block identities are supporting identifications, rather than extra premises of the main theorem.

Significance: continuity after optimization

The main result identifies a single limit after optimization over entangled inputs and unbounded block lengths. It permits near-one regularized Rényi quantities to approach regularized relative entropy for arbitrary channel pairs in the stated finite-dimensional setting. When the latter is infinite, the conclusion is convergence to positive infinity. The paper discusses applications to discrimination and asymptotic approximation; those operational conclusions are beyond this mission's targets. Wang–Yang, arXiv:2609.28635v1.

This is a contribution of a known, formally proved result, rather than an unsolved conjecture. The original public Lean development includes proofs of the definitions' supporting properties and both block identities. Its recorded verification reports Lean checking with a transitive axiom audit, Comparator statement comparison and Lean kernel replay, and independent Nanoda kernel checking. These records concern the original pinned development. They are unsigned and do not establish independent human review of correspondence to the paper. The converted contribution uses Lean 4.30.0 and Mathlib c5ea003. Its 95 Definition bundles and 27 theorem nodes have been published; every theorem has an ACCEPTED proof and public Proved status. Before upload, the exact statement and solution files compiled locally, their types and transparent definition values were compared with the frozen compatibility port, and a transitive axiom audit of every generated declaration found only propext, Classical.choice, and Quot.sound. These new checks are separate from the original Comparator and Nanoda records. Human review of correspondence to the paper is still required.

Difficulty: optimization and singular inputs

Pointwise continuity for a fixed pair of output states does not justify interchanging a limit with the supremum over all block inputs. That domain includes every positive block length, so finite-dimensionality of each block does not itself supply a uniform conclusion. The right-hand limit is particularly sensitive to the order of these operations. Singular inputs introduce a separate issue: support mismatch can force genuine infinity, and converting all expressions to ordinary real numbers would discard that case. The formalization must preserve these domains and conventions throughout, as documented in the paper-to-Lean mapping.

Formalization scope

The Lean representation uses actual positive density operators, CPTP maps, reference systems, and tensor powers. State divergences have extended-real values; channel and regularized divergences take values in $[0,+\infty]$. Nonnegativity is proved for the admissible orders, so conversion to nonnegative extended reals preserves those values. Supremum definitions quantify over positive block lengths. The normalized block sequences are total at $n=0$, which is irrelevant to convergence as $n\to\infty$.

The main formal statement uses a punctured neighborhood of one. A sufficiently small such neighborhood lies within $\alpha>\tfrac12$, so totalized definitions at other real orders impose no assertion about their divergence interpretation outside the admissible range. No support inclusion, finite max-relative entropy, filter estimate, or Schatten estimate is assumed by the main theorem. Defining the limiting value to equal the desired conclusion, or replacing arbitrary channels by an easy special family, would not meet these targets.

The development builds on Mathlib and Lean-Quantum. Reusable components include extended-valued Fekete convergence, channel tensor identities, quantum testing quantities, prescribed-dilation approximation, and finite-dimensional Schatten bounds. The scope mapping records that the supporting decomposition estimate is formalized for $1<\alpha\le2$, sufficient near one; it does not claim the paper's entire all-orders version. Contributions that improve reuse, verify the converted dependency graph, or extend separately stated results are welcome. The paper's later operational corollaries are excluded.

Selected references

• Jinzhao Wang and Yuxiang Yang, Continuity of Regularized Channel Rényi Divergences, arXiv preprint, 2026, version 1. Paper and versioned source.
• Jinzhao Wang, Continuity of regularized channel Rényi divergence: Lean formalization, public software repository, 2026; development assisted by Codex. Source commit e29274a, v1.1.0 verification release.
• Hayata–Yamasaki Group, Lean-Quantum, formalization library, pinned revision bf1c4f6, 2026. Dependency source.
• Lean community, Mathlib4, mathematical library for Lean 4, 2026. Converted contribution's selected revision c5ea003.

Motivation

Rademacher cotype measures how vector norms compare with random signed sums. The target relates cotype of a space and its dual to boundedness of the Rademacher projection. The pinned manuscript supplies the research context.

Setting

X is a nonzero real Banach space with the ordinary approximation property: finite-rank operators approximate the identity on each compact set, with no uniform operator-norm bound required.

Formalization target

The selected goal is OAI.Cotype.mainTarget_proved. Its central assertion is

$$K\text{-convex}(X)\quad\Longleftrightarrow\quad\mathrm{finite\ cotype}(X)\land\mathrm{finite\ cotype}(X^*).$$

The theorem states that, for every real Banach space X (a complete real normed space) that is nontrivial, the defined proposition MainTarget(X) holds. MainTarget(X) says: if X has the approximation property, then X is K-convex if and only if both X and its dual space of continuous linear functionals X →L[ℝ] ℝ have finite cotype. Here the approximation property means that for every compact set M ⊆ X and every δ > 0 there is a continuous linear operator S : X → X with finite-dimensional range such that ‖Sx − x‖ < δ for all x in M. On the discrete cube {±1}ⁿ (with sign false = +1 and true = −1), the L² norm of f : cube → X is the square root of the average of ‖f(ε)‖² over all ε. The moment of f at coordinate i is the average of ε_i f(ε), and the Rademacher projection of f is the function ε ↦ Σᵢ ε_i times the moment at i. X is K-convex if there is a constant K ≥ 0 such that, for every n and every f on the n-cube, the L² norm of the Rademacher projection of f is at most K times the L² norm of f. X has cotype q, for real q ≥ 2, if there is C ≥ 0 such that, for every n and all vectors x₁, …, xₙ in X, (Σ ‖xᵢ‖^q)^(1/q) ≤ C times the L² norm of ε ↦ Σ ε_i xᵢ. Finite cotype means cotype q for some such q.

Significance and status

The approximation property is a hypothesis inside MainTarget. The statement does not assert the equivalence without it; the cube normalization is the encoded average L² norm. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.

Difficulty

The two cotype exponents may differ, and ordinary approximation cannot be strengthened silently to bounded approximation.

Formalization scope

The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.

The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.

Selected references

• OpenAI, The cotype–cotype conjecture under the approximation property, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

A Banach norm supplies both linear and metric structure. A bi-Lipschitz equivalence controls distances, but the target asks for spaces whose linear structures cannot be identified. The pinned manuscript supplies the research context.

Setting

The two spaces are real, complete and separable. The obstruction uses the space of null sequences with values in the real Hilbert space ℓ².

Formalization target

The selected goal is OAI.LipschitzCounterexample.main. Its central assertion is

$$\frac4{21}\|s-t\|\leq\|\Psi(s)-\Psi(t)\|\leq\frac{76}{25}\|s-t\|.$$

The theorem states that the defined proposition MainClaim holds (it is admitted in the source, not proved here). MainClaim asserts that there exist two separable real Banach spaces X and Y, each given as a type with a norm, a real normed-space structure, completeness and separability, together with a bijection Ψ from X onto Y, such that Ψ is a bi-Lipschitz equivalence with explicit constants: for all s and t in X, (4/21)‖s−t‖ ≤ ‖Ψ(s)−Ψ(t)‖ ≤ (76/25)‖s−t‖. Moreover, there is no continuous linear equivalence (linear homeomorphism) between X and Y, so the two spaces are Lipschitz equivalent but not linearly isomorphic. In addition, there is a linear isometric embedding of C0L2 into X, where C0L2 is the space of continuous functions from the natural numbers to the real Hilbert space ℓ² that vanish at infinity. Finally, Y does not contain a linear copy of C0L2, meaning there is no bounded linear map T from C0L2 to Y and constant a>0 with a‖x‖ ≤ ‖T x‖ for every x in C0L2.

Significance and status

The goal includes the explicit distortion bounds, lack of continuous linear equivalence, an isometric copy of c0(ℓ²) in X, and absence of a bounded-below linear copy in Y. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.

Difficulty

A global metric bijection must coexist with a linear embedding obstruction, so the counterexample cannot follow merely from nonlinearity of a particular map.

Formalization scope

The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.

The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.

Selected references

• OpenAI, Lipschitz Equivalent Separable Banach Spaces Need Not Be Linearly Isomorphic, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

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: 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

This mission formalizes A. Connes, J. Feldman and B. Weiss, An amenable equivalence relation is generated by a single transformation, Ergodic Theory Dynam. Systems 1 (1981) 431–450 (doi:10.1017/S014338570000136X).

Motivation

A countable group acting on a measure space partitions it into countable orbits, and much of ergodic theory studies actions only through this orbit equivalence relation. The simplest relations are those of a single transformation, the orbits of an action of $\mathbb Z$. Connes, Feldman and Weiss characterize exactly which relations are of this kind, up to null sets: the amenable ones, those carrying an invariant mean. Since the orbit relation of any action of a countable amenable group is amenable, every such action is orbit equivalent to an action of $\mathbb Z$. The same theorem gives the uniqueness of Cartan subalgebras in hyperfinite von Neumann algebras.

On this platform it is the missing link in the Lodha–Moore mission, which passes between Lodha and Moore's definition of a $\mu$-amenable relation (an orbit relation of $\mathbb Z$ off a null set) and the invariant-mean definition of the Monod bundle: one direction is proved, the other (LodhaMoore.isMuAmenable_of_isAmenableRel) is this mission's goal in Lodha and Moore's language.

Timeline.

• 1959, 1963: Dye proves orbit equivalence for measure-preserving actions of abelian groups and groups of polynomial growth (doi:10.2307/2372852, doi:10.2307/2373108).
• 1976: Krieger classifies non-singular transformations up to orbit equivalence (doi:10.1007/BF01360278).
• 1977: Feldman and Moore set up countable Borel equivalence relations and their von Neumann algebras (doi:10.1090/S0002-9947-1977-0578656-4).
• 1978: Zimmer introduces amenable actions and shows that discrete subgroups act amenably on $G/P$ for $P$ amenable (doi:10.1016/0022-1236(78)90013-7).
• 1980: Ornstein and Weiss prove that every measure-preserving action of a countable amenable group is orbit equivalent to an action of $\mathbb Z$ (doi:10.1090/S0273-0979-1980-14702-3).
• 1981: Connes, Feldman and Weiss prove it for every amenable non-singular countable equivalence relation, without a group.
• 2004: Kechris and Miller give a detailed modern account in Topics in orbit equivalence (doi:10.1007/b99421).

Setting

$X$ is a standard Borel space with a $\sigma$-finite measure $\mu$. A discrete measured equivalence relation (IsDiscreteMeasured μ R) is a Borel equivalence relation $R \subseteq X \times X$ whose classes are countable and for which $\mu$ is quasi-invariant: the saturation $R(A) = \{x \mid \exists y \in A, (x, y) \in R\}$ of a null Borel set $A$ is null.

$R$ carries the measure $m = \int \nu^x\, d\mu(x)$, $\nu^x$ the counting measure on the class of $x$ (relMeasure), and the module $\delta$, the density of $m$ against its image under $(x, y) \mapsto (y, x)$ (module). A partial transformation of $R$ is a Borel bijection between Borel subsets of $X$ whose graph lies in $R$ (Monod.PartialTransformation).

$R$ is amenable (Monod.IsAmenableRel) when it has a left invariant mean: a positive normalized map $P$ from bounded functions on $R$ to bounded functions on $X$ with $P(f^\phi) = (Pf)^\phi$ for every partial transformation $\phi$ (Definitions 5–6). $R$ is of type I (IsTypeI) when, off a null saturated set, its quotient is a standard Borel space, and hyperfinite (IsHyperfinite) when, off a null set, it is a countable increasing union of type I equivalence relations (Definition 1). A finite subequivalence relation (IsFiniteSubrelation) is a Borel $T \subseteq R$ that is an equivalence relation with finite classes on $T^{(0)} = \{x \mid (x, x) \in T\}$.

Formalization targets

Goal (p. 431)

For $R$ amenable there are a non-singular Borel automorphism $T$ of $X$ and a null set $N$ with

$$(x, y) \in R \iff \exists n \in \mathbb Z,\ y = T^n x \qquad (x, y \notin N).$$

Milestones

• §1 (p. 434): the type I criterion; hyperfinite relations are those generated by one automorphism (Dye, external); subrelations of hyperfinite relations are hyperfinite.
• §§2–3: Lemma 2 (disintegration over a finite subrelation), Feldman and Moore's Theorem 1 (external, as the proof of Lemma 3 applies it), Lemma 3 (bounded sets), Lemma 4 (local triviality).
• §§5–6: Lemma 8 (the Følner condition), Lemma 9 (approximation by finite subrelations), Theorem 10 (hyperfinite if and only if amenable).
• §7: Corollary 12, Corollary 13 (Vershik), and Corollary 14 with the amenability of the action it rests on (Zimmer, external).

Significance

The result. Theorem 10 turns amenability, which is usually easy to check, into hyperfiniteness, which is the structure one wants: for instance, the action of $\mathrm{SL}_2(\mathbb Z)$ on the projective line, or of any discrete group on $G/P$ with $P$ amenable, is generated by a single transformation. On this platform it closes the open direction, LodhaMoore.isMuAmenable_of_isAmenableRel, and with it Lodha and Moore's Theorem 2.1.

Formalizing it. No machine-checked proof of the theorem exists, in Mathlib or elsewhere as far as a search finds; Mathlib has no theory of countable Borel equivalence relations. A complete development builds that theory from the descriptive set theory Mathlib has.

Difficulty

The theorem is about relations without a group. The obvious route, through a countable group generating $R$ and an amenability of that group, is unavailable: the orbit relation of a nonamenable group, such as $\mathrm{SL}_2(\mathbb Z)$ acting on the projective line, can be amenable, and there is no group whose Følner sets one could use. The Følner sets of Lemma 8 have to be produced from the invariant mean on the relation itself, which needs duality between $L^1$ and $L^\infty$ and convexity arguments. Underneath, even the basic facts used in §§1–3 (that $R$ is a countable union of graphs of Borel automorphisms, that $m$ is a measure, that saturations of Borel sets are Borel) rest on the Lusin–Novikov uniformization theorem, which is not in Mathlib. It is published here as standalone theorems: a Borel set with countable sections is a countable union of Borel graphs, and a countable-to-one Borel map is injective on countably many Borel pieces covering its domain.

Formalization scope

All statements carry the hypotheses of §1: $X$ standard Borel (StandardBorelSpace), $\mu$ $\sigma$-finite, $R$ a Borel equivalence relation with countable classes and $\mu$ quasi-invariant. Lemmas 8 and 9 take $\mu$ a probability measure, as the paper's proof of Lemma 9 does. “Up to a null set” is read as “off a $\mu$-null Borel set of points”, which by quasi-invariance agrees with the paper's $m$-null sets. Amenability is the published Monod definition, an invariant mean on bounded measurable functions modulo null sets; it is not trivial (the relation of $\mathrm{PSL}_2(A)$ for a countable dense subring $A$ of $\mathbb R$ is not amenable, Monod.not_isAmenableRel_mob).

The definitions are in the definition bundle ConnesFeldmanWeiss. Reusable beyond this mission: the Feldman–Moore theorem and the basic theory of countable Borel equivalence relations, both welcome as standalone theorems.

What is left out. Proposition 7 and Corollary 11 need the von Neumann algebra of a relation and its Cartan subalgebras, which Mathlib does not have. The final part of the paper (Lemma 15 to Corollary 21) treats relations with uncountable classes through transverse functions, including foliations; it is a different setting with its own definitions.

Selected references

• A. Connes, J. Feldman, B. Weiss, An amenable equivalence relation is generated by a single transformation, Ergodic Theory Dynam. Systems 1 (1981) 431–450. doi:10.1017/S014338570000136X
• H. A. Dye, On groups of measure preserving transformations. I, Amer. J. Math. 81 (1959) 119–159. doi:10.2307/2372852
• J. Feldman, C. C. Moore, Ergodic equivalence relations, cohomology, and von Neumann algebras. I, Trans. Amer. Math. Soc. 234 (1977) 289–324. doi:10.1090/S0002-9947-1977-0578656-4
• R. J. Zimmer, Amenable ergodic group actions and an application to Poisson boundaries of random walks, J. Funct. Anal. 27 (1978) 350–372. doi:10.1016/0022-1236(78)90013-7
• D. Ornstein, B. Weiss, Ergodic theory of amenable group actions. I: The Rohlin lemma, Bull. Amer. Math. Soc. 2 (1980) 161–164. doi:10.1090/S0273-0979-1980-14702-3
• A. S. Kechris, B. D. Miller, Topics in orbit equivalence, Lecture Notes in Math. 1852, Springer, 2004. doi:10.1007/b99421

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 establishes the best possible constant for complex diagonal matrices for every real $p\ge256$. The result is proved in Lean. For each exponent, one constant works for every triple of diagonal matrices of the same size, across all finite sizes.

The constant comes from a simple family of three $3\times3$ diagonal matrices, called the cyclic family. Varying one parameter determines the largest comparison constant these examples require. The theorem proves that this value also works for every other triple of diagonal matrices, however large. The goal theorem gives the exact formula and statement.

This is the foundation of the sharp diagonal Hlawka campaign. It supplies the shared definitions and supporting results for lowering the exponent cutoff while keeping the same formula. A later mission has now established the result in Lean for every real $p\ge90$; the campaign invites further improvements.

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

Established results on Prove2Me

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

This mission formalizes A. Garrido, An introduction to amenable groups, lecture notes from four talks at the Oxford Advanced Class in Algebra, Michaelmas 2013 (archived PDF) — its Section 1.2, Section 2 and Section 3.

Motivation

A group is amenable when its subsets can be measured in a way that translation does not disturb. Von Neumann isolated the notion in 1929 to explain the Banach–Tarski paradox: a solid ball in $\mathbb{R}^3$ can be cut into finitely many pieces and reassembled into two balls of the original size, and the reason is group-theoretic rather than geometric — the rotation group $SO(3,\mathbb{R})$ contains a free group of rank two, while the isometry groups of $\mathbb{R}$ and $\mathbb{R}^2$ do not. No paradox is possible for a group carrying a translation-invariant finitely additive probability measure.

Mahlon Day proved in the 1950s that von Neumann's definition agrees with the existence of an invariant mean on bounded functions, moving the theory into functional analysis, and coined the word "amenable" as a pun on "mean"; the problem below was first stated in print, with von Neumann's name attached, in Day's 1957 paper. Følner gave a combinatorial criterion — a group is amenable exactly when it has finite subsets almost invariant under translation — now usually taken as the definition, and the link to growth.

The organizing question of the classical theory was the von Neumann–Day problem: writing $EG$ for the elementary amenable groups, $AG$ for the amenable groups and $NF$ for the groups with no free subgroup of rank two, one has $EG \subseteq AG \subseteq NF$, and both inclusions were asked to be equalities. Both are strict. Ol'shanskii (1980) showed $AG \neq NF$, and Grigorchuk (1985) showed $EG \neq AG$ with a group of intermediate growth. Chou (1980) supplied the structural facts about $EG$ that the separation rests on.

Amenability is now basic vocabulary in geometric group theory, ergodic theory and operator algebras.

Setting

Let $G$ be a discrete group. A measure on $G$, in von Neumann's sense, is a function $\mu$ assigning a value to every subset of $G$ — not merely to a distinguished $\sigma$-algebra — such that

$$\mu(G) = 1, \qquad \mu(A \sqcup B) = \mu(A) + \mu(B), \qquad \mu(gA) = \mu(A)$$

for all $g \in G$ and all disjoint $A, B \subseteq G$. Only finite additivity is required; countable additivity together with invariance is impossible for a countably infinite group. $G$ is amenable if such a $\mu$ exists.

Two reformulations matter. A left-invariant mean is a positive linear functional $m$ on the bounded real functions $\ell^\infty(G)$ with $m(\mathbf{1}) = 1$ and $m({}_g f) = m(f)$, where ${}_g f(h) = f(g^{-1}h)$. And $G$ satisfies the Følner condition if for every finite $A \subseteq G$ and every $\varepsilon > 0$ there is a finite nonempty $F \subseteq G$ with

$$\frac{|aF \,\triangle\, F|}{|F|} \le \varepsilon \qquad \text{for every } a \in A,$$

where $\triangle$ is symmetric difference. In the Cayley graph this says $F$ has small boundary relative to its size.

Against amenability stands paradoxicality. Two subsets $A, B$ of a $G$-set $X$ are $G$-equidecomposable, written $A \sim B$, if $A$ can be cut into finitely many pieces which, after each is moved by a single element of $G$, reassemble to $B$; and $E \subseteq X$ is $G$-paradoxical if it has two disjoint proper subsets each equidecomposable with $E$ itself. A group that is paradoxical under left translation admits no invariant measure.

Formalization targets

Goal — Theorem 3.6

$$G \text{ satisfies the Følner condition} \iff G \text{ is amenable}$$

This is the goal because it bridges the combinatorial and measure-theoretic sides of the subject, and every later application of amenability to growth uses it in one direction or the other.

Supporting equivalences — Theorems 1.15 and 2.7

For a group $G$, these four are equivalent: $G$ is amenable; there is a left-invariant mean on $\ell^\infty(G)$; $G$ is not paradoxical; and $G$ has the invariant extension property.

Closure properties — Proposition 2.2

Amenability passes to subgroups and quotients, is closed under extensions, and is closed under directed unions; hence all abelian and all virtually solvable groups are amenable, and $EG \subseteq AG$.

Significance

Each of the three equivalent pictures serves a different purpose: the measure gives non-paradoxicality, the mean gives access to functional analysis and fixed-point arguments, and the Følner condition is what one can verify for a concrete group. Theorem 3.8 is the typical consequence — a group of subexponential growth is amenable — proved by exhibiting the balls of the word metric as a Følner sequence, which only the equivalence licenses.

Mathlib has very little of this. It names no definition of amenability: FoelnerFilter.lean says one "has not yet been given" for want of "a general consensus" on the right generality, and writes the property out inline in the conclusion of IsFoelner.amenable, which is one direction of the goal. Equidecomp.lean has the equidecomposition machinery, with a TODO asking for the Schröder–Bernstein theorem for equidecomposability that is Theorem 1.2 here.

This mission supplies the missing definitions, that Schröder–Bernstein theorem, the closure properties, and the direction of the Følner equivalence that is genuinely open. Nothing here is a new mathematical result: all of it is classical, and the work is formalization.

Difficulty

The Følner-implies-amenable direction is the easier one, and the natural construction almost works: given a Følner sequence $F_n$, set $\mu(B) = \lim_n |B \cap F_n| / |F_n|$. That limit need not exist. It must be replaced by a limit along a non-principal ultrafilter, or the measure obtained by compactness in $[0,1]^{\mathcal{P}(G)}$.

The converse — amenable implies Følner — is where the content is, and no averaging argument reaches it. One has to produce, from a mean, finite sets that are almost invariant; the passage runs through a separation theorem in $\ell^1(G)$, the only step here needing a genuinely infinite-dimensional tool. The classical arguments provide no combinatorial route.

Two smaller obstructions are worth naming. Tarski's theorem — an invariant measure giving a set measure one exists precisely when that set is not paradoxical — is quoted without proof in the source and is the hardest single statement in the mission. And Theorem 2.6 rests on a finitely additive extension theorem for measures on a Boolean algebra, which is not the Carathéodory construction in Mathlib; Mathlib's is about outer measures and $\sigma$-additivity.

Formalization scope

Amenability is IsAmenable G: the existence of $m : \mathcal{P}(G) \to [0,\infty]$ with $m(G) = 1$, finitely additive on disjoint pairs, and invariant under left translation. The codomain is the extended nonnegative reals rather than $[0,1]$, to match the conclusion of Mathlib's IsFoelner.amenable — which at $X = G$ with every set measurable is exactly IsAmenable — so that theorem is directly usable; finite additivity and $m(G) = 1$ force $m(s) \le 1$ anyway, so nothing is added or lost.

Committed conventions. Means live on $\ell^\infty(G)$, realised as lp (fun _ : G => ℝ) ∞ — not on all of $G \to \mathbb{R}$, where invariance and normalisation are already contradictory (proved for $\mathbb{Z}$), so every statement about means would be vacuously unprovable. Normalisation is phrased via constantly-$1$ functions, to avoid depending on the ring structure of $\ell^\infty$. Cardinalities use Set.ncard, so no DecidableEq instance propagates into the statements. Paradoxicality is defined for an arbitrary subset, recovering the source's whole-space notion as a special case, because the source states it for the whole space but uses it for subsets throughout. Equidecomposability builds on Mathlib's Equidecomp, and growth on the published Chou_Growth bundle, rather than either being redefined.

One trivialising formalization is ruled out: amenability requiring only $m(G) = 1$ and additivity, without invariance, is satisfied by any normalised counting density and would make the mission vacuous. Left-invariance is part of every definition here, and IsAmenable is exhibited non-vacuously for finite groups.

A complete development needs finitely additive measures on a power set, invariant means on $\ell^\infty$, the Følner condition and sequences, paradoxical decompositions, and a finitely additive extension theorem on a Boolean algebra; the definitions and the last of these are reusable beyond this mission. Contributions are welcome on any milestone. Proposition 2.2's closure properties are the most self-contained entry points, and Theorem 1.2 is the one Mathlib has explicitly asked for.

What is left out

Two bodies of material from the source are deliberately out of scope, left for later missions in this series.

The geometric construction of the Banach–Tarski paradox — that $SO(3,\mathbb{R})$ contains a free group of rank two, the Hausdorff paradox, and the paradoxical decompositions of the sphere and the ball. This mission takes the measure-theoretic half of Section 1 and leaves the half about the $2$-sphere. Tarski's theorem and the Banach–Schröder–Bernstein theorem are in scope despite being printed alongside that material, because both are equidecomposability combinatorics and both are needed by results that are in scope.

The Grigorchuk group — its construction on the binary rooted tree, the proof that it is amenable but not elementary amenable, and its subexponential growth. Theorem 4.2 and Theorem 4.3 are the exceptions, and they enter as references rather than targets.

Also out of scope: the locally compact case. The source gives most definitions for both discrete and locally compact groups, then says it will "mostly focus on discrete groups"; only the discrete case is formalized. Følner nets for uncountable groups are likewise omitted, as is the extension of Example 3.5 to finitely generated abelian groups, which the source leaves as an exercise.

Selected references

• A. Garrido, An introduction to amenable groups, lecture notes, Oxford Advanced Class in Algebra, Michaelmas 2013. archived PDF
• S. Banach and A. Tarski, Sur la décomposition des ensembles de points en parties respectivement congruentes, Fund. Math. 6 (1924), 244–277. DOI
• J. von Neumann, Zur allgemeinen Theorie des Maßes, Fund. Math. 13 (1929), 73–116. DOI
• M. M. Day, Amenable semigroups, Illinois J. Math. 1 (1957), 509–544. DOI
• E. Følner, On groups with full Banach mean value, Math. Scand. 3 (1955), 243–254. DOI
• I. Namioka, Følner's conditions for amenable semi-groups, Math. Scand. 15 (1964), 18–28 — the source of the argument for the goal theorem. DOI
• J. M. Rosenblatt, Invariant measures and growth conditions, Trans. Amer. Math. Soc. 193 (1974), 33–53 — where supramenability is introduced. DOI
• A. Yu. Ol'shanskii, On the problem of the existence of an invariant mean on a group, Russian Math. Surveys 35 (1980), 180–181 — the paper Grigorchuk credits for $AG \neq NF$. DOI
• C. Chou, Elementary amenable groups, Illinois J. Math. 24 (1980), 396–407. DOI
• R. I. Grigorchuk, Degrees of growth of finitely generated groups, and the theory of invariant means, Math. USSR-Izvestiya 25 (1985), 259. DOI
• S. Wagon, The Banach–Tarski Paradox, Cambridge University Press, 1985. DOI