Papers With

← All papers
First page of Rigidity of unit spheres in finite-dimensional real normed spaces

Rigidity of unit spheres in finite-dimensional real normed spaces

Jumpei Nakamura, Ryotaro Tanaka

math.FA Sep 25, 2026 · v1
formalization mathlib analysis geometry
Read PDF arXiv abstract Code
TL;DR
The sphere rigidity theorem is formalized in Lean 4 with Mathlib, released in MathlibAnnex v0.4.0, with AI tools assisting the Lean code.
Abstract
We prove that finite-dimensional real normed spaces with isometric unit spheres are linearly isometric, where each sphere carries the distance induced by the ambient norm. This answers the object-level question of Kadets and Martín in finite dimensions, without asserting linear extension of a prescribed sphere isometry. We associate with each norm a family of Plücker contraction bodies generated by volume-normalized maximal minors of linear contractions into finite-dimensional $\ell_\infty$ spaces. Null-Lagrangian identities show that the sphere metric determines these bodies. A finite exposed-face construction recovers almost-norming contractions from the convexified data, and compactness together with an exact volume identity yields a linear isometry.
Problem

Kadets and Martín asked whether two real normed spaces with isometric unit spheres must be linearly isometric. Each sphere carries the metric induced by the ambient norm. The question is open even in finite dimensions.

Approach

Each norm is assigned a family of Plücker contraction bodies, built from volume-normalized maximal minors of linear contractions into finite-dimensional ℓ_∞ spaces. Null-Lagrangian (Piola) boundary-trace identities and an orientation argument show that the sphere metric determines these bodies. A finite exposed-face construction then recovers almost-norming contractions with exact determinant–volume identities, and compactness gives an exact isometry. The result is also formalized in Lean 4 using Mathlib.

Results

Finite-dimensional real normed spaces with isometric unit spheres are linearly isometric, with no smoothness, strict convexity or polyhedrality assumptions. The theorem does not claim that the given sphere isometry itself extends linearly. A machine-checked Lean formalization is available in MathlibAnnex v0.4.0.