结果族 174：Deterministic construction of strong thin trees · 学科：Combinatorics · 验证状态：暂无形式化证明，请以社区核验为准
想象一座防守森严的城市：道路网结实到想把它拦腰切断，必须同时炸掉至少 k 条路。数学家早已证明这样的路网里藏着一条”纤细但连通”的骨架线路，可那条证明像一张存在性支票——保证金库里有这笔钱，却取不出来。这篇论文造出了”取款机”：一个确定性算法，能在多项式时间里把这条细骨架真正算出来。
关键词卡片
看个具体例子
定理说算法输出的树 T 满足 @@M@@|\delta_T(S)|\le\frac{C}{k}\,|\delta_G(S)|@@。代入 k=100、某个横跨 200 条边的割：树只派至多 2C 条边跨线。下图中虚线是一个割，灰线是图的边，红线是算法造出的细生成树——它在割处只留 2 条。
为什么值得关心
细树是网络设计与近似算法的关键零件，把”存在”变成”可算”才真正可用；即使平行边以二进制紧凑编码，算法依然多项式时间完成。
暂无形式化证明（AI 结果待核验）
第一级台阶
导读把连通图比作防守森严的城市：想拦腰切断，必须同时砍掉至少 k 条路。现在把比喻翻译成半数学语言：对象是一个由顶点和边组成的路网；操作是从中挑出一个保持连通、边数最少的子网，并且要求它在任何可能的”切断位置”处占用道路的比例都很小。
第二级台阶
用本科图论术语精确化。对顶点子集 S，把一端在 S、另一端在 S 之外的所有边记作一个割 δ(S)。若每个非平凡割都至少含 k 条边，图称为 k-边连通。生成树 T 是恰用 n−1 条边连通全部顶点的子图；若对每个割都有 T 占的边数不超过图总边数的 α 倍，则称 T 是 α-细的。
第三级台阶
定理在算法的语境下陈述：存在绝对常数 C 与确定性算法，输入 k-边连通无环多重图（边可显式列出，也可按二进制重数紧凑编码），在输入长度的多项式时间内输出 C/k-细的生成树。”k-边连通”挡住了割太小、任何树都必然霸占比割的麻烦；”允许二进制编码”挡住了实际边数达到输入长度指数倍的膨胀困难；无环假设排除了对割无贡献的自环。结论把姊妹篇经由紧性论证与不动点得到的纯存在性支票，兑换成可以真正运行的取款机。
给出确定性多项式时间算法：对任意 @@M@@k@@-边连通多重图（重边多重数可用二进制编码），构造出对每个割至多占 @@M@@C/k@@ 比例的生成树。它把姊妹篇证出的强细树猜想变成可执行构造，运行时间对输入的二进制长度是多项式的。
强细树猜想说 @@M@@k@@-边连通图必有 @@M@@C/k@@-细的生成树，姊妹篇已证明其存在性，但那条路线经过紧性论证与 Brouwer 不动点，只保证某个快捷矩阵存在，不给任何统一的有限搜索界，因此无法直接变成算法。算法化另有三道难关：其一，证明中的”白化”（whitening）会产生无理数矩阵，多项式位算法必须全程用有理数并逐一控制精度损失；其二，矩阵划分步骤原先用的是 Marcus–Spielman–Srivastava 的存在性定理，需要换成能真正算出符号的构造版本；其三，若平行边多重数以二进制书写，图的实际边数可达输入长度的指数倍，逐条展开不可行。
定理（算法版强细树）：存在绝对常数 @@M@@C@@ 与确定性算法，输入至少一个顶点、@@M@@k\ge1@@ 的 @@M@@k@@-边连通无环多重图 @@M@@G@@，输出满足
@@M@@D|\delta_T(S)|\le \frac Ck\,|\delta_G(S)|\qquad(\varnothing\ne S\subsetneq V(G))@@
的生成树 @@M@@T@@；运行时间对输入的二进制编码长度是多项式，无论边被逐条显式列出，还是多重数以二进制给出；单顶点图输出空树。作为附带收获，算法还给出”费用与割同时舍入”（Corollary：给定每割质量至少为 1 的非负有理边权与任意非负有理费用，可在正支撑中找到割负载与总费用均为相应分数量的常数倍的树），且不需要费用满足任何度量假设。
框架沿用姊妹篇的”打包—稀疏化—迭代”，但把三处存在性论证替换为有限计算。
先用 Nash–Williams–Tutte 定理装出 @@M@@\lfloor k/2\rfloor@@ 棵边不相交生成树。核心的稀疏化引理把含 @@M@@r@@ 棵树的显式图 @@M@@H@@ 变为子图 @@M@@H'@@：仍含 @@M@@r'\in[r/4,\,r/2]@@ 棵树，每个割缩至 @@M@@a_r=\tfrac12+3C_sr^{-1/8}@@ 倍，且比值损失 @@M@@a_r/(r'/r)\le1+C_1r^{-1/16}@@。由于 @@M@@r_i@@ 每步至少减半，@@M@@\sum_i r_i^{-1/16}@@ 被几何级数控制，累积损失是一绝对常数；迭代到只剩 @@M@@O(1)@@ 棵树时图仍连通，任取其生成树即为 @@M@@C/k@@-细。这一数值结构与存在性证明完全平行。
第一处替换处理自指问题：快捷矩阵须与”由它自身决定的划分”相容，而紧性/不动点不给有限界。改在度量锥（metric cone，中心化半正定矩阵加平方距离三角不等式）上优化——该锥的约束数是多项式的；用连续的容量”坡道”代替硬阈值选边，经 uncrossing 把障碍归约到一条划分链，再用椭球法（ellipsoid method）做精确有理分离，配合构造性图拟阵划分（graphic matroid partition）取出整数装填。
第二处替换无理白化：按 Barthe 的变分方法做对数行列式归一化，把堆叠向量有理逼近后，将其协方差精确补全为单位阵。第三处替换存在性矩阵划分：采用 Ezeunala–Jiang 的公开构造性符号化方法，附录给出带常数的定量实现；有理证书保证下一步所需的全部割与装填估计，且迭代中乘法损失乘积保持有界。
二进制多重数单独归约：令 @@M@@c'_{uv}=\min\{c_{uv},k\}@@、@@M@@a_{uv}=\lfloor 2n^2c'_{uv}/k\rfloor@@，得到少于 @@M@@n^4@@ 条显式边、每个割至少 @@M@@n^2@@ 的显式图 @@M@@\widetilde G@@；在 @@M@@\widetilde G@@ 上跑显式算法，输出树在 @@M@@\widetilde G@@ 中 @@M@@C/n^2@@-细，映射回原图即 @@M@@2C/k@@-细。归约中的算术只依赖 @@M@@\log k@@、多重数编码长度与 @@M@@n@@。
本文暂无形式化证明；姊妹篇的存在性定理已 Lean 形式化，且本文以其层级几何为主要输入，两篇互相支撑。按 OpenAI 官方声明，未经形式化的结果可能存在问题，本文算法部分的常数与精度控制尤其需要社区核验。
问 1：算法版证明里最脆弱的一步替换在哪里？
答：是”快捷矩阵须与由它自身决定的划分相容”这一步。姊妹篇用紧性与 Brouwer 不动点，不提供统一有限搜索界；本文改在度量锥（中心化半正定矩阵加平方距离三角不等式）上优化，并主动扩大检验锥——这反而加强了所需不等式，必须靠新构造的加倍距离轮廓多面体重做 bag 与 charging 论证。这是全文最新的几何论证，最需要核验。
问 2：C/k 这个阶为什么不能再改进？
答：论文指出阶是紧的：两个顶点之间连 k 条平行边时，唯一割含 k 条边，而任何生成树只能在其中取 1 条，比例恰为 1/k。故任何 o(1/k) 的细度都不可能，改进空间只在常数 C。
问 3：与 Anari–Oveis Gharan 的 poly(log log n)/k 存在性结果相比，真正新意何在？
答：新意不在细度（他们的界更优），而在两点：其一，对任意多重图给出确定性的多项式位构造——此前构造性逆连通性界只有平面/固定曲面（Oveis Gharan–Saberi）与层状割族（Klein–Olver 一系）；其二，平行边多重数可用二进制编码而运行时间仍多项式，这是存在性路线完全没有触及的输入模型。
问 4：二进制重数归约是否可信？
答：这步相对独立：令 c′=min(c,k)，再取 ⌊2n²c′/k⌋ 得到少于 n⁴ 条显式边、每割至少 n² 的显式图；在其中跑显式算法得 C/n²-细的树，映射回原图即 2C/k-细。所涉算术只依赖 n 与编码长度，逻辑短，较易核验。
问 5：无理数白化如何变成有理计算？
答：按 Barthe 的变分方法做对数行列式归一化，把堆叠向量有理逼近后，将协方差精确补全为单位阵；再用 Ezeunala–Jiang 的公开构造性符号化方法（附录给出带常数的定量实现）替换 Marcus–Spielman–Srivastava 的存在性矩阵划分定理。有理证书保证下一步所需的全部割与装填估计。
问 6：AI 生成证明最可能在哪里出错？
答：典型风险是精度与常数的累积控制：迭代中 r 每步至少减半，需 ∑r^(−1/16) 的几何级数论证保证乘法损失乘积有界；三处替换各自引入常数，任一处算错都可能使最终 C 失效。论文未给出 C 的显式数值，核验者必须重走整条定量链。
问 7：谁会实际用到这个算法？
答：近似算法社区最直接：细树是非对称 TSP 最大熵舍入的经典零件，论文推论还给出”费用与割同时舍入”且不需要成本的度量假设，可用于网络设计与分数舍入管线；形式化社区则可把本算法接到姊妹篇已 Lean 化的层级几何上。
总评
这项工作把强细树猜想从”存在”推进到”可算”，并覆盖二进制编码输入，是对算法工具箱的实质贡献；最大风险在于三处构造性替换中全新的度量锥几何与精度论证未经形式化，常数链条最容易藏错。