结果族 174：Deterministic construction of strong thin trees · 学科：Combinatorics · 验证状态：主结果已 Lean 形式化
设想城市群之间修了 @@M@@k@@ 条互不相干的干道。现在要选一套”骨架路网”：连通所有城市、一条不多修，还得处处谦让——无论从哪里把地图切成两半，骨架最多占用跨越切口干道的一小份（比例 @@M@@C/k@@）。干道越多，可挑选的余地越大，骨架理应越”瘦”；本文证明它永远选得出来，这正是”强”形式的含义：比例必须严格与 @@M@@1/k@@ 成正比。
关键词卡片
@@M@@n-1@@ 条）的骨架网@@M@@k@@-边连通（k-edge-connected）：任意两城之间至少有 @@M@@k@@ 条互不共享的干道@@M@@C/k@@ 比例的生成树看个具体例子
数字版定理：@@M@@k=1000@@ 连通的图中，任何一条 2000 边的割，骨架至多跨越 @@M@@C\cdot 2000/1000=2C@@ 条。比例 @@M@@C/k@@ 无法再改进：两点间连 @@M@@k@@ 条重边时，唯一的生成树必须占用割中 1 条边，占比恰为 @@M@@1/k@@。
为什么值得关心
Goddyn 2004 年猜想的”强形式”就此解决；细树是非对称旅行商问题近似算法的核心零件，比例常数直接影响算法质量。此前一般多重图上最好的存在性结果只有 @@M@@\mathrm{poly}(\log\log n)/k@@，还非构造性。
已 Lean 形式化
第一级台阶
入门导读把问题想成”城市群之间修了 @@M@@k@@ 条互不相干的干道，要选一套处处谦让的骨架路网”。翻译成半数学语言：对象是允许重边的公路网，质量保证是任意两地之间至少有 @@M@@k@@ 条不共享的干道；操作是挑一套连通全部城市、一条不多修的骨架；要求是谦让性：无论从哪里把地图切成两半，骨架占用跨越切口干道的比例不超过一个小份额，且干道越多份额越小。
第二级台阶
用本科语言精确化：生成树是连通所有顶点、恰用 @@M@@n-1@@ 条边的子图；割 @@M@@\delta_G(S)@@ 是恰有一端落在 @@M@@S@@ 内的边集；@@M@@k@@-边连通多重图指每个割都含至少 @@M@@k@@ 条边（重边按重数计）。细树就是对每个割都满足 @@M@@|\delta_T(S)|\le\frac{C}{k}|\delta_G(S)|@@ 的生成树——比例严格与连通度成反比，这正是”强”形式的含义。
第三级台阶
主定理：存在普适常数 @@M@@C@@，使每个无环、至少两个顶点的 @@M@@k@@-边连通多重图（@@M@@k\ge1@@）都有这样的细树。@@M@@C/k@@ 这一阶无法改进：两点连 @@M@@k@@ 条重边时，唯一的生成树必占割中一条，比例恰为 @@M@@1/k@@。证明是”装填—抽取—迭代稀疏化”三段式：Nash–Williams–Tutte 定理先装出约 @@M@@k/2@@ 棵边不相交的生成树；抽取定理用快捷矩阵与 Brouwer 不动点解决”矩阵决定划分、划分又决定矩阵”的自指困难；最后迭代稀疏化，每步损失 @@M@@1+O(r^{-c})@@，乘积收敛到绝对常数。
证明了强细树猜想（strong thin tree conjecture）：每个 @@M@@k@@-边连通无环多重图都含一棵生成树，与任何割的交不超过割规模的 @@M@@C/k@@ 倍（@@M@@C@@ 为普适常数）。这一阶是最优的，把此前 @@M@@\mathrm{poly}(\log\log n)/k@@ 的存在性结果推进到与连通度严格成反比。
生成树只用 @@M@@n-1@@ 条边就保持连通，却可能吃掉某个割（cut）的很大一部分。Goddyn（2004）猜想：边连通度（edge connectivity）足够高时，存在对每个割都只占小比例的生成树，即细树（thin tree）；Anari 与 Oveis Gharan 明确区分了定性形式与指定速率 @@M@@C/k@@ 的”强”形式。细树是 Asadpour 等人非对称旅行商问题（asymmetric TSP）近似算法中舍入步骤的核心，比例常数直接影响近似比。此前一般多重图上的最好结果是 Anari–Oveis Gharan 的 @@M@@\mathrm{poly}(\log\log n)/k@@-细树存在性，既差一个随 @@M@@n@@ 增长的因子，也非构造性。卡点在于：Nash–Williams–Tutte 定理保证约 @@M@@k/2@@ 棵边不相交生成树，这只让割负载的平均值小，无法保证同一棵树对所有割同时小。
定理：存在绝对常数 @@M@@C@@，使每个至少两个顶点、无环的 @@M@@k@@-边连通多重图（multigraph，重边按重数计）都有生成树 @@M@@T@@ 满足
@@M@@D|\delta_T(S)|\le \frac{C}{k}\,|\delta_G(S)|\qquad(\varnothing\ne S\subsetneq V(G),\ k\ge 1),@@
其中 @@M@@\delta_G(S)@@ 是恰有一端落在 @@M@@S@@ 内的边集。@@M@@C/k@@ 这一阶无法改进：两个顶点连 @@M@@k@@ 条重边时，唯一的生成树恰好用到那个割中一条边。常数 @@M@@C@@ 与图的规模、结构均无关。
证明是”打包—抽取—迭代稀疏化”的三段式，核心新工具是把层级结构（hierarchy）与不动点结合的快捷矩阵（shortcut matrix）方法。
先由 Nash–Williams–Tutte 定理取出约 @@M@@k/2@@ 棵边不相交的生成树，图成为 @@M@@r@@-树可装填（r-tree-packable）图。再引入快捷矩阵：正定矩阵 @@M@@D@@ 在每个非平凡割上满足 @@M@@\mathbf 1_S^{\mathsf T}D\mathbf 1_S\le|\delta_H(S)|@@，其逆赋予每条边有效电阻（effective resistance）@@M@@R_D(e)=b_e^{\mathsf T}D^{-1}b_e@@。关键的层级估计是 Anari–Oveis Gharan 的 Tree-CP 定理的多项式推论：若图带局部 @@M@@q@@-连通层级——一棵由顶点集构成的根树，每个节点在其父节点内至少跨出 @@M@@q@@ 条边——则存在快捷矩阵，使所有被标记边界 @@M@@O(A)@@ 上的平均电阻不超过 @@M@@q^{-31/40}@@。附录沿其对偶—几何路线（把顶点映入 @@M@@\{0,1\}^d@@，围绕”球袋”（bags）组出尺度几何分离的球族）给出带显式损失的完整证明。
抽取定理是全文枢纽：当 @@M@@r@@ 充分大时，@@M@@r@@-树可装填图存在 @@M@@X\succ0@@ 同时满足 @@M@@L_H\preceq X@@、割约束 @@M@@\mathbf 1_S^{\mathsf T}X\mathbf 1_S\le 3|\delta_H(S)|@@，且电阻不超过 @@M@@4r^{-1/2}@@ 的边里仍装得下 @@M@@q=\lfloor(1-r^{-1/16})r\rfloor@@ 棵不相交生成树。难点是自指：矩阵 @@M@@X@@ 决定电阻阈值图和它的装填划分（packing partition），响应矩阵的构造又依赖这个划分。绕行的办法是：把可能出现的划分按规模分进 dyadic 箱，每箱取最细代表，这些代表划分的部件合成层叠族（laminar family）从而构成层级；对该层级取快捷矩阵作响应，便得到对一切阈值同时成立的坏边计数（至多 @@M@@40r^{-1/4}M_s@@ 条）。随后用单位分解把有限多个响应插值成紧凸集上的连续自映射，以 Brouwer 不动点定理（附录从 Sperner 引理自足证出）过渡到不动点并取极限；条件的闭性把”绝大多数边电阻小”传给极限矩阵，最终逼出装填划分只能是平凡的 @@M@@\{V\}@@。
最后迭代稀疏化：每步保留低电阻边构成的子图，装填数与割规模近似同步减半，每步只损失 @@M@@1+O(r^{-c})@@ 的比值；参数几何递减使损失乘积收敛到绝对常数。迭代到只剩常数棵树时图仍连通，任取生成树，其对每个割的占用比例即为 @@M@@C/k@@ 量级。其中矩阵减半所用的签名工具依赖 Marcus–Spielman–Srivastava 矩阵划分定理（Kadison–Singer 定理），论文附录设有专节。
主结果已由 OpenAI 完成 Lean 形式化。需注意：本文证明经紧性论证与不动点极限，作者明言”不对计算代价作任何承诺”，属于纯存在性结果；同族姊妹篇将该框架算法化，给出确定性多项式时间构造，与本文互为支撑——本文的层级几何正是姊妹篇的直接输入。按 OpenAI 官方声明，未经形式化的结果可能存在问题，而本文主结果已经形式化，可信度较高。
问 1：证明最关键、也最脆弱的一步在哪？
（答：抽取定理。难点是自指：正定矩阵 @@M@@X@@ 同时决定电阻阈值图与它的装填划分，而响应矩阵的构造又依赖这个划分。论文把可能出现的划分按规模分进 dyadic 箱、每箱取最细代表合成层叠族，对该层级取快捷矩阵得到对一切阈值同时成立的坏边计数，再用单位分解插值出紧凸集上的连续自映射，以 Brouwer 不动点过渡并取极限，逼出装填划分只能是平凡的 @@M@@\{V\}@@。）
问 2：为什么 @@M@@C/k@@ 这一阶不能再改进？
（答：两点之间连 @@M@@k@@ 条重边时，生成树唯一，必须占用那个割中恰好一条边，占比 @@M@@1/k@@。任何普适比例的下限就是 @@M@@1/k@@ 的常数倍；定理把此前 Anari–Oveis Gharan 的 @@M@@\mathrm{poly}(\log\log n)/k@@ 中随 @@M@@n@@ 增长的因子整个去掉，一步到位到理论最优。）
问 3：Nash–Williams–Tutte 已给 @@M@@k/2@@ 棵边不相交生成树，为什么还不够？
（答：它只保证割负载的平均值小：@@M@@k/2@@ 棵树分摊一个割，平均每棵占约 @@M@@2/k@@。但细树要求同一棵树对所有割同时小——平均小与一致小之间隔着全部困难，这正是需要有效电阻权重、快捷矩阵与不动点论证的原因。）
问 4：哪个假设看似技术性、撤掉就出问题？
（答：无环（loopless）。环对连通与割毫无贡献，却会干扰装填计数与电阻估计；”至少两个顶点、@@M@@k\ge1@@“是防退化条款；重边必须按重数计——细树猜想本来就是多重图语境，忽略重数会让 @@M@@k@@-边连通失去意义。）
问 5：层级估计里的 @@M@@q^{-31/40}@@ 这个奇怪指数从哪来？
（答：它是 Anari–Oveis Gharan 的 Tree-CP 定理的多项式推论：带局部 @@M@@q@@-连通层级（每个节点在父节点内至少跨出 @@M@@q@@ 条边）的图存在快捷矩阵，使被标记边界上的平均有效电阻不超过 @@M@@q^{-31/40}@@。论文附录沿对偶—几何路线（顶点映入 @@M@@\{0,1\}^d@@、围绕球袋组出尺度分离的球族）给出带显式损失的完整证明，而非仅引用。）
问 6：最可能出错的模式？机器核验覆盖到哪？
（答：紧性与不动点极限是 AI 生成证明最易翻车之处——把严格不等式传给极限时丢失严格性，或在单位分解插值处破坏连续性。本文主定理已 Lean 形式化，主链风险被机器核验覆盖；但作者明言”不对计算代价作任何承诺”，这是纯存在性结果，构造性版本由姊妹篇承担。）
问 7：谁会用到它？
（答：非对称旅行商问题近似算法是直接受益者——Asadpour 等的舍入步骤以细树为核心零件，比例常数直接影响近似比；矩阵减半所用的 MSS 矩阵划分定理（Kadison–Singer）也使谱稀疏化社区关注此框架。姊妹篇把框架算法化为确定性多项式时间构造，本文的层级几何是其直接输入。）
总评
Goddyn 2004 年猜想强形式的完全解决，把细树比例推进到理论最优的 @@M@@C/k@@ 且主定理经 Lean 核验；残余风险在未形式化的附录细节与其纯存在性性质——可用构造还需姊妹篇支撑。