Sphere Rigidity

The mathematical claim

Verification record

These entries refer to different aspects of the project. They must not be combined into a single claim that this brief report is verified.

Report and related materials

The Brief Report is a preliminary mathematical record. Its preparation date is distinct from publication and review dates.

Comments, corrections, and collaborative verification are welcome. People and contact

Formalization and LFH

MathlibAnnex source v0.4.0 is public, at commit 437e6e46228bbb8e91211ebded349d7a30020e73. Recorded source qualification is separate from manuscript correspondence.

The Research Companion presents 75 approved Cards, with separate exploration of 467 exact source declarations: Open Companion · PDF · JSON.

The Brief Report mapping is mechanical; whole-document correspondence remains pending.

Version and publication record

Draft R2 published 21 Sept 2026. Draft R1 was first published on 17 September 2026.

Brief Report publication responsibility: Ryotaro Tanaka. No mathematical author is designated for the Brief Report. Citation metadata · Version history.

Prior-art search

The search record below retains its original cutoff. See Related work for the comparison with the subsequently identified OpenAI preprint.

Documented through 15 September 2026 · AI-assisted

Kadets and Martín explicitly separated the object-level question from Tingley’s marked extension problem: if two finite-dimensional normed spaces have isometric unit spheres, must the spaces themselves be linearly isometric? Their paper proves the marked extension result for polyhedral spaces and poses the broader object-level question [1, §5].

The search examined that paper, selected cited and citing literature, later work on Tingley’s problem, recent preprints, and broader searches under adjacent formulations. No source examined was identified as stating or clearly implying the same theorem for all finite-dimensional real normed spaces. The closest general inspected result covers every two-dimensional real Banach space [2]; other inspected results require special classes or additional hypotheses.

This is a record of the sources examined, not a guarantee that no earlier result exists. See the Prior-Art Search Note (PDF) for the search scope, limitations, method context, and update rule.

Selected references

1. V. Kadets and M. Martín, “Extension of isometries between unit spheres of finite-dimensional polyhedral Banach spaces,” Journal of Mathematical Analysis and Applications 396 (2012), 441–447, especially §5. DOI: 10.1016/j.jmaa.2012.06.031.
2. T. Banakh, “Every 2-dimensional Banach space has the Mazur–Ulam property,” Linear Algebra and its Applications 632 (2022), 268–280. DOI: 10.1016/j.laa.2021.09.020.

About the report

A standalone mathematical record.

The brief report contains the statements, proofs, necessary notation, and references. Published editions retain their original version-specific notices. Subsequent Lean, library, and paper milestones belong to this project record; they do not require a new report edition unless the report itself changes.

AI assistance and human direction.

The research direction and revisions were developed through human–AI dialogue. AI contributed substantially to proof development and manuscript preparation. This description does not change the stated scope of the available evidence.

Reusable tools on a separate path.

MathlibAnnex v0.4.0 is public. Its Research Companion records the exact formal source structure separately from Brief Report correspondence.

Comments and collaborative verification.

Comments, corrections, and proposals for collaborative verification are welcome. Editable manuscript files may be shared individually by agreement.

Record history