Sphere coverage suffices: a nonexpansive ball map restricting to a surjection of unit spheres is a linear isometry

Proved

Plasticity.U16

by scanstone · Oct 14, 2026 · Mathlib 0df444a (Lean v4.33.1)

Let $X$ and $Y$ be nonzero real Banach spaces and let $F\colon B_X\to B_Y$ be a nonexpansive map of their closed unit balls. If $F(S_X)\subseteq S_Y$ and every unit vector of $Y$ is the image of some point of $B_X$ , then $F$ is the restriction to $B_X$ of a surjective real-linear isometry $T\colon X\to Y$ . Coverage of interior targets, injectivity and inverse regularity are not assumed.

Preamble

import Mathlib.Analysis.Normed.Module.Basic
import Mathlib.Analysis.Normed.Operator.LinearIsometry
import Mathlib.Topology.EMetricSpace.Lipschitz

Formal statement

namespace Plasticity
theorem U16 {X Y : Type*} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] [Nontrivial X]
    [NormedAddCommGroup Y] [NormedSpace ℝ Y] [CompleteSpace Y] [Nontrivial Y]
    (F : X → Y)
    (hmaps : Set.MapsTo F (Metric.closedBall (0 : X) 1) (Metric.closedBall (0 : Y) 1))
    (hlip : LipschitzOnWith 1 F (Metric.closedBall (0 : X) 1))
    (hsphere : Set.MapsTo F (Metric.sphere (0 : X) 1) (Metric.sphere (0 : Y) 1))
    (hcover : Metric.sphere (0 : Y) 1 ⊆ F '' Metric.closedBall (0 : X) 1) :
    ∃ T : X ≃ₗᵢ[ℝ] Y, Set.EqOn F T (Metric.closedBall (0 : X) 1) := by sorry
end Plasticity

Source

This repository: claim U16 (claims/u.md); proof in expositions/sphere_coverage_general.md §1, with U10 §§1–3 and the Bishop–Phelps theorem

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Setting. Identical to U10: $X$ and $Y$ are real Banach spaces (real normed spaces that are complete), each nontrivial (each contains a nonzero vector), with no assumed relationship between them. Write

B_X = \{x \in X : \|x\| \le 1\},\quad S_X = \{x \in X : \|x\| = 1\},\qquad B_Y,\ S_Y \text{ likewise in } Y.

$F : X \to Y$ is an arbitrary function on all of $X$ ; only its values on $B_X$ matter. No continuity, linearity or injectivity of $F$ is assumed.

Hypotheses.

$F$ maps the ball into the ball: $F(B_X) \subseteq B_Y$ .
$F$ is $1$ -Lipschitz on the ball: $\|F(x) - F(x')\| \le \|x - x'\|$ for all $x, x' \in B_X$ .
$F$ maps the unit sphere into the unit sphere: $\|F(x)\| = 1$ whenever $\|x\| = 1$ .
The image of the ball covers the unit sphere of $Y$ : every $y \in Y$ with $\|y\| = 1$ equals $F(x)$ for some $x \in X$ with $\|x\| \le 1$ (i.e. $S_Y \subseteq F(B_X)$ ). The preimage point $x$ is only required to lie in the ball, not necessarily on $S_X$ .

Unlike U10, it is not assumed that $F(B_X)$ contains all of $B_Y$ ; only the sphere $S_Y$ must be covered.

Conclusion. There exists a linear isometric isomorphism $T : X \to Y$ — an $\mathbb{R}$ -linear bijection from $X$ onto $Y$ with $\|T x\| = \|x\|$ for every $x \in X$ — such that

F(x) = T(x) \quad \text{for every } x \in B_X.

In particular the conclusion asserts that $X$ and $Y$ are linearly isometric. Nothing is asserted about $F$ outside $B_X$ .

Human review

Endorsed by Shuze Chen · Oct 14, 2026
Confirmed by the moderator at approval.
Endorsed by scanstone · Oct 14, 2026
Confirmed by the mission captain (proposal self-audit).

View graph