Normed spaces: a ball whose sphere is covered by finite-dimensional faces is plastic

Proved

Plasticity.Faces.hasPlasticUnitBall_of_sphere_covered_normedSpace

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

Let $X$ be a real normed space, not necessarily complete, such that every point of its unit sphere lies in a finite-dimensional face of the closed unit ball $B_X$ contained in the sphere. Then $B_X$ is plastic: every nonexpansive bijection of $B_X$ onto itself is an isometry.

Preamble

import Definitions.Def_Plasticity_Basic
import Definitions.Def_Plasticity_Faces

Formal statement

namespace Plasticity.Faces
theorem hasPlasticUnitBall_of_sphere_covered_normedSpace {X : Type*} [NormedAddCommGroup X] [NormedSpace ℝ X]
    (hcover : ∀ x ∈ Metric.sphere (0 : X) 1, ∃ C : Set X,
      IsSphereFace C ∧ FiniteDimensional ℝ (vectorSpan ℝ C) ∧ x ∈ C) :
    HasPlasticUnitBall X := by sorry
end Plasticity.Faces

Source

This repository: claim F17 (claims/f.md), last sentence; the case X = Y of the card Plasticity.Faces.exists_linearIsometryEquiv_of_sphere_covered_normedSpace

Read-back

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

Read-back. Let $X$ be a real normed space, not necessarily complete. Assume that for every $x \in S_X$ there is a set $C \subseteq X$ with $x \in C$ such that $C$ is a sphere face of $B_X$ (nonempty, convex, contained in $S_X$ , extreme subset of $B_X$ ) and the affine span of $C$ is finite-dimensional. Then the closed unit ball $B_X$ , regarded as a metric space with the distance $\|a - b\|$ inherited from $X$ , is plastic in the repository's sense (HasPlasticUnitBall, IsPlasticSpace): for every map $f : B_X \to B_X$ that is $1$ -Lipschitz ( $\|f(a) - f(b)\| \le \|a - b\|$ for all $a, b \in B_X$ ) and bijective from $B_X$ onto $B_X$ , $f$ is an isometry, that is $\|f(a) - f(b)\| = \|a - b\|$ for all $a, b \in B_X$ .

Lean conventions that change meaning. None that I found. The ball is a subtype with the induced metric, LipschitzWith 1 on the subtype is the same as $1$ -Lipschitz on $B_X$ , Function.Bijective is bijectivity of $B_X$ onto itself, and Mathlib's Isometry (preservation of extended distance) is preservation of distance. The conclusion asserts only that $f$ preserves distances; it does not assert linearity or that $f$ extends to a linear isometry (that stronger form is card 1 with $Y = X$ ).

Degenerate cases. If $X = 0$ , the hypothesis is vacuous and $B_X = \{0\}$ is trivially plastic. For finite-dimensional or strictly convex $X$ the hypothesis holds automatically by (O2).

Hypotheses. The single hypothesis (covering of $S_X$ by finite-dimensional sphere faces) is not known to be removable: without it the statement is plasticity of the unit ball of every real normed space, an open problem even for Banach spaces as far as I know. Its finite-dimensionality clause is the substantive part, by (O2).

Name. Accurate for the conclusion; normedSpace signals the absence of completeness. As in card 1, sphere_covered omits "by finite-dimensional faces".

Truth. It is a direct corollary of card 1 with $Y = X$ (extend $f$ to $F : X \to X$ by any values off $B_X$ ; bijectivity and the Lipschitz bound give the hypotheses of card 1, and the linear isometry $T$ preserves distances). So I believe it true exactly to the extent that I believe card 1.

Human review

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

View graph