结果族 248：Thompson’s group F is nonamenable · 学科：Group theory · 验证状态：主结果已 Lean 形式化
想象一家搬家公司，每种”搬法”都会重新排列棋盘上的棋子。温和的公司允许你圈出一大块地盘：无论用公司里哪几种标准搬法，地盘边界都几乎不动；暴躁的公司则任你圈哪块地盘，总有搬法把它搅得面目全非。这篇论文证明：几何群论的明星对象 Thompson 群 @@M@@F@@ 属于暴躁的一类——它不是顺从群，Geoghegan 1979 年提出、悬置四十多年的难题就此定案。
关键词卡片
@@M@@[0,1]@@ 上所有”断点取二进分数、斜率取 2 的幂”的分段线性变形组成的群@@M@@|hA\triangle A|/|A|@@ 可以任意小@@M@@A\triangle B@@ 是只属于 @@M@@A@@、@@M@@B@@ 之一的元素全体，用来量”搬动前后差了多少”看个具体例子
先看温和的例子：整数群 @@M@@\mathbb{Z}@@ 中取地盘 @@M@@A=\{1,2,\dots,100\}@@，搬法 @@M@@h@@ 是”右移一格”，@@M@@hA@@ 与 @@M@@A@@ 只在两端各差一个数，边界比 @@M@@=2/100=0.02@@；地盘越大比值越小，故 @@M@@\mathbb{Z}@@ 顺从。论文证明 @@M@@F@@ 中存在一组固定搬法 @@M@@S@@ 与正常数 @@M@@c@@，使任何有限地盘 @@M@@A@@ 都被某个 @@M@@h\in S@@ 搅动到边界比不小于 @@M@@c@@——”右移一步几乎不动”的好事在 @@M@@F@@ 里永远不会发生。
为什么值得关心
@@M@@F@@ 早在 1985 年就被证明不含非交换自由子群，也不属于初等顺从类，两条判断非顺从的经典路径全部失效，使它成为该领域最著名的悬案之一；本文以”无穷维球面上一个没有近似不动点的映射”加一次有限平均论证将其攻克。
已 Lean 形式化
结果族 248：Thompson’s group F is nonamenable · 配套入门导读见同目录文章
第一级台阶
导读里把群想成一家搬家公司：每个”搬法”都是把区间重新切分、再把各段拉伸拼接的变形方式，两个搬法先后施行仍是同类搬法，全体搬法因此构成一个群。判断公司暴躁与否，看的不是某一个搬法，而是：任选一块由群元素组成的有限”地盘”，是否总有某种搬法让它大面积变形。
第二级台阶
用精确语言说，Thompson 群 @@M@@F@@ 由区间 @@M@@[0,1]@@ 上所有保定向分段线性同胚构成，断点取二进分数、斜率取 2 的整数幂。一个群称为顺从群，若对任意有限子集 @@M@@T@@ 和 @@M@@\varepsilon>0@@，都存在有限非空集 @@M@@A@@ 使 @@M@@|tA\triangle A|/|A|<\varepsilon@@ 对一切 @@M@@t\in T@@ 成立（Følner 准则），其中 @@M@@tA@@ 是 @@M@@t@@ 平移 @@M@@A@@ 所得的像，@@M@@\triangle@@ 表示对称差。
第三级台阶
定理正是在这条准则的反面陈述：论文构造出与被测集合无关的有限集 @@M@@S\subset F@@ 及正常数 @@M@@c@@，使得一切有限非空 @@M@@A\subset F@@ 都满足 @@M@@\max_{h\in S}|hA\triangle A|/|A|\ge c@@，Følner 准则随之失效，@@M@@F@@ 非顺从。支撑构造的是 @@M@@F@@ 的两个特性：它能把任意一对分离区间仿射地”搬运”到另一对，而无穷维球面上存在没有近似不动点的 Lipschitz 自映射。递归染色把这两件事缝合起来，方差展开中公共相关值的系数恰好相消，只剩边界比项。
论文证明了 Thompson 群 @@M@@F@@——区间 @@M@@[0,1]@@ 上二进分段线性同胚构成的群——不是顺从群（nonamenable），确认了 Geoghegan 1979 年猜想，为这个悬置四十余年的几何群论难题画上句号。
Thompson 群 @@M@@F@@ 由 @@M@@[0,1]@@ 上所有保定向分段线性同胚构成，要求分段有限、断点均为二进有理数（dyadic rational）、斜率均为 2 的整数幂；它由 Thompson 于 1965 年引入（早期构造见 McKenzie–Thompson 1973），是几何群论的核心对象。顺从性（amenability）源自 von Neumann 与 Day 的经典理论：群顺从当其上有正的、归一的左不变平均（invariant mean）；由 Følner 准则可知，顺从群对任何有限平移集都能找到相对边界 @@M@@|hA\triangle A|/|A|@@ 同时任意小的有限集。Cannon–Floyd–Parry 讲义记载了 Geoghegan 1979 年的猜想：@@M@@F@@ 非顺从。问题之难在于两条经典判据全部失效：Brin–Squier（1985）证明 @@M@@F@@ 不含非交换自由子群，自由群障碍用不上；@@M@@F@@ 又不属于初等顺从类（elementary amenable）。此前不乏两个方向的证明断言——Akhmedov 2021 宣称非顺从，Shavgulidze 2009 宣称顺从（被 Moore 指出错误，Moore 亦撤回过自己一篇顺从证明）——均未成为定论。Moore 还证明了 Følner 集大小的塔式下界与 Ramsey 刻画，Haagerup–Olesen 证明 Thompson 群 @@M@@T@@ 的约化 C*-代数单性蕴含 @@M@@F@@ 非顺从，但都不能直接定夺。
主定理：Thompson 群 @@M@@F@@ 不是顺从群。论文实际证明的是定量版本（finite-proof.tex，命题 avg:boundary）：存在与待测集无关的有限集 @@M@@S\subset F@@ 及正常数
@@M@@Dc=\frac{\delta^2/L^2-4/D}{4(1-1/D)}>0,@@
使得对一切非空有限集 @@M@@A\subset F@@ 均有 @@M@@\max_{h\in S}|hA\triangle A|/|A|\ge c@@，与 Følner 准则直接矛盾。推论有两条（consequences.tex，均援引配套定理）：其一，对每个 @@M@@\varepsilon>0@@，存在表示 @@M@@\pi:F\to\mathrm{GL}(H)@@ 满足 @@M@@\sup_g\|\pi(g)\|\le1+\varepsilon@@，却不能被任何有界可逆算子整体酉化（nonunitarizable，不可酉化）；其二，对任意有限对称生成集给出的 Cayley 图，Bernoulli 边渗流（bond percolation）满足 @@M@@\|T_{p_c}\|_{2\to2}<\infty@@、@@M@@p_c<p_{2\to2}\le p_u@@，且对每个 @@M@@p\in(p_c,p_u)@@ 几乎必然出现无穷多个无穷开簇（open cluster），并存在确定性窗口 @@M@@[p_1,p_2]@@ 使之同时发生。
整个证明是”反证法＋无穷维现象＋一次有限平均”的组合。先固定三样与待测集无关的原料。其一，Benyamini–Sternfeld 定理（1983）供给的映射：无穷维 Hilbert 空间闭单位球 @@M@@B@@ 上存在 Lipschitz 自映射 @@M@@f@@ 与 @@M@@\delta>0@@ 使 @@M@@\|f(x)-x\|\ge\delta@@ 处处成立（无近似不动点）；附录在 @@M@@L^2([0,1];\mathbb R^2)@@ 上以 @@M@@\delta=1/2@@ 显式构造——沿一条带”有界尾部”的螺线曲线取固定半径的管状邻域，再令 @@M@@f(x)=-G(x)/\|G(x)\|@@。其二，满足 @@M@@D>4L^2/\delta^2@@ 的大整数 @@M@@D@@。其三，@@M@@D@@ 个两两分离的内部二进区间 @@M@@I_1<\cdots<I_D@@（父区间），并在每个父区间内放入这组区间的仿射拷贝 @@M@@I_i\cdot I_j@@（子区间）。随后对每个基本二进划分按胞腔数递归定义颜色 @@M@@p(T)\in B@@：当 @@M@@T@@ 尊重全部父区间时，@@M@@p(T)=f(\text{诸限制颜色的均值})@@，否则取 @@M@@0@@；取限制会严格减少胞腔数，故归纳良定。对群元 @@M@@g@@ 取足够细的水平 @@M@@n@@，使像划分 @@M@@gT^{(n)}@@ 基本化并尊重所有相关区间，据此定义颜色函数 @@M@@X_I(g)@@ 与标量相关（scalar correlation）@@M@@\varphi_{I,J}(g)=\langle X_I,X_J\rangle@@。
接着是组合核心”搬运”：@@M@@F@@ 能把任意分离区间对标仿射地送到任意另一对（在三个余隙中反复二分配平胞腔数即可），据此预先固定有限搬运元集 @@M@@S@@。精确的协方差恒等式 @@M@@((hg)T^{(n)})_{I'}=(gT^{(n)})_I@@ 给出 @@M@@\varphi_{I,J}(g)=\varphi_{I_1,I_2}(h_{I,J}g)@@；再配合初等的有限平均比较 @@M@@|\mathbb E_A\varphi(hg)-\mathbb E_A\varphi(g)|\le|hA\triangle A|/|A|=\eta@@，可得：凡严格分离的区间对，其平均相关都落在同一公共值 @@M@@\alpha@@ 的 @@M@@\eta@@ 邻域中。
最后是方差估计。令 @@M@@m@@ 为父颜色均值、@@M@@z_i@@ 为第 @@M@@i@@ 个父区间诸子颜色的均值，递归定义给出精确恒等式 @@M@@X_{I_i}=f(z_i)@@，而 @@M@@m@@ 又是诸 @@M@@f(z_i)@@ 的均值。位移下界、平方范数的凸性与 Lipschitz 条件联合给出
@@M@@D\delta^2\le\|m-f(m)\|^2\le\frac{L^2}{D}\sum_i\|z_i-m\|^2 .@@
展开 @@M@@\mathbb E_A\|z_i-m\|^2@@ 时，交叉项中严格分离对的相关被 @@M@@\alpha\pm\eta@@ 控制，公共值 @@M@@\alpha@@ 的系数恰好正负相消；对角项与嵌套对只占比例 @@M@@1/D@@，由单位球界控制。合并得 @@M@@\mathbb E_A\|z_i-m\|^2\le4/D+4(1-1/D)\eta@@，代回上式整理即得一致正下界 @@M@@c@@，与 Følner 准则矛盾，故 @@M@@F@@ 非顺从。
论文标注主结果已获 Lean 形式化证明（结果族 248 附有形式化文档），这对该量级的结论是重要保障。两条推论分别援引同项目关于不可酉化表示与渗流的姊妹定理：它们依赖本文结论而非相反，论文也明确说明二者未参与非顺从性的证明。按 OpenAI 官方声明，未经形式化的结果可能存在问题；本文主结果已形式化，推论所涉配套定理仍请以社区核验为准。
问 1：整个证明最关键、也最脆弱的一步在哪里？
答：命题 avg:boundary 里的方差估计（式 (avg:variance)）。展开 @@M@@\mathbb E_A\|z_i-m\|^2@@ 时，非对角交叉项的平均相关被公共值 @@M@@\alpha\pm\eta@@ 控制，而 @@M@@\alpha@@ 的系数必须正负精确相消；任何一对区间被错分类——比如把嵌套对当成严格分离对——都会留下未消项，常数 @@M@@c@@ 就立不住。论文专门用图 mixed-pairs 展示混合项的两类配对划分。
问 2：为什么必须用无穷维 Hilbert 球？这条假设能去掉吗？
答：不能。染色递归依赖引理 lem:displacement 供给的映射 @@M@@f@@：Lipschitz 常数 @@M@@L@@ 有限、又处处满足 @@M@@\|f(x)-x\|\ge\delta@@。有限维闭单位球由 Schauder 不动点定理必有不动点，这样的 @@M@@f@@ 根本不存在；只有无穷维（Benyamini–Sternfeld 定理）才供给。下界常数 @@M@@c=(\delta^2/L^2-4/D)/4(1-1/D)@@ 为正还要求 @@M@@D>4L^2/\delta^2@@，故证明开头必须选足够大的 @@M@@D@@。
问 3：与以往失败的尝试相比，真正的新意是什么？
答：经典两条路全堵死：Brin–Squier 证明 @@M@@F@@ 无非交换自由子群，@@M@@F@@ 又非初等顺从，故既不能用自由群障碍也不能用顺从类封闭性。本文首次把无穷维无不动点映射递归植入二进划分的染色，再只用一次初等的有限平均（式 (eq:finite-translation)）把任意候选 Følner 集的边界比压到统一正下界，完全绕开不变平均与约化 C*-代数（Haagerup–Olesen 路线）。
问 4：AI 生成证明最可能在哪里出错？
答：最可疑的是良定性与一致性细节：颜色 @@M@@p(T)@@ 按胞腔数递归是否良定、@@M@@(n,g)@@ 的容许性在 @@M@@h_{I,J}g@@ 处是否成立——搬运元不必保持 @@M@@\mathcal I@@ 中其他区间，论文在 finite-proof.tex 中明确承认并单独处理——以及精确协方差恒等式 @@M@@((hg)T^{(n)})_{I'}=(gT^{(n)})_I@@。本主定理已 Lean 形式化，此类错误风险大幅降低。
问 5：两条推论（consequences.tex）分量如何？
答：推论 cor:nonunitarizable 给出 @@M@@F@@ 上 @@M@@\sup_g\|\pi(g)\|\le1+\varepsilon@@ 却不可酉化的表示；推论 cor:percolation 给出任意 Cayley 图上 @@M@@p_c<p_{2\to2}\le p_u@@ 且 @@M@@(p_c,p_u)@@ 内几乎必然无穷多无穷开簇。但二者分别援引姊妹论文（OpenAIUnitarizability2026 定理 1.1、OpenAIPercolation2026 推论 1.2），论文明确说明这些配套结果不参与非顺从性证明，其自身也未形式化，社区核验前应视为暂定。
问 6：这个结果谁会用到？
答：Haagerup–Olesen 的”Thompson 群 @@M@@T@@ 约化 C*-代数单性蕴含 @@M@@F@@ 非顺从”从此方向反转、失去必要性；算子代数中 Dixmier 酉化问题与粗几何、渗流理论中一切以”群非顺从”为输入的定理现在多了一个具体而重要的群作为实例来源。
总评
一项已形式化、了结 Geoghegan 1979 年以来四十余年悬案的硬定理，证明短而组合味浓；最大风险不在主结果，而在其推论链条挂在两条未形式化的姊妹定理上。