The mathematical claim
CLAIM PRESENTED IN THE BRIEF REPORT
Finite-dimensional real normed spaces with isometric unit spheres are linearly isometric as normed spaces.
This is an existence statement about the two spaces. It is not a claim that a prescribed sphere isometry extends to a linear isometry.
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.
Scope and evidence
No equivalent result was identified in the sources examined through 15 September 2026. This is not a novelty certificate or a guarantee that no earlier result exists.
Scope and evidence
Full human verification of the Sphere Rigidity Brief Report, Draft R1, has not been completed. An AI-assisted review of the written argument was recorded on 10 September 2026; this is not human verification or journal peer review.
Scope and evidence
The exact MathlibAnnex v0.2.0 source release includes the Sphere Rigidity Project entry and source manifest. Its pinned qualification is recorded separately from human review and Brief Report correspondence.
Scope and evidence
The correspondence between the Sphere Rigidity Brief Report, Draft R1, and the Lean formalization has not yet been checked in full.
Scope and evidence
The progressive Research Companion is available in HTML, PDF and JSON. Its 467 exact declarations are not provisional Cards; public Declaration Cards remain zero.
Scope and evidence
The preliminary Brief Report is available as a PDF. Full human mathematical verification and Brief↔Lean semantic correspondence remain incomplete. Conventional paper, arXiv and DOI milestones remain separate.
Report and related materials
The Brief Report is a preliminary mathematical record. Its preparation date is distinct from publication and review dates.
File details
- Size
- 411,489 bytes
- SHA-256
7eabe530c8ab74462515797325044ab5128a752a66c44581df9c5551ea07df1d
File details
- Size
- 192,068 bytes
- SHA-256
00fe9df433dc0ca5c20824f5fb688555ec6206d3b66a3a52789eb085d4321221
Brief Report publication record
Prepared: 10 September 2026. First published: 17 September 2026.
Responsible for publication: Ryotaro Tanaka. This role covers release, versioning, corrections, and withdrawal; it does not constitute mathematical authorship or independent verification. Issued by Exact Mathematics with AI.
The Brief Report has no named author. Citation metadata and authorless reference examples.
Formalization and LFH
The formal source is the MathlibAnnex v0.2.0 release, commit 30963f26ac8ffa3dc3e9ec9de91fd0f9daf05305, tree b3378851a5287f5e3c8418f668e4d0ba52718739. Project entry · Project Source Manifest.
The progressive Research Companion is available here: HTML · PDF · JSON. Its 467 exact declaration nodes do not create provisional Cards.
Correspondence between the Brief Report and this Lean release remains pending. The Project view records source structure; it is not a completed document alignment or human verification.
Prior-art search
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
- 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.
- 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. Its footer reads “AI-assisted manuscript · Human verification incomplete”. 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 imply that full human verification has been completed.
Related formalization materials.
The MathlibAnnex v0.2.0 formal source is public. The progressive Research Companion is available here in HTML, PDF and JSON. Public Declaration Cards remain zero, and correspondence between the Brief Report and Lean source remains pending.
Comments and collaborative verification.
Comments, corrections, and proposals for collaborative verification are welcome. Editable manuscript files may be shared individually by agreement.
Read about MathlibAnnexRecord history
PDF-only report distribution
The website provides the report as a PDF. Editable manuscript sources are retained privately. The report bytes and mathematical review status are unchanged.
Brief Report, Draft R1, prepared
The 22-page preliminary Brief Report and conventional manuscript incorporated the same local corrections. Preparation alone did not establish full human verification.
AI textual review recorded
Statements and proof applications were re-examined, with eight groups of local corrections recorded. Full human verification and a new Lean build were not performed.
Website record prepared
Initial presentation and status fields were prepared. This entry is not a mathematical review or a new Lean build.