Quantitative common-face rigidity: $\|H-I\|_\infty\le\min\{2,4\varepsilon^{1/3}\}$

Proved

Plasticity.A01_quant

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

Let $X$ be a real Banach space with closed unit ball $B_X$ and unit sphere $S_X$ , let $\varepsilon\ge0$ , and let $H\colon B_X\to B_X$ be $(1+\varepsilon)$ -Lipschitz. If $\|a+H(a)\|=2$ for every $a\in S_X$ , then

\sup_{x\in B_X}\|H(x)-x\|\le\min\{2,\,4\varepsilon^{1/3}\}.

For $\varepsilon=0$ this is the exact form (card Plasticity.A01). No injectivity or surjectivity of $H$ is assumed.

Preamble

import Mathlib.Analysis.Normed.Module.Basic
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Topology.EMetricSpace.Lipschitz

Formal statement

namespace Plasticity
theorem A01_quant {X : Type*} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X]
    (ε : NNReal) (H : X → X)
    (hmaps : Set.MapsTo H (Metric.closedBall (0 : X) 1) (Metric.closedBall (0 : X) 1))
    (hlip : LipschitzOnWith (1 + ε) H (Metric.closedBall (0 : X) 1))
    (halign : ∀ a ∈ Metric.sphere (0 : X) 1, ‖a + H a‖ = 2) :
    ∀ x ∈ Metric.closedBall (0 : X) 1, ‖H x - x‖ ≤ min 2 (4 * (ε : ℝ) ^ ((1 : ℝ) / 3)) := by sorry
end Plasticity

Source

This repository: claim A01 (claims/a.md), displayed quantitative form; proof in expositions/universal/conjugated_contractions.md §2 (Lemma 2.1), using the rate sup‖Pⁿx−K(Pⁿx)‖ ≤ 2/√(πnα(1−α)) for averaged nonexpansive maps (Cominetti–Soto–Vaisman, arXiv:1206.4195, Theorem 1)

Read-back

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

Declaration Plasticity.A01_quant (theorem; proof omitted). Let $X$ be any real Banach space: a real normed vector space with norm $\|\cdot\|$ that is complete. No other assumption is made on $X$ : it may be of any dimension, including the zero space $X=\{0\}$ , and no smoothness, strict convexity, separability or finite-dimensionality is assumed. Write $B=\{x\in X:\|x\|\le 1\}$ for the closed unit ball and $S=\{a\in X:\|a\|=1\}$ for the unit sphere. Let $\varepsilon\ge 0$ be a nonnegative real number, and let $H:X\to X$ be an arbitrary function defined on all of $X$ (only its values on $B$ are constrained below). Assume the following three hypotheses.

$H$ maps the ball into the ball: $H(x)\in B$ , i.e. $\|H(x)\|\le 1$ , for every $x\in B$ . Nothing is assumed about surjectivity onto $B$ , injectivity, or invertibility.
$H$ is $(1+\varepsilon)$ -Lipschitz on the ball: for all $x,y\in B$ ,

\|H(x)-H(y)\|\le (1+\varepsilon)\,\|x-y\|.

The constant is $1+\varepsilon$ , not $1$ ; when $\varepsilon=0$ this is nonexpansiveness on $B$ . 3. Sphere alignment: for every $a\in S$ ,

\|a+H(a)\|=2.

Together with hypothesis 1 and the triangle inequality $\|a+H(a)\|\le \|a\|+\|H(a)\|\le 2$ , this forces $\|H(a)\|=1$ for every $a\in S$ , i.e. $H$ maps the sphere into the sphere, and the midpoint $\tfrac12(a+H(a))$ is also a unit vector. It does not by itself force $H(a)=a$ (that would need strict convexity, which is not assumed).

Conclusion. For every $x\in B$ ,

\|H(x)-x\|\;\le\;\min\Bigl\{\,2,\;4\,\varepsilon^{1/3}\Bigr\},

where $\varepsilon^{1/3}$ is the ordinary nonnegative real cube root of $\varepsilon$ (the exponent is the real number $1/3$ , not an integer quotient). The constants $2$ , $4$ and $1/3$ are absolute: the same bound holds for every space $X$ , every $\varepsilon$ and every $H$ satisfying the hypotheses.

Edge cases and effective strength.

$\varepsilon=0$ : since $0^{1/3}=0$ , the right-hand side is $\min\{2,0\}=0$ , so the statement asserts that every nonexpansive self-map of $B$ satisfying the sphere-alignment condition is the identity on $B$ : $H(x)=x$ for all $x\in B$ . No bijectivity, surjectivity or condition on $H(0)$ is assumed in this case either.
$\varepsilon\ge 1/8$ : then $4\varepsilon^{1/3}\ge 2$ , the right-hand side equals $2$ , and the conclusion $\|H(x)-x\|\le 2$ already follows from hypothesis 1 alone, since $\|H(x)-x\|\le\|H(x)\|+\|x\|\le 2$ . The statement therefore carries content only for $0\le\varepsilon<1/8$ , where the bound reads $\|H(x)-x\|\le 4\varepsilon^{1/3}<2$ .
Trivial space $X=\{0\}$ : $S$ is empty, so hypothesis 3 is vacuous; $B=\{0\}$ and hypothesis 1 forces $H(0)=0$ ; the conclusion $0\le\min\{2,4\varepsilon^{1/3}\}$ holds.
Satisfiability: the hypotheses are not contradictory; for example the identity map $H(x)=x$ satisfies all three for every $\varepsilon\ge 0$ and every $X$ .
Behaviour off the ball: values of $H$ outside $B$ are unrestricted and do not enter the conclusion, which concerns only points $x\in B$ .

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

Quantitative common-face rigidity: ∥H−I∥∞≤min⁡{2,4ε1/3}\|H-I\|_\infty\le\min\{2,4\varepsilon^{1/3}\}∥H−I∥∞​≤min{2,4ε1/3}

Quantitative common-face rigidity: $\|H-I\|_\infty\le\min\{2,4\varepsilon^{1/3}\}$