结果族 322：Tingley’s sphere-isometry problem · 学科：Functional analysis · 验证状态：主结果已 Lean 形式化
只给你一只球的外壳，并告诉你壳面上任意两点的直线距离，你能据此重建整个三维空间、连同它的线性结构吗？Tingley 在 1987 年问：两个赋范空间的单位球面之间若存在保持距离的一一对应，它是否必然来自某个线性等距算子？本文给出肯定回答，且不设任何维数、可分性或光滑性限制。
关键词卡片
@@M@@T(x)=\|x\|\,f(x/\|x\|)@@，把球面对应沿射线按比例放大到全空间。看个具体例子
扩张方式像太阳光线：壳面上的点如何对应，同一条射线上的内部点就按比例照搬，比如半径一半处的 @@M@@t\cdot x@@ 映到 @@M@@t\cdot f(x)@@：
定理断言这样定义的 T 必是满的实线性等距：外壳的度量几何完全决定内部结构。此前结论只对 @@M@@\ell^p@@、@@M@@L^p@@、C*-代数等具体空间逐类成立。
为什么值得关心
三十余年的逐类验证就此收官为一条无限制的一般定理，”球面决定空间”从经验升级为定律。
已 Lean 形式化
第一级台阶
导读问：”只给球的外壳和壳面距离，能否重建整个空间？”换成半数学的话：研究对象是带范数的向量空间及其单位球壳；已知数据是两个球壳之间一对一、到上、且保持任意两点直线距离的对应；问题是这个对应是否必然由整个空间之间的某个线性等距算子逐点导出。导读里”太阳光线照搬”的直觉对应一个自然的候选公式：同一射线上的内部点按半径比例照搬壳面上的对应关系。
第二级台阶
用本科术语精确化。实赋范空间 @@M@@X@@ 的单位球面是 @@M@@S_X=\{x:\|x\|=1\}@@；满等距 @@M@@f:S_X\to S_Y@@ 指双射且保持距离。候选的径向扩张定义为 @@M@@T(0)=0@@、@@M@@T(x)=\|x\|\,f(x/\|x\|)@@（@@M@@x\neq0@@）。它天然保范、也保持同一半径上的距离；全部困难在恢复不同半径的点之间的距离。收官工具是 Mazur–Ulam 定理：整个空间之间的满等距自动仿射，故一旦 @@M@@T@@ 被证明保距，线性免费跟进。
第三级台阶
定理的语境是：@@M@@X,Y@@ 取任意非零实 Banach 空间——不设维数、可分性、光滑性、严格凸性任何限制，这一宽松舞台正是问题悬置三十余年的原因；此前的肯定答案都限于 @@M@@\ell^p@@、@@M@@L^p@@、@@M@@C^*@@-代数等具体类别。主定理断言：上述径向映射 @@M@@T@@ 必是 @@M@@X@@ 到 @@M@@Y@@ 的满实线性等距，且是 @@M@@f@@ 唯一的线性扩张。结论对复 Banach 空间按实空间理解时给出实线性，不断言复线性。证明以”亏损”@@M@@D_q(x,y)=\|f(x)-qf(y)\|-\|x-qy\|@@ 的上确界 @@M@@M@@ 为纲：只要证 @@M@@M=0@@，径向映射便保距，Mazur–Ulam 完成收尾。
本文肯定地解决了 Tingley 问题：实 Banach 空间单位球面之间的满等距映射必可唯一扩张为全空间上的满实线性等距算子，且对维数、可分性、光滑性均无限制——单位球面的度量几何在线性等距意义下完全决定整个空间。
对实赋范空间 @@M@@X@@，记单位球面（unit sphere）@@M@@S_X=\{x:\norm{x}=1\}@@，距离继承自 @@M@@X@@。1987 年 Tingley 提出：球面间的满等距映射（surjective isometry）@@M@@f:S_X\to S_Y@@ 是否总能扩张（extension）为全空间之间的线性等距？经典工具在此失灵：Mazur–Ulam 定理（1932）只处理整个空间之间的满等距，Mankiewicz（1972）的推广要求凸集具有非空内部，而球面在所在空间中没有内部。Tingley 原文仅在有限维证明了对径点（antipodal points）被保持，即 @@M@@f(-x)=-f(x)@@。此后三十余年，@@M@@\ell^p@@、@@M@@L^p@@ 等序列与函数空间，@@M@@C^*@@-代数、von Neumann 代数，以及二维空间等具体空间类相继获得肯定答案，但完全不设限制的一般情形始终悬而未决。
主定理（main.tex，定理 1.1）：设 @@M@@X,Y@@ 为非零实 Banach 空间，@@M@@f:S_X\to S_Y@@ 是满等距映射，则径向映射
@@M@@DT(0)=0,\qquad T(x)=\norm{x}\,f\Bigl(\frac{x}{\norm{x}}\Bigr)\quad(x\ne0)@@
是 @@M@@X@@ 到 @@M@@Y@@ 的满实线性等距算子，且是 @@M@@f@@ 唯一的线性扩张。候选映射 @@M@@T@@ 天然保范、保同一半径上的距离，全部困难在于从单个球面的度量恢复不同半径的点之间的距离。空间可以是任意维数，不必可分、自反、光滑或严格凸；复 Banach 空间视为实空间时结论是实线性，不断言复线性。
全文围绕亏损（defect）@@M@@D_q(x,y)=\norm{f(x)-qf(y)}-\norm{x-qy}@@（@@M@@x,y\in S_X@@，@@M@@0\le q\le1@@）及其上确界 @@M@@M@@ 展开。因 @@M@@f@@ 保范保距，@@M@@D_0=D_1=0@@，故 @@M@@M\le1@@；只要证明 @@M@@M=0@@，径向映射便保持全部距离、满且固定原点，再由 Mazur–Ulam 定理得仿射性、进而实线性。以下反设 @@M@@M>0@@。
先取到极大：以自由超滤子（free ultrafilter）构造 Banach 空间超幂（ultrapower），将 @@M@@f@@ 逐项作用，得到一对可能放大的空间上仍以 @@M@@M@@ 为亏损上界的球面满等距，且亏损在某处精确取等：存在 @@M@@x_0,y\in S_X@@ 与 @@M@@0<t<1@@ 使 @@M@@\norm{f(x_0)-tf(y)}-\norm{x_0-ty}=M@@。于是只需排除这个”极大已取到”的构型。
再对齐弦（chord）：固定 @@M@@y,t@@，记 @@M@@b=f(y)@@。从内点 @@M@@ty@@ 沿方向 @@M@@v@@ 交 @@M@@S_X@@ 于 @@M@@x=ty+pv@@，其像记 @@M@@f(x)=tb+sw@@；再从 @@M@@tb@@ 沿 @@M@@-w@@ 交 @@M@@S_Y@@ 于 @@M@@f(z)=tb-uw@@，把 @@M@@z@@ 拉回并反向得返回映射 @@M@@g(v)@@。@@M@@g@@ 的不动点恰好给出两条沿各自方向对齐的弦，满足 @@M@@s-p=r-u=M@@。为找不动点，令极值方向集 @@M@@E=\{v\in S_X:s(v)-p(v)=M\}@@，其核心传播规则是：凡与 @@M@@g(v)@@ 共有支撑泛函（common support）的单位方向都落入 @@M@@E@@——支撑泛函由”范数等于权重之和”时的 Hahn–Banach 论证给出。据此归纳构造闭凸集 @@M@@C=\clco\{v_0,v_1,\dots\}\subset E\subset S_X@@ 且 @@M@@g(C)\subset C@@，并证明 @@M@@g@@ 严格压缩 Kuratowski 非紧性测度（measure of noncompactness）：@@M@@\chi(g(H))\le\gamma\chi(H)@@，@@M@@\gamma=(1-M/(1+t))^2<1@@；Darbo 不动点定理（Darbo’s fixed-point theorem，附录中自 Sperner 引理完整证明）便给出不动方向。
最后弦矛盾：记 @@M@@d=\norm{x-z}=p+r=s+u\le2@@，@@M@@A=p/d@@，@@M@@B=u/d@@，@@M@@\epsilon=1-t@@，则 @@M@@A+B=1-M/d<1@@。割线（secant）估计把支撑泛函在 @@M@@v@@ 处的值夹逼于 @@M@@\epsilon/p@@ 与 @@M@@1-B@@（或 @@M@@B@@）之间。若 @@M@@A>\epsilon@@ 或 @@M@@B>\epsilon@@，借助逆映射构型的对称性 @@M@@(p',s',r',u')=(u,r,s,p)@@ 可推出：@@M@@v@@ 处的支撑在 @@M@@y@@ 上恒取负值、@@M@@w@@ 处的支撑在 @@M@@b@@ 上恒取正值，于是小径向扰动使 @@M@@\norm{sw+\eta b}>s@@ 而 @@M@@\norm{pv+\eta y}<p@@，与亏损界 @@M@@\le M=s-p@@ 矛盾。故只能 @@M@@A,B\le\epsilon@@，对原构型与逆构型分别用割线估计得 @@M@@\epsilon\le dA(1-B)@@、@@M@@\epsilon\le dB(1-A)@@；两乘积中较小者 @@M@@<1/4@@，迫使 @@M@@\epsilon<1/2@@。最后比较凸函数 @@M@@F(\lambda)=\norm{y+\lambda v}@@ 与 @@M@@G(\lambda)=\norm{b+\lambda w}@@ 的割线斜率：得 @@M@@F(r/\epsilon)>1/t@@ 而 @@M@@G(u/\epsilon)\le1/t@@，但球面保距要求 @@M@@\epsilon F(r/\epsilon)=\norm{y-z}=\norm{b-f(z)}=\epsilon G(u/\epsilon)@@，矛盾。故 @@M@@M=0@@，中点反射论证（Mazur–Ulam 的简证形式）最终完成实线性与唯一性。
据任务元信息，本篇主结果已有 Lean 形式化证明，族内附有对应文档（lean/docs/322.md）；从支撑泛函、超幂构造到 Darbo 不动点定理的完整证明链均写入正文与附录，可经机器核验。本篇是该结果族的核心：它不限定空间类别，此前 @@M@@\ell^p@@、@@M@@L^p@@、@@M@@C^*@@-代数、二维空间等肯定结论皆为其特例。仍请留意 OpenAI 官方声明：未经形式化的结果可能存在问题，核验请以形式化版本与社区审查为准。
问 1：证明里最关键、也最难复核的一步是什么？
（答：命题 prop:alignment：由共同支撑泛函的传播规则造出闭凸不变集 @@M@@C\subset S_X@@，再证返回映射 @@M@@g@@ 严格压缩 Kuratowski 非紧性测度 @@M@@\chi(g(H))\le\gamma\chi(H)@@，@@M@@\gamma=(1-M/(1+t))^2<1@@，Darbo 不动点给出对齐弦。压缩估计里”按 @@M@@p,u@@ 的值域细分覆盖”的 @@M@@4\eta/a@@ 误差控制是全文计算最密处。）
问 2：超幂这一步为什么不能省？
（答：亏损上确界 @@M@@M@@ 在原空间未必取到；引理 lem:attainment 用自由超滤子把 @@M@@f@@ 逐项搬到超幂上，得到”极大已取到”的构型再排除。代价是空间可能被放大，且构造用了选择公理（论文明言）。省去它就要在原空间处理一列逼近极大的三元组，目前的对齐论证没有这样的版本。）
问 3：为什么不断言复线性？
（答：定理把复空间视为实空间，径向扩张天然只是实线性的；Mazur–Ulam 也只给实仿射。论文未讨论是否存在球面复等距不复线性的具体反例，这一复情形留白，做算子代数延拓问题的人需要另行核对。）
问 4：与此前逐类结果相比，真正的新意是什么？
（答：@@M@@\ell^p@@、@@M@@L^p@@、von Neumann 代数、二维空间等都是”指定源与目标”或指定空间类的 Mazur–Ulam 性质；本文是首个不设任何类别限制的一般定理，此前全部肯定结论成为特例。方法上与 Tanaka 的面（facial）几何有亲缘——共同支撑传播是”面”的替身，但不依赖空间的光滑性。）
问 5：AI 生成证明最可能出错的地方，本文风险如何？
（答：高危点通常是引理 lem:secant 的双向夹逼 @@M@@\epsilon/p\le\varphi(v)\le K@@ 与逆构型参数置换 @@M@@(p',s',r',u')=(u,r,s,p)@@ 的对称性使用——两处都是”换个支撑泛函就差一个符号”的典型陷阱。但据任务元信息本篇主结果已有 Lean 形式化（lean/docs/322.md），从支撑泛函、超幂到 Darbo 定理全链可机器核验，这类风险已被吸收。）
问 6：收尾的 @@M@@\epsilon<1/2@@ 与割线斜率矛盾为何必要？单靠径向扰动不够吗？
（答：引理 lem:large 用径向扰动排除 @@M@@A>\epsilon@@ 或 @@M@@B>\epsilon@@ 的大参数区；剩下 @@M@@A,B\le\epsilon@@ 的小参数区扰动失效，须对原构型与逆构型各用一次割线估计得 @@M@@\epsilon\le dA(1-B)@@、@@M@@\epsilon\le dB(1-A)@@，两乘积较小者 @@M@@<1/4@@ 加 @@M@@d\le2@@ 逼出 @@M@@\epsilon<1/2@@，最后比较凸函数 @@M@@F,G@@ 的割线斜率与球面保距相撞。两个参数区各需要一件武器。）
问 7：谁会用到它？
（答：Banach 空间几何与等距延拓问题的人——所有逐类 Mazur–Ulam 性质研究一夜之间变成特例；算子代数与量子信息里”保距结构决定代数结构”型的定理也因此有了通用底座；凸分析与不动点理论提供了纯几何的交叉应用样本。）
总评
三十余年的逐类验证就此升格为无限制的一般定理，且已有 Lean 形式化背书，是本批结果里可信度最高的一篇；残余风险仅在形式化尚未覆盖的复线性留白与叙述性转述，数学内容本身基本封账。