A ball whose sphere is covered by finite-dimensional faces is plastic

Proved

Plasticity.Faces.hasPlasticUnitBall_of_sphere_covered

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

Let $X$ be a real Banach space 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 {X : Type*} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace 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

Read-back

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

Read-back. Let $X$ be a real Banach space such that every $x \in S_X$ lies in some sphere face $C$ of $B_X$ (nonempty, convex, $C \subseteq S_X$ , extreme subset of $B_X$ ) whose span of $C - C$ is finite-dimensional. Then the closed unit ball $B_X$ , with the metric $\|a - b\|$ , is plastic: every map $f : B_X \to B_X$ that is bijective and satisfies $\|f(a) - f(b)\| \le \|a - b\|$ for all $a, b \in B_X$ in fact satisfies $\|f(a) - f(b)\| = \|a - b\|$ for all $a, b \in B_X$ .

Flags.

Conventions. "Plastic" and "isometry" are unfolded from the audited Def_Plasticity_Basic; bijectivity is of $f$ as a self-map of the ball. For $X = 0$ the hypothesis is vacuous and the conclusion trivially true.
Hypotheses. Completeness is assumed; nothing missing.
Name. Accurate.
Truth. Not refuted; not verified. It follows from exists_linearIsometryEquiv_of_sphere_covered with $Y = X$ (extend $f$ arbitrarily off the ball). It covers finite-dimensional $X$ (known by compactness) and strictly convex $X$ (singleton faces; known).

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