Tingley's sphere-isometry extension

Source and verification

This article explains family 322 of the October 6, 2026 OpenAI collection. Research conclusions are attributed to its manuscripts. The review covers statements, introductions, and selected proof mechanisms; it is not an independent verification of the complete proofs.

Overview

A unit sphere records distances between unit vectors, but a linear map must also preserve distances between vectors of different lengths. Family 322 claims that this missing radial information is already determined by every surjective sphere isometry between real Banach spaces. Its argument measures the failure of the natural radial extension, realizes a maximal failure, and turns it into an impossible pair of aligned chords. (OpenAI, 2026)

🏷️ Preliminaries: sphere geometry and linear extensions

A real Banach space is a complete real normed vector space. Write $S_X=\{x:\Vert x\Vert =1\}$. A surjective sphere isometry is an onto map $f:S_X\to S_Y$ satisfying $\Vert f(x)-f(y)\Vert =\Vert x-y\Vert$.

Any linear extension is forced to equal the radial map

$$\begin{array}{c}T(0)=0,\\ T(x)=\Vert x\Vert f(x/\Vert x\Vert )(x\ne 0).\end{array}$$

This formula preserves norms, is onto, and preserves distances between points of the same radius. It does not by itself prove additivity.

For Hilbert spaces, polarization explains why the assertion is plausible. For unit vectors,

$$⟨x,y⟩=1-\frac{1}{2}\Vert x-y{\Vert }^2.$$

The sphere map preserves these inner products. Consequently, for positive $r,s$,

$$\begin{array}{c}\Vert rf(x)-sf(y){\Vert }^2\\ =r^2+s^2-2rs⟨x,y⟩\\ =\Vert rx-sy{\Vert }^2.\end{array}$$

This proves that the radial extension is an onto isometry. General norms have no such inner-product identity; recovering unequal-radius distances is the research problem.

Manuscript claim

For every pair of nonzero real Banach spaces, every surjective isometry of their unit spheres has a unique surjective real-linear isometric extension. No separability, finite-dimensionality, reflexivity, smoothness, or strict convexity is assumed. (OpenAI, 2026)

For complex spaces considered as real spaces, the conclusion remains real linearity. Complex conjugation on $\mathbb{C}$ shows why complex linearity cannot follow from distances alone.

🏷️ The radial defect

For unit vectors $x,y$ and $0\le q\le 1$, define

$$\begin{array}{c}{D}_q(x,y)\\ =\Vert f(x)-qf(y)\Vert -\Vert x-qy\Vert ,\\ M=\underset{x,y,q}{\sup }|D_q(x,y)|.\end{array}$$

The reverse triangle inequality makes each of the two terms $1$-Lipschitz in $q$. Since $D_0=D_1=0$,

$$\begin{array}{c}|D_q(x,y)|\le 2\min (q,1-q),\\ M\le 1.\end{array}$$

Thus a positive defect must occur away from the two endpoint radii.

If $M=0$, unequal-radius distances follow by factoring out the larger radius. For $r\ge s>0$,

$$\begin{array}{c}\Vert T(rx)-T(sy)\Vert \\ =r\Vert f(x)-(s/r)f(y)\Vert \\ =\Vert rx-sy\Vert .\end{array}$$

The whole theorem therefore reduces to eliminating $M>0$.

A supremum need not be attained in an infinite-dimensional space. The manuscript passes to a Banach-space limit construction: bounded sequences are identified when their norm difference tends to zero along a fixed ultralimit. Applying $f$ coordinatewise preserves sphere distances in this construction. Maximizing sequences become actual unit vectors attaining the defect, while the bound by $M$ survives for every pair and every radius. Replacing $f$ by its inverse changes the sign of the defect, so the attained defect may be taken positive. This is an analytic compactness device; it does not assume compactness of the original sphere.

🏷️ Common supports and aligned chords

A supporting functional at a unit vector $v$ is a linear functional $\phi$ with $\Vert \phi \Vert \le 1$ and $\phi (v)=1$. Hahn–Banach supplies such functionals. If

$$\Vert \alpha v+\beta w\Vert =\alpha +\beta ,\alpha ,\beta >0,$$

a functional norming this sum must take value one at both $v$ and $w$: each value is at most one, and their positively weighted average attains its maximum.

This equality case propagates the maximal-defect condition. Fix an interior center $ty$, $0<t<1$. Every ray from it has a unique sphere contact, at a distance between $1-t$ and $1+t$. Map that contact using $f$, take the opposite contact through $tf(y)$, and pull it back. The resulting return map acts on directions.

The manuscript constructs a nonempty closed bounded convex set of extremal directions invariant under this map. It then proves contraction of the measure of noncompactness, rather than contraction of ordinary distances. For a bounded set $H$, this measure is the infimum of diameters needed in a finite cover of $H$. Darbo’s fixed-point theorem turns the strict contraction of this measure into a fixed direction.

At that direction the two chords are aligned:

$$\begin{array}{c}x=ty+pv,z=ty-rv,\\ f(x)=tf(y)+sw,\\ f(z)=tf(y)-uw,\end{array}$$

with positive radii satisfying

$$\begin{array}{c}s-p=r-u=M,\\ p+r=s+u\le 2.\end{array}$$

These equalities encode a transfer of length from one half of a chord to the other. The source’s final geometric comparison rules it out: one parameter regime permits a radial perturbation with defect larger than $M$; the other contradicts a preserved sphere distance using convexity. The invariant-set construction, quantitative noncompactness estimate, and this final comparison are the substantive manuscript inputs, not consequences of Hahn–Banach alone.

