结果族 250：Boone–Higman embeddings with higher finiteness · 学科：Group theory · 验证状态：暂无形式化证明，请以社区核验为准
有的群自带”标准判卷机”：给它一串由生成元拼成的词，算法能判定它是否等于单位元——这是计算机性质。有的群住得极其极简又通透：有限条规则就能写清全部说明书，且内部没有任何隔间（单群）——这是纯代数性质。这篇论文证明两者惊人地等价：字问题可判定，当且仅当能搬进某个有限呈现的单群。这就是 1974 年提出、悬置五十余年的 Boone–Higman 猜想。
关键词卡片
看个具体例子
拿最简单的无限群 @@M@@\mathbb{Z}=\langle a\rangle@@ 试：词只有 @@M@@a^n@@ 形式，判它是否为单位元只需检查 @@M@@n@@ 是否为 0，一步即得，字问题可判定。于是定理断言 @@M@@\mathbb{Z}@@ 必能住进某个有限呈现单群。数字版定理（对一切有限生成群成立）：
@@M@@D\exists\,\text{有限呈现单群 }H,\ G\hookrightarrow H \iff \text{字问题可判定}@@
反向用 Kuznetsov 的老结论：非平凡有限呈现单群的字问题可判定且传给子群；全新的是正向构造——先造一个忠实且二重传递的”置换包络”，再套 Belk–Zaremsky 判据封进单群。
为什么值得关心
它把”算法可解”这一计算概念完整翻译成纯群论语言，让可判定性第一次拥有不提算法的纯代数刻画，是算法群论的里程碑。
暂无形式化证明（AI 结果待核验）
结果族 250：Boone–Higman embeddings with higher finiteness · 配套入门导读见同目录文章
第一级台阶
导读说有的群自带”标准判卷机”，有的群住得”极简又通透”。翻译一下：对象是一个带有限份说明书（生成元）的群，考题是把生成元连乘得到的词；”判卷机”是一台对任何词都能停机并给出”是/否代表单位元”的算法。”极简又通透”则是说这个大群本身由有限条规则完整描述、且内部没有非平凡的正规”隔间”。定理声称：这两种品质可以同时安放在同一对群之间。
第二级台阶
精确地说：群 @@M@@G@@ 的字问题可判定，指存在算法判定每个词是否代表单位元；@@M@@G@@ 有限呈现，指由有限个生成元与有限条关系给出；单群指无非平凡正规子群的非平凡群；嵌入指单同态 @@M@@G\hookrightarrow H@@。中间概念是忠实二重传递作用：群在无穷集上作用，只有单位元作用平凡，且在有序点对上传递。
第三级台阶
定理（thm:main）对每个有限生成群 @@M@@G@@ 断言：字问题可判定当且仅当 @@M@@G@@ 嵌入某个有限呈现单群。反向由 Kuznetsov 论证直接得到；难点在正向，经中间定理（thm:envelope）：把 @@M@@G@@ 装进一个有限呈现、在可数集上有忠实二重传递作用且点稳定子有限生成的群，再用 Zaremsky 的判据封进扭曲 Brin–Thompson 单群。二重传递恰好把无序点对缩成一个轨道，凑齐判据最后一条；有限生成假设保证考题有限份说明书可考，去掉它判卷机本身无从谈起。
证明了 1974 年提出的 Boone–Higman 猜想：有限生成群的字问题（word problem）可判定，当且仅当它能嵌入一个有限呈现的单群。这把”可判定”这一算法性质完全翻译成纯群论的嵌入性质，是算法群论中悬置五十余年的核心刻画。
一个群的字问题问：给定生成元上的一个词，是否有算法判定它表示单位元。1961 年 Higman 嵌入定理把有限呈现群的有限生成子群刻画为恰是递归可枚举呈现的群；字问题可判定是更强的条件，它同时给出相等与不等的算法。1974 年 Boone 与 Higman 证明：字问题可判定当且仅当 @@M@@G\leq H\leq K@@，其中 @@M@@H@@ 单、@@M@@K@@ 有限呈现。两条件分属两个群，而有限呈现性一般不遗传给子群，他们随即问（原文第 43 页）：中间的单群 @@M@@H@@ 本身能否取成有限呈现？这就是 Boone–Higman 猜想。此前 Thompson 只能得到有限生成的单超群；正面情形局限于双曲与收缩自相似群、Baumslag–Solitar 群、free-by-cyclic 群、自由群自同构群与映射类群等特殊族。
主定理：对每个有限生成群 @@M@@G@@，下列等价：(i) @@M@@G@@ 的字问题可判定；(ii) @@M@@G@@ 嵌入某个有限呈现的单群（finitely presented simple group）。构造方向只需 @@M@@G@@ 的有限生成集与一个字问题判定器，@@M@@G@@ 本身不必有限呈现；反向用 Kuznetsov 的并行搜索论证——非平凡有限呈现单群的字问题可判定，且遗传给有限生成子群。关键中间定理是”置换包络”：每个这样的 @@M@@G@@ 嵌入一个有限呈现群 @@M@@\Gamma@@，它在一个可数无限集上有忠实（faithful）、二重传递（two-transitive）的作用，且每点稳定子有限生成。二重传递恰使 @@M@@X@@ 的无序点对只有一个轨道，凑齐 Zaremsky 2024 年 type (A) 作用的全部条件，再经 Belk–Zaremsky 的扭曲 Brin–Thompson 构造即得有限呈现单群。
先做群论归约：取 HNN 扩张（HNN extension）@@M@@\widehat G=\langle G\times G,s\mid s(g,g)s^{-1}=(1,g)\rangle@@，由 Britton 引理知 @@M@@G\times G@@ 嵌入且 @@M@@\widehat G@@ 仍字问题可判定，并且 @@M@@[(g,g),s]=(g,1)@@ 把 @@M@@G@@ 的元素写成受控换位子（commutator）。再做代数封装：在 @@M@@k=\mathbb F_2@@ 上构造有限呈现代数 @@M@@B@@、含单位 @@M@@e@@ 的单子代数 @@M@@A\subseteq B@@、像落在 @@M@@A@@ 内的单射非酉自同态 @@M@@\phi@@（记 @@M@@p=\phi(1_B)\neq 1_B@@）、角代数（corner）@@M@@pBp@@ 中与 @@M@@\phi(B)@@ 交换且满足 @@M@@t_is_j=\delta_{ij}p@@、@@M@@s_0t_0+s_1t_1=p@@ 的分裂对（splitting pairs），以及分离向量 @@M@@b_*@@。然后组装作用：取系数环 @@M@@R=B\otimes_k B^{\mathrm{op}}@@，给出有限呈现的仿射 Steinberg 群 @@M@@\Gamma_0=B^6\rtimes\mathrm{St}_6(R)@@。障碍在于 @@M@@\mathrm{St}_6(R)\to\mathrm E_6(R)@@ 的核；论文的关键定理证明由 @@M@@\psi=\phi\otimes\phi^{\mathrm{op}}@@ 诱导的系数映射一步湮灭整个核：先借经典 Steinberg 中心性论证（用作用外指标）与”角等价”引理把核元素变为中心元，再用四个两两正交又彼此等价的角（@@M@@P=E_0+E_1@@，@@M@@E_0=E_{00}+E_{01}@@）比较其像，得 @@M@@z_{E_0}=z_{E_1}=z_{E_{00}}=z_{E_{01}}@@ 且 @@M@@z_{E_0}=z_{E_0}^2@@，故为平凡——全程无需任何中心性假设。随后取映射环面（mapping torus）：@@M@@M_\infty=\varinjlim(B,\phi)@@，作用集 @@M@@X=M_\infty^6@@，群 @@M@@\Gamma\cong(M_\infty^6\rtimes\mathrm E_\infty)\rtimes\mathbb Z@@，其中 @@M@@t@@ 平移”层级”。任何有限组坐标先落进某个 @@M@@B@@ 层、再前进一步便进入单代数 @@M@@A@@；单性给出 @@M@@AmA=A@@，使初等矩阵能把任一非零坐标改成任意值，从而把非零向量标准化为 @@M@@(0,\dots,0,e)@@，加上平移即得二重传递。忠实性靠两条：@@M@@b_*@@ 在 @@M@@\psi@@ 之后探测每个非零系数；@@M@@p\neq 1_B@@ 使层级严格递增、平移 @@M@@t@@ 可被察觉。零点稳定子为 @@M@@\mathrm E_\infty\rtimes\langle t\rangle@@，有限生成。最后用平衡对角矩阵把 @@M@@\widehat G@@ 放进线性部分：@@M@@[D_{12}(a_g),D_{13}(b)]=\mathrm{diag}(\bar\nu((g,1)),1,1,1,1,1)@@。整套代数数据由一对互相编码的幺半群（monoid）给出：从程序指标句法地编译出有限呈现幺半群，其带预算的部分求值器让归约调用严格变短，经 Kleene 递归定理取不动点、按长度归纳证全景合流；”选择子”规则 @@M@@\mathtt d\mathtt l^{N_j}w_i\mathtt r^{N_j}\mathtt h\to\varepsilon/\zeta@@ 在收缩幺半群代数中逐一隔离基项而造出单代数，分离符 @@M@@\mathtt z@@ 区分有序对给出忠实探测器。
本篇为 OpenAI 批量产出的预印本之一，主结果暂无 Lean 形式化证明，请以社区核验为准；OpenAI 官方声明”未经形式化的结果可能有问题”。它是结果族 250 的基石篇：两篇姊妹篇分别把结论强化为 @@M@@F_\infty@@ 型单超群与含一切有限呈现群的万有群，三者共享同一套代数封装与编码机制、互为支撑。论文外部引用 Zaremsky 与 Belk–Zaremsky 的已发表判据，自身新颖内核是”代数封装定理”与 Steinberg 核一步湮灭；附录中编译器求值器的完整证明技术性较强，此处从略。
问 1：证明里最关键、也最脆弱的一步是什么？
答：Steinberg 核的一步湮灭。仿射 Steinberg 群 @@M@@\Gamma_0=B^6\rtimes\mathrm{St}_6(R)@@ 中 @@M@@\mathrm{St}_6(R)\to\mathrm E_6(R)@@ 的核是忠实作用的障碍，引言称”由 @@M@@\psi=\phi\otimes\phi^{\mathrm{op}}@@ 诱导的系数映射一次湮灭整个核”，靠两对分裂对的角恒等式在 Steinberg 展示里精确计算，且”无需任何中心性假设”。这是全文代数心脏：角等价推理若有一处符号或指标出错，映射环面里的忠实性就崩塌。
问 2：哪个假设最不能去掉？
答：@@M@@G@@ 有限生成。字问题本身依赖一份有限的生成元”考卷”；对任意可数群叙述 Boone–Higman 猜想需要换成枚举呈现的语言。另一个不可去的是单性中的”非平凡”：反向推理用 Kuznetsov 的并行搜索，其前提是非平凡有限呈现单群，平凡群会立刻退化。
问 3：与 Boone–Higman 1974 原定理相比，新意究竟在哪？
答：原定理是 @@M@@G\le H\le K@@、@@M@@H@@ 单、@@M@@K@@ 有限呈现，两个性质分属两个群；Thompson 1980 只推进到有限生成单超群。本文新内核有二：一是定理 thm:envelope 的”置换包络”——有限呈现＋忠实二重传递＋点稳定子有限生成，恰好凑齐 Zaremsky 2024 的 type (A) 判据；二是”选择子”技术把 Boone–Higman 半群版里的 contextual-collapse 强化为逐项隔离，造出所需的单代数。
问 4：AI 生成证明最可能在哪里出错？
答：bootstrap 与编译器部分。有限呈现幺半群从程序指标”句法地”编译、带预算的部分求值器让调用严格变短、Kleene 递归定理取不动点再按长度归纳证全景合流——这是自指与归纳交织的重灾区，附录 compiler 的求值器证明技术性极强，一处预算不等式反向就会全局崩盘。本篇无形式化，风险真实。
问 5：为什么作用要搭在 @@M@@M_\infty^6@@ 这种映射环面上？
答：有限呈现来自有限代数 @@M@@B@@，单性来自子代数 @@M@@A@@，两者不能同在一个代数里；直极限 @@M@@M_\infty=\varinjlim(B,\phi)@@ 让任何有限组坐标先落进某个 @@M@@B@@ 层、再前进一步进入 @@M@@A@@，”晚一步才有单性可用”。平移给点的传递性，线性部分在 @@M@@A@@ 的单性下传递于非零向量，合成二重传递。
问 6：下游谁在用？结果族 250 的另外两篇什么关系？
答：两篇姊妹篇（@@M@@F_\infty@@ 型单超群、含一切有限呈现群的万有群）直接复用本文的代数封装与编码机制并强化结论；算法群论与判定问题方向（Higman 嵌入谱系、双曲群、映射类群等此前的特殊族结果）从此获得统一刻画。但三篇共享同一套底座，底座若错则连坐。
总评
正面解决悬置五十余年猜想的地标性工作，路线（代数封装＋Zaremsky 判据）清晰可信；最大风险是未经形式化的编译器/自引用机器，以及三姊妹篇的共同模式失效。