AI 辅助证明 Banach 空间单位球非扩张映射的等距刚性，并公开两个 Lean 形式化核心结论

Kaarel August Kurik 10 月 20 日首发研究：对实 Banach 空间 X、Y，若单位球之间的非扩张映射 F 将源单位球面映入目标单位球面、且其像覆盖目标球面，则 F 必是一个满射线性等距的限制。论文以量化刚性引理和 Baillon–Bruck 渐近正则性为核心，并得出单位球等距映射的极点结论，回答 Bargetz、Dymond、Pirk 的有关问题。arXiv 注明证明研究使用 AI 语言模型，定理 1 和引理 2 提供 Lean 形式化链接；并未宣称整篇论文每一个推论已被 Radar 复现或得到独立审稿。