🏷️ From metric preservation to real linearity

Once $T$ is an onto isometry fixing zero, the classical Mazur–Ulam argument gives linearity. Its key observation is that reflection about a target midpoint, conjugated by an onto isometry, doubles any midpoint defect. All such defects for a fixed pair have a common distance bound; repeated doubling therefore forces the defect to vanish.

Midpoint preservation and $T(0)=0$ imply additivity and rational homogeneity. Continuity extends rational homogeneity to every real scalar. Uniqueness was already forced by the radial formula.

🏷️ Key steps and proof outlines

Attainment preserves the full defect bound

Choose sphere pairs and radii whose absolute defects tend to $M>0$. Pass to a subsequence with the same sign of defect and, if necessary, replace the isometry by its inverse. The radii have a convergent subsequence in $[0,1]$; the endpoint estimate forces their limit $t$ into $(0,1)$.

In the ultrapower, the norm of a bounded sequence is the ultralimit of its norms after quotienting zero-norm sequences. Sphere elements can be represented by unit vectors by normalizing a representative on the indices where its norm is nonzero. Applying the original sphere map coordinatewise is therefore well-defined and remains onto and distance preserving. The uniform Lipschitz estimate in the radius permits replacing the varying radii by $t$. The maximal pair now attains defect $M$, while the original inequality $|D_q|\le M$ survives for every new sphere pair and every $q$. This last universal bound is needed for the later perturbation contradiction. (OpenAI, 2026)

Condensing the return map produces aligned extremal chords

The interior center $ty$ determines a continuous contact-radius function $\rho (v)$ by $\Vert ty+\rho (v)v\Vert =1$. Convexity and interiority give a unique positive contact on each ray, with $1-t\le \rho (v)\le 1+t$. Supporting functionals propagate equality in the extremal-defect inequalities and define an invariant convex set of directions.

The return map need not contract norm distance. Its estimate includes a strictly contracting term plus errors depending on two bounded scalar radii. To estimate the measure of noncompactness, start with a finite diameter cover and refine every piece according to fine bins of those two radii. On each refined piece the scalar errors are arbitrarily small, while the diameter term contracts by a fixed factor $\gamma <1$. Thus $\chi (gH)\le \gamma \chi (H)$.

Taking successive closed convex hulls of the images gives nested bounded convex sets with measures of noncompactness tending to zero. Their intersection is nonempty and compact, and the return map preserves it. A compact convex fixed-point theorem then supplies a fixed direction. This explains why the scalar errors do not obstruct the fixed-point argument and why ordinary Banach contraction is not the theorem being used.

A secant estimate splits the chord contradiction into two regimes

Use the aligned-chord notation above and put $d=p+r=s+u$, $A=p/d$, $B=u/d$, and $ϵ=1-t$. Then $A+B=1-M/d<1$. The source compares defects at radii $t-sh$ and $t+uh$, where

$$h=\min (t/s,ϵ/u).$$

Both radii are admissible and at least one is an endpoint with zero defect. A weighted sum cancels the common target norm and bounds a secant slope of the source norm. Supporting functionals bound that secant from below. The result is $ϵ/p\le K$, with $K\le 1-B$ when $B\le ϵ$ and $K\le B$ otherwise.

If $B>ϵ$, the support inequalities force every support at $v$ to be negative on $y$. Applying the same argument to the inverse configuration exchanges $A$ and $B$ and forces supports at the target direction $w$ to be positive on $f(y)$. A small decrease of radius then strictly decreases the source norm and strictly increases the target norm, producing defect greater than $M$. Hence both $A,B\le ϵ$.

The remaining regime contradicts one preserved sphere distance

Apply the secant estimate in both directions to obtain

$$ϵ\le dA(1-B),ϵ\le dB(1-A).$$

Since $A+B<1$ and $d\le 2$, these imply $ϵ<1/2$ and the needed ordering of chord ratios. Define convex functions $F(\lambda )=\Vert y+\lambda v\Vert$ and $G(\lambda )=\Vert f(y)+\lambda w\Vert$. Their values at zero are one, and the unit endpoint identities give $F(p/t)=G(s/t)=1/t$.

Monotonicity of secant slopes forces $F(r/ϵ)>1/t$, whereas convexity on the shorter target interval gives $G(u/ϵ)\le 1/t$. But preservation of the sphere distance from $y$ to $z$ says these two values are equal after multiplication by $ϵ$. This contradiction eliminates $M>0$. The radial extension is therefore an onto isometry, and Mazur–Ulam supplies real linearity as explained earlier.

See Also

• Bi-Lipschitz equivalence allows multiplicative distortion and leads to a very different relation between metric and linear structure.
• Nonexpansive fixed points uses a different compactness mechanism; Darbo’s condensing hypothesis here should not be confused with mere nonexpansiveness.

🏷️ Manuscripts and verification scope

• A positive solution to Tingley’s problem — pinned manuscript and companion source.

The family scope page describes selected formalization coverage. The documented selection states the unique real-linear extension for arbitrary nonzero real Banach spaces. It does not assert complex linearity. No Lean build, axiom audit, or manuscript-to-formal-statement equivalence check was performed for these notes.

OpenAI collection provides prerequisites and the reading sequence; coverage register records completed and pending families.

🐻  OpenAI 2026. A positive solution to Tingley’s problem.