结果族 156：Borsuk’s conjecture fails in dimension nine · 学科：Combinatorics · 验证状态：主结果已 Lean 形式化
一张直径为 2 的圆形大饼，切成三块 120° 扇形，每块直径只有 √3≈1.73，都变小了。Borsuk 在 1933 年猜测：任何 d 维空间中直径为正的集合，都能切成 d+1 块直径严格更小的部分。这篇论文在 9 维造出反例：有一个集合，10 块不够切。
关键词卡片
看个具体例子
平面情形：圆盘切三块扇形，每块直径 √3≈1.73，严格小于 2：
反例本身：取 ℝ⁴ 中所有单位向量 u 的”影子矩阵”P=uuᵀ 的全体，它落在九维空间里，直径恰为 √2——两个影子矩阵距离最大，当且仅当对应直线互相垂直（@@M@@\|P_u-P_v\|_F=\sqrt2@@）。论文证明 b(X) 大于 10，而 10=d+1，猜想失效；同一构造还推广到每个 d≥9。证明思路是把覆盖问题化为射影空间上的映射，再用模二度与有限组合推出矛盾。
为什么值得关心
把反例维度纪录从 63 一举压到 9，且首次用连续构形（而非有限点组）攻下 Borsuk 问题；Lean 机器验证为这条横跨几何、拓扑与组合的长论证提供了强背书。
已 Lean 形式化
第一级台阶
导读里的”切饼”说的是：给一个有确定直径的点集，问至少要切几块，才能让每块的直径都严格变小。圆饼切三块扇形就够，Borsuk 猜想猜 d 维空间切 d+1 块总够。导读里的”影子机器”说的是：把每条过原点的直线映射成它在该方向上的投影矩阵，直线之间的夹角关系被原封不动翻译成矩阵之间的距离关系。对象是矩阵空间里的一个紧集；操作是量距离、切分、覆盖。
第二级台阶
精确化：集合的直径是其中两点距离的上确界；b(Y) 记把 Y 覆盖成直径都严格变小的块所需的最少块数。取四阶实对称矩阵空间，配 Frobenius 范数（把矩阵当向量量长度），迹为一的仿射超平面是九维欧氏空间。令 X 为全体秩一正交投影矩阵 P=uuᵀ（u 为单位向量）之集；恒等式 ‖P_u−P_v‖²_F=2−2⟨u,v⟩² 说明：两个投影矩阵相距恰为 √2，当且仅当对应直线互相垂直，故 X 的直径是 √2。
第三级台阶
主定理断言：X 不能被 10 个直径严格小于 √2 的集合覆盖，即 b(X)>10=9+1，Borsuk 断言在九维失效；推论用”在直径距离处添加新点”把反例推广到每个更高维度。假设与语境：X 紧、直径为正，正是 Borsuk 问题的适用对象；此前全部反例都是有限点组且维度停在 63，本文首次用连续构形（实射影空间的完整紧像）降维。注意定理未断言 9 是失效的最小维度，也未给出 b(X) 的精确值——它只证明十块不够。
本文构造了 @@M@@\mathbb{R}^9@@ 中的紧集——@@M@@\mathbb{R}^4@@ 上全体秩一正交投影矩阵在 Frobenius 度量下的像——其直径为 @@M@@\sqrt2@@，却不能被 10 个直径严格小于 @@M@@\sqrt2@@ 的集合覆盖，从而在 9 维推翻 Borsuk 覆盖猜想，把反例维度纪录从 63 一举压到 9。
1933 年 Borsuk 提出划分问题：@@M@@\mathbb{R}^d@@ 中每个直径为正的有界集，能否用 @@M@@d+1@@ 个直径严格更小的子集覆盖？记 @@M@@b(Y)@@ 为所需子集个数的最小值，猜想即断言 @@M@@b(Y)\le d+1@@。Kahn 与 Kalai 在 1993 年借助 Frankl–Wilson 的禁距定理（forbidden-intersection theorem）在高维推翻了它，此后反例维度被持续压低：Nilli 的 946、Raigorodskii 的 561、Hinrichs 用 Leech 格球码（spherical code）得到的 323、Bondarenko 与 Jenrich–Brouwer 用强正则图（strongly regular graph）得到的 65 与 64，直到 2026 年 Grinsztajn 的 63。这些反例都是有限点组，继续降维极为困难。本文改用连续构形——实射影空间 @@M@@\mathbb{RP}^3@@ 经投影矩阵嵌入的完整紧像——并直面新困难：它的”面”来自映射的坐标支撑而非三角剖分的单纯形，Walkup、Arnoux–Marin 等关于 @@M@@\mathbb{RP}^3@@ 三角剖分的经典顶点数下界无法直接套用，面结构必须从映射本身重新推导。
定理：设 @@M@@\operatorname{Sym}_4(\mathbb{R})@@ 为实对称 @@M@@4\times 4@@ 矩阵空间，配 Frobenius 范数 @@M@@\|A\|_F^2=\operatorname{tr}(A^2)@@；迹一超平面 @@M@@\{\operatorname{tr}A=1\}@@ 是九维欧氏空间（论文给出到 @@M@@\mathbb{R}^9@@ 的显式等距映射）。紧集
@@M@@DX=\{uu^{\mathsf T}:u\in\mathbb{R}^4,\ \|u\|=1\}@@
由全体秩一正交投影矩阵（rank-one orthogonal projector）组成，其直径为 @@M@@\sqrt2@@，且不能被 10 个直径严格小于 @@M@@\sqrt2@@ 的集合覆盖，即 @@M@@b(X)>10@@。于是在 9 维 Borsuk 断言失效；论文还给出推论，把同一构造推广为每个 @@M@@d\ge 9@@ 维的紧反例。几何上一切归结为公式 @@M@@\|P_x-P_y\|_F^2=2-2\langle u,v\rangle^2@@：两个投影矩阵相距恰为 @@M@@\sqrt2@@，当且仅当它们对应的直线正交。
证明分四大步：先把覆盖问题化为射影空间上的映射，再做矩阵扩张，然后用模二度约束支撑复形，最后归结为有限组合矛盾。
先做几何约化。若 @@M@@X@@ 被 @@M@@m@@ 个直径 @@M@@<\sqrt2@@ 的集合覆盖，则把每个集合稍稍加厚为开集（直径仍 @@M@@<\sqrt2@@），拉回 @@M@@\mathbb{RP}^3@@ 后用光滑单位分解得到非负、和为 1 的函数组 @@M@@f_1,\dots,f_m@@，使得正交直线的正坐标标号集 @@M@@S(x)@@ 与 @@M@@S(y)@@ 不相交——此即”容许映射”（admissible map）。再做矩阵扩张：令 @@M@@H(v)=\|v\|^2f([v])@@，对半正定矩阵按球面积分 @@M@@E(Q)=k\int H(Q^{1/2}u)\,d\mu(u)@@，其正标号恰为 @@M@@Q@@ 的值域中直线用到的标号之并；对一般对称矩阵写 @@M@@A=A_+-A_-@@，令 @@M@@F(A)=E(A_+)-E(A_-)@@。正负谱子空间彼此正交，两组正标号无相消，故 @@M@@\|F(A)\|_1=\operatorname{tr}|A|@@，归一化后 @@M@@F@@ 成为球面间的奇映射（odd map）。
然后是拓扑核心。奇映射 @@M@@S^n\to S^d@@ 要求 @@M@@n\le d@@，故 @@M@@m\ge N_k=k(k+1)/2@@；@@M@@k=4@@ 时即 @@M@@m\ge 10@@，而 @@M@@m=10@@ 为等式情形，此时 @@M@@F@@ 的模二度（mod-2 degree）为 1。对支撑复形的任一极大面 @@M@@I@@，在单个仿射坐标卡内取水平集 @@M@@L@@，并在 @@M@@L@@ 上由正交补构成的球丛中诱导出奇映射 @@M@@G@@：一方面 @@M@@F@@ 的奇度强制 @@M@@G@@ 的正则原像个数为奇数；另一方面当 @@M@@\dim L>0@@ 时，Stiefel–Whitney 类的拉回计算迫使诱导的射影丛间映射模二度为零、原像数应为偶——矛盾。由此每个极大面恰含 4 个标号（四面体），且全部四面体之和构成 @@M@@\mathbb{F}_2@@ 闭链：每个三角形属于正偶数个四面体。
最后化为有限组合矛盾。把 @@M@@f@@ 限制到某四面体见证直线的正交补 @@M@@\mathbb{RP}^2@@ 上，在 6 个补标号上得到”三角形系统”——每对互补三元组恰取其一、每对标号恰属于两个三角形；该系统刚性极强：顶点链环均为五边形圈，任何对换都不能保持它。回到 10 标号层面，沿相邻四面体搬运这些系统，依次得出每个三角形恰属两个四面体、边的链环只能是 3 或 4 圈，标号最终被组织成大小为 @@M@@3,2,2@@ 的”伙伴块”（partner block）外加 3 个余留标号；于是必有一个三角形至多属于一个四面体，与”恰属两个”矛盾。故容许映射 @@M@@\mathbb{RP}^3\to\Delta^9@@ 不存在，@@M@@b(X)>10@@。
本篇主结果已由 Lean 形式化验证（结果族 156 附有对应 Lean 文档），机器检查为这一横跨几何、拓扑与组合的长论证提供了强背书；OpenAI 官方声明”未经形式化的结果可能有问题”，而本篇恰属已形式化之列，可信度较高。本结果族仅此一篇手稿，无姊妹篇互相支撑，但结论与 Kahn–Kalai 以来的反例谱系完全相容，且论文显式给出九维等距坐标，便于独立复核。需注意：论文并未断言 9 是 Borsuk 猜想失效的最小维度，也未确定 @@M@@b(X)@@ 的精确值。
问 1：证明里最关键也最脆弱的一步是什么？
（答：拓扑核心处的等式情形分析。奇映射 Sⁿ→Sᵈ 要求 n≤d 给出 m≥k(k+1)/2=10，而反证恰在等式 m=10 处工作：模二度为 1，配合 Stiefel–Whitney 类拉回迫使球丛诱导映射的原像数为偶，与奇度要求的奇数个原像矛盾，从而每个极大面恰含 4 个标号且构成 F₂ 闭链。等式情形里”每个极大面”都必须逐一排除例外，是全文最细的针脚。）
问 2：为什么改用连续构形，而不是沿用有限点组路线？
（答：有限路线经 Kahn–Kalai、Raigorodskii、Hinrichs、Bondarenko 一路压到 63 维后逼近极限；连续构形（RP³ 的完整紧像）的”面”来自映射的坐标支撑而非三角剖分单纯形，Walkup、Arnoux–Marin 关于 RP³ 三角剖分顶点数的经典下界套不上，面结构只能从映射本身重推——这既是降维成功的钥匙，也是新增的脆弱面。）
问 3：”10 块不够”与覆盖的染色解释有什么联系？
（答：直径严格小于 √2 的块不能同时含两条正交直线的投影矩阵，故覆盖相当于给正交图染色、无单色正交对。经典的 Borsuk–Ulam 型论证只给 χ≥4 一类的下界；本文通过对称矩阵扩张构造奇映射到标号单纯形，把下界顶到 10，是对该图更精细的拓扑探测。）
问 4：方法为什么不直接给出 b(X) 的精确值或更小的反例维度？
（答：论证依赖奇映射维数界的等号 m=10：要证明 11 块不够，需要全新机制；而降维受制于 k=4 的投影矩阵构形——k=3 时迹一超平面只有 5 维且奇映射论证不再闭合。论文明说未断言 9 是最小失效维度，四至八维仍开放（二维、三维 Borsuk 已知成立）。）
问 5：AI 生成证明在这篇的典型风险还剩多少？
（答：主结果已 Lean 形式化，机器层面风险基本排除。残余风险在跨域接缝：几何（‖P_u−P_v‖²=2−2⟨u,v⟩² 恒等式）、拓扑（模二度、示性类）、组合（三角形系统刚性、五边形链环、3,2,2 伙伴块）三层粘合处最易出现”叙述正确但引理引用错位”；另外覆盖集加厚为开集再配单位分解的约化步用了直径的严格 slack，属需要但容易被略读的细节。）
问 6：高维推论的构造为什么如此便宜？
（答：第 7 节的 Gram 矩阵论证是一次性添加全部新点：取 Gram 矩阵 I+¼1·1ᵀ 的 s 个向量，使每个新点与 Y 中每点及彼此都恰距 √2；于是含新点的小直径块孤立成单点，覆盖块数只增不减，九维结论直接抬升。这是对 Hinrichs–Richter、Bondarenko 既有技巧的复用，风险低。）
问 7：谁会用到它？
（答：离散与组合几何社区：Borsuk 数 b(d) 的上界与真值估计自此改写，4–8 维成为主战场；正交图的染色、射影空间的拓扑组合方法研究者也会直接引用这一构形。）
总评
把一个九十年的猜想反例维度从 63 砍到 9，且首次以连续构形破门，加上 Lean 验证背书，这是本批结果中最扎实的之一；剩余不确定性集中在 4–8 维的开放地带与方法对 b(X) 精值的沉默。