结果族 257：A hyperbolic group without a geometric CAT(0) action · 学科：Group theory · 验证状态：主结果已 Lean 形式化
有些群的内部世界像双曲马鞍面：处处下凹、三角形内角和小于 180°，迷路了也容易抄近路找回。数学家长期猜想，这样的”负曲率群”总能搬进某个真正的非正曲率空间安家，Gromov 本人找了多年。这篇论文造出反例：一个规规矩矩的负曲率群，任何维数的非正曲率新房都容不下它。
关键词卡片
看个具体例子
双曲性的直观招牌是”回路便宜”：一条长 100 的迷路，在双曲群里用与周长同量级的窄带就能填平（左图）；在平面 @@M@@\mathbb{Z}^2@@ 里，边长 100 的方框内部必须整块填满，代价约 100²（右图）。论文构造的复形 K 恰恰有线性填充（故其基本群是双曲群），却无论如何也造不出 CAT(0) 几何——”容易填平”并不保证”住得进平地”。
为什么值得关心
它否定了”群论负曲率总能实现为几何负曲率”的长期期待，给 Gromov 时代的实现问题画上句号：双曲与 CAT(0) 从此是真正不同的两类。
已 Lean 形式化
第一级台阶
导读把双曲群说成”内部像马鞍面、回路便宜”的结构。换成半数学语言：研究对象是由有限份生成规则给出的群，它的大尺度特征是——任何一条闭的迷路，都能用与长度成比例的少量”面片”填平；这种”负曲率式的便宜”是纯组合可验证的。要问的问题：这种内部负曲率，是否总能通过某个外部非正曲率空间上的规整对称行动来实现。
第二级台阶
用本科术语精确化。字双曲群：有限呈现群满足线性等周不等式——万有覆盖中长 ℓ 的组合边缘回路可用至多 C·ℓ 个三角面填成圆盘。CAT(0) 空间：每个三角形都不胖于欧氏参照三角形的度量空间；几何作用：群经等距变换真（有界集稳定子有限）且余紧（商紧）地作用于其上。逐球复形：万有覆盖可缩的胞腔空间；有限逐球复形即群的有限分类空间。
第三级台阶
定理的语境是实现问题：Gromov 引入双曲群后自陈寻找多年，CAT(−1) 版列作 1999 年问题表 H11，直至 2025–2026 年综述仍公开。主定理给出二维有限逐球单纯复形 K，同时满足：其万有覆盖有线性圆盘填充（故 π₁K 双曲），且 π₁K 在任何真完备 CAT(0) 空间上都没有几何作用。”真完备”挡掉无穷分支的病态舞台；更强的模型级结论还允许在同伦等价类内更换整个复形——任何相容的局部 CAT(0) 测地长度度量都被排除，从而局部 CAT(−1) 模型也不存在。注意这是存在性论证：K 无有效规模，填充常数可依赖所选呈现。
构造出一个带有限分类空间（finite classifying space）的字双曲群，它不容许在任何维数的真完备 @@M@@\mathrm{CAT}(0)@@ 空间上有真且余紧的等距作用，从而对”每个双曲群都是 @@M@@\mathrm{CAT}(0)@@ 群”这一长期公开的实现问题给出否定回答。
对有限呈现群，线性等周不等式（linear isoperimetric inequality）刻画字双曲性（word hyperbolicity），这是 Gromov 1987 年提出的”负曲率的群论化身”。但群论负曲率未必能实现为几何负曲率：实现问题问，是否每个双曲群都能在某个真完备 @@M@@\mathrm{CAT}(0)@@ 甚至 @@M@@\mathrm{CAT}(-1)@@ 空间上有几何作用（geometric action，即真、余紧的等距作用）。Gromov 本人在访谈中回忆曾为此寻找多年；@@M@@\mathrm{CAT}(-1)@@ 版本作为问题 H11 列入 Baumslag–Myasnikov–Shpilrain 1999 年问题表，两个版本直到 2025–2026 年的综述与预印本中仍列为公开问题。此前最好的反方向结果局限于二维：Brady–Crisp 2007 年造出不容许在二维真 @@M@@\mathrm{CAT}(0)@@ 空间上作用的无限双曲群，依赖二维平移长度约束，高维毫无排除。本文首次在一切维数上一举排除。
主定理：存在有限连通二维逐球（aspherical）单纯复形 @@M@@K@@ 与常数 @@M@@C<\infty@@，使得一，@@M@@K@@ 的万有覆盖中每条长 @@M@@\ell@@ 的组合边缘回路都由至多 @@M@@C\ell@@ 个三角面填充（线性组合圆盘填充不等式）；二，@@M@@\pi_1K@@ 不容许任何在真完备 @@M@@\mathrm{CAT}(0)@@ 空间上的几何作用。由线性 Dehn 函数与字双曲性等价，@@M@@\pi_1K@@ 是双曲群。更强的有限模型结论：任何与 @@M@@K@@ 同伦等价的有限单纯复形都不容许与其拓扑相容的局部 @@M@@\mathrm{CAT}(0)@@ 测地长度度量，因而也不容许局部 @@M@@\mathrm{CAT}(-1)@@ 度量。证明是存在性论证，不给出 @@M@@K@@ 的有效规模，填充常数可依赖所选的有限呈现。
组合模板取自 @@M@@\mathbb F_2@@ 上射影平面（Fano 平面）的关联图：把四个点的顶点加倍，删去其中一条关联（@@M@@Y_D@@–@@M@@CD@@）而保留另一端的”松边”，其余关联在每个点处连成”扇”。再对生成元字母随机采样若干独立伯努利表格——七个扇表、一个顶层表、给每条非回溯二边核心路径配一张四字段方形装饰表（共九十张）、外加一张六字母表——把被选中闭路的标签全部取为关系。概率指数精心设计，使期望计数恰低于 @@M@@N^2@@、@@M@@N^3@@，赤字 @@M@@\alpha@@、@@M@@\beta-7\alpha@@、@@M@@\delta@@ 为正。论证分三大支柱。第一是图表计数（diagram counting）：被多个整体拷贝共享的扇只贡献一次概率代价，却可能被同一关系反复使用；通过对不同表格条目赋重数权重化解这一矛盾，局部关联估计迫使图的面积必须由边界支付，再用平面分隔子从有界片段推广到全部圆盘与球面图，同时得到线性填充与逐球性。第二是”对后续作用一致”的采样：把若干匹配（match）沿放大的条件元组粘合并证明延伸数目集中，使每个分支近似均匀、新标签近似独立均匀——结论以全变差形式陈述，因而适用于表格揭晓之后才任意选取的作用所定义的有界检验。第三是刚性构型导出矛盾：假设无穷多个群都有几何作用，用 Gromov–Izeki–Nayatani 调和能量框架取能量极小基点并归一化平均平方位移，六字母表借助 @@M@@a^{-1}=s_2\cdots s_6@@ 型关系给出与作用无关的位移上界；把所有匹配的轨道构型取乘积再取超极限，装饰方形迫使二步距离平方恰为 @@M@@2@@，所有核心六边形共享公共中心 @@M@@c@@、半径 @@M@@\sqrt3/2@@ 且中心三角形平坦。最后的几何反驳在切锥 @@M@@T_cZ@@ 中进行：加倍点给出单位向量 @@M@@M_i@@（扇恒等式），线性关联经标量积凹性迫使 @@M@@\langle M_A,M_B\rangle\ge 0@@；而松边处的例外恒等式 @@M@@h_0=M_C\oplus x_D@@ 连同 @@M@@\mathrm{CAT}(1)@@ 方向空间中的半圆推理迫使 @@M@@M_C,M_D@@ 对径，平行集分解 @@M@@P(\ell)=\mathbb R\times Q@@ 在横截因子 @@M@@Q@@ 中暴露一个单位平坦正方形，其对边中点又迫使 @@M@@M_A,M_B@@ 对径，@@M@@\langle M_A,M_B\rangle=-1@@，矛盾。最后经对角选取取定一个无作用的实例，并经单纯替换转移到单纯模型 @@M@@K@@。
主结果已由 Lean 形式化验证（结果族文档 lean/docs/257.md），与随机群、调和能量方法等外部引理的引用链条清晰，可信度高。本篇是该结果族的核心构造篇，族内 Lean 记录与其互为支撑。按 OpenAI 官方声明，未经形式化的结果可能存在问题，故读者应以形式化版本及社区核验为准；另请注意定理不给出 @@M@@K@@ 的具体规模。
问 1：证明里最关键也最脆弱的一步是什么？
（答：三支柱缺一不可，最脆弱的是后两个的接缝。第二支柱要求采样对”表格揭晓之后才任意选取的作用”一致——靠全变差耦合把若干匹配粘合、证延伸数集中（第 4 节）；第三支柱在切锥里推理：扇恒等式给 ⟨M_A,M_B⟩≥0，松边的例外恒等式与平行集分解暴露平坦正方形、迫使 M_A,M_B 对径得 −1（第 6 节）。任何一处度量恒等式在超极限中只近似而非精确成立，矛盾即消失。）
问 2：为什么反例必须是随机化的存在性构造，而不是显式群？
（答：关系要同时”稀疏到保住双曲与逐球”（图表计数的正赤字 α、β−7α、δ）又”稠密到产生障碍”，两者在固定小模板上难以手工配平；论文经概率指数设计让期望计数恰低于 N²、N³。代价是定理不给 K 的有效规模（第 1 节明言），填充常数依赖所选呈现。）
问 3：与 Brady–Crisp 相比真正的新意是什么？
（答：Brady–Crisp 2007 只排除二维目标（其 Theorem 1 是 CAT(0) 维二、CAT(−1) 维三的群），靠二维平移长度约束；本文排除一切维数的几何 CAT(0) 作用，且模型级结论允许整个复形在同伦型内更换。与 Ollivier–Wise 密度 <1/6 随机群可 cubulate 相对照，本文的随机关系还须额外生成障碍——同一概率模型的两种命运，本身就是方法的看点。）
问 4：哪些假设去掉后结论不再有意义？
（答：空间”真完备”与作用”真、余紧”是几何作用的定义性条款；论文未讨论非余紧或非真的等距作用是否存在。模型级结论限定”诱导原拓扑的测地长度度量”，这是把度量任意性收进可比较范围的关键，去掉则无从陈述。）
问 5：作为 AI 生成但已 Lean 形式化的证明，最可能出错的模式是什么？
（答：形式化覆盖主定理后，风险移向两处：外部引理链（Gromov–Izeki–Nayatani 调和能量、Sturm 归纳平均）的引用条件是否与本文用法逐条吻合；以及形式化语句与自然语言定理（尤其”任何同伦等价有限模型”一句）的忠实对应。概率赤字与超极限的细节若已在形式化内，则可信度高。）
问 6：谁会用到它？
（答：它终结了实现问题的两个版本（CAT(0) 与 CAT(−1)），双曲群与 cubulation 纲领必须绕行；一个直接推论——论文本身未展开——是该群不可能 virtually compact special，否则特殊商将经立方复形给出几何 CAT(0) 作用，这为 Wise 纲领提供了新的边界样本。）
总评
这是对 Gromov 时代实现问题的否定终章，且主结果已形式化，分量很重；最大风险是非有效构造难以独立复算，剩余校验压力集中在外部能量引理的使用条件上。