结果族 181：The Erdős–Gallai cycle-decomposition conjecture · 学科：Combinatorics · 验证状态：主结果已 Lean 形式化
一团乱麻般的电线，总能理成一圈圈的”环”再剩几根单线吗？1966 年 Erdős 等人猜测：任何 n 个顶点的图，其边总能拆成至多”常数 × n”个圈与单边。此后近六十年，最好的结果总差一个缓慢增长的尾巴；这篇论文终于把尾巴剪掉，证明了最优的线性界。为什么必须允许单边？因为森林里一个圈也没有；为什么线性阶不能再降？因为一棵树就得用上 n−1 条单边。
关键词卡片
看个具体例子
主定理的数字版：@@M@@E(G)@@ 可划分成至多 @@M@@Cn@@ 个简单圈与单边。看 @@M@@K_5@@：5 个顶点、10 条边、每点度数 4，可完全拆成红、蓝两个 5 圈（下图），2 个部件远小于 C·5；而一棵树只能全用单边，恰好说明线性阶是最优的。
为什么值得关心
Erdős–Goodman–Pósa 猜想就此解决；推论还给出 Euler 图的线性圈分解，经典图论的一块拼图就此归位。从 @@M@@O(n\log\log n)@@ 到 @@M@@O(n\log^* n)@@，前人一步步逼近，本文终于摘下了挂在”线性”上的那颗果子。
已 Lean 形式化
第一级台阶
导读把问题比作理乱麻：电线总能理成一圈圈的环、再剩几根单线吗？翻译成半数学语言：对象是有限个顶点与边构成的简单无向网；操作是把边集划分成若干块，每块要么围成一个不重复经过任何顶点的闭合回路，要么只剩一根单独的边；问题是最少需要多少块。
第二级台阶
用本科图论术语精确化。简单圈是不重复经过顶点的闭合路径；划分要求每条边恰属于一块、块与块不共享边。必须允许单边块：森林里一个圈也没有。若所有顶点度数均为偶，图是 Euler 图，可完全拆成圈不剩单边。一棵 n 个顶点的树需要 n−1 个单边块，说明部件数的阶无法低于线性；完全二部图的例子甚至需要 (3/2−o(1))n 块。
第三级台阶
定理陈述：存在绝对常数 C，使每个 n 顶点有限简单图的边集可划分成至多 Cn 个简单圈与单边——即 Erdős–Gallai 圈分解猜想的正面解决。历史脉络是 Erdős–Goodman–Pósa 1966 年的 O(n log n)、Conlon–Fox–Sudakov 的 O(n log log n)、Bucić–Montgomery 的 O(n log^* n)，本文剪掉最后那条缓慢增长的尾巴。证明按尺度 D_j = n^{0.95^j} 分层分拆，把一段前缀的工作记账到一个扩张层，用配对折叠节省该层顶点数的固定比例，再以带位势 φ(n) = 1 − 1/√log n 的强归纳吞掉重叠开销；推论给出 Euler 图的纯圈分解与拟随机情形逼近平凡下界 Δ/2 的分解。
证明了任何 @@M@@n@@ 个顶点的有限简单无向图的边集都能划分成至多 @@M@@Cn@@ 个简单圈（simple cycle）与单边，@@M@@C@@ 为绝对常数。这正面解决了 Erdős–Gallai 圈分解猜想，把此前最好的 @@M@@O(n\log^* n)@@ 上界推进到猜想所需的最优线性阶。
一个图的边能拆成多少个圈？森林不含任何圈，所以必须允许把单边也算作部件。1966 年 Erdős–Goodman–Pósa 的论文（即 Erdős–Gallai 圈分解猜想的出处）提出：任何 @@M@@n@@ 点图的边都能划分成至多 @@M@@Cn@@ 个圈与单边，并纪录了 @@M@@O(n\log n)@@ 的上界。此后 Conlon–Fox–Sudakov（2014）改进到 @@M@@O(n\log\log n)@@，Bucić–Montgomery（2024）改进到 @@M@@O(n\log^* n)@@，距线性始终差一个随 @@M@@n@@ 缓慢增长的因子。线性阶是最优的：一棵树需要 @@M@@n-1@@ 个单边部件，完全二部图的例子甚至需要 @@M@@(3/2-o(1))n@@ 个部件。难点在于一般图同时含有稀疏区域和度数悬殊的顶点，而此前的线性界只对随机图、最小度为线性比例等特殊图类成立。
主定理：存在绝对常数 @@M@@C>0@@，使得每个 @@M@@n@@ 个顶点的有限简单无向图 @@M@@G@@ 的边集 @@M@@E(G)@@ 可以划分成至多 @@M@@Cn@@ 个部分，每部分是一条简单圈的边集或一条单边。各部分共享顶点但不共享边，每条边恰属一个部分。
定理还给出两个纯圈推论。其一：每个 @@M@@n@@ 点 Euler 图（Eulerian graph，即所有顶点度数为偶，不要求连通）的边集可划分成至多 @@M@@Cn@@ 个圈。其二：对固定的 @@M@@\delta,p>0@@，在弱 @@M@@(\varepsilon,p)@@-拟随机条件下，足够大的 Euler 图可划分成至多 @@M@@\Delta(G)/2+\delta n@@ 个圈，几乎达到平凡下界 @@M@@\Delta(G)/2@@（每个圈在任一顶点至多用两条邻边）。
证明是对 @@M@@n@@ 的强归纳（strong induction），且把归纳命题加强为”至多 @@M@@C\phi(n)n@@ 个部件”，位势 @@M@@\phi(n)=\max\{1/2,\,1-1/\sqrt{\log n}\}@@。这个 @@M@@1/\sqrt{\log n}@@ 的折扣是全局关键，用来支付分层分拆时顶点被重复计数的开销。
先按尺度 @@M@@D_j=n^{0.95^j}@@ 逐层分解。每个尺度先删去一族长度至少 @@M@@D^{1.01}@@ 的长圈，直接算作完成部件；再把剩余的边装进阶至多 @@M@@D^{1.02}@@ 的盒子（box），盒子顶点集允许少量重叠，总阶只膨胀 @@M@@1+O(1/\log D)@@ 倍。此处用 DFS 长圈论证的逆否形式：若每个不超过半数的顶点集都有足够大的外部邻域，图中就有长圈；长圈既已删尽，必存在外部邻域很小的集合，沿它做”重叠分裂”，并以对数型位势函数控制总阶增长。随后在每个盒内反复剥离稀疏割，取出顶点互不相交、割扩张度（cut expansion）至少 @@M@@D^{0.90}@@ 的碎片，残差图平均度降至 @@M@@D^{0.95}@@，恰是下一尺度的合法输入。
若各层碎片总量都小，就一路做到底，长圈加单边直接收尾。否则由前缀选择引理挑出一层 @@M@@i@@，使它连同其后 @@M@@K=200@@ 层的碎片总量都被第 @@M@@i@@ 层的总阶 @@M@@S_i@@ 控制。隔了 200 个尺度后盒中残余的边已极稀疏：把第 @@M@@i@@ 层盒子的后代归并成批（batch），在每个批与碎片的交集里取度数至多 @@M@@a=D^{0.01}@@ 的”好顶点”构成活跃集，对其做配对折叠（pair folding）。均匀随机配对下，坏边（折叠后成环或重边的边）的期望不超过活跃集总量的两倍，全部记作单边部件；商图的阶每配掉一对顶点就减少一，合计节省活跃集总量的三分之一，即 @@M@@S_i@@ 的一个固定比例。
商图的阶至多 @@M@@D^{0.30}@@，交给归纳假设后，再把商圈”提升”回原图：商圈从折叠对的一个成员进入、从另一个成员离开时，经碎片中预先随机二分的”路由器”子图接回。路由引理以 Aharoni–Haxell 超图匹配定理为核心，给出边不交、同圈内部点不交且避开禁区的路，保证每条商圈恰好提升为一条简单圈。碎片本身由小残差引理处理：随机抽取三个储水池（reservoir），其余的边分派到避开某一水池的一侧并拆成路径，再经水池内部仍保持割扩张度的样本子图闭合成圈，只留下总量至多 @@M@@\eta r@@ 的残差图递归。结算时 @@M@@S_i@@ 的系数非正，而 @@M@@\phi@@ 在 @@M@@n@@ 与 @@M@@D^{0.30}@@ 之间的增益约 @@M@@1/\sqrt{\log D}@@，足以吞掉全部 @@M@@O(n/\log D)@@ 的重叠开销；常数次序为先定绝对参数、再定尺度下限、最后选 @@M@@C@@。
据任务元信息，主结果已通过 Lean 形式化证明；文中的确定性论证亦完整，概率步骤（随机配对、随机边染色、顶点采样）只用于存在性论证。本文是结果族 181 的核心论文，其 Euler 圈分解推论与 Erdős–Gallai 猜想等价，出自同一证明。按 OpenAI 官方声明，未经形式化的结果可能有问题；本篇主结果已形式化，其余细节仍建议以社区核验为准。
问 1：为什么此前停在 O(n log^* n)，本文的破局机制是什么？
答：引言点明卡点：若每层都按全图顶点数付账，开销会随尺度层数累积成因子。本文的新机制是”前缀记账 + 顶点节省”：用前缀选择引理挑出一层，使其后 K = 200 个尺度的碎片总量都被该层总阶 S_i 控制；对该层的活跃顶点做配对折叠，每配掉一对顶点商图阶减一，合计节省 S_i 的三分之一——恰好付清递归之外的全部工作，S_i 的系数被压成非正。
问 2：证明中最脆弱的一步是什么？
答：路由引理（lem:routing）。商圈提升回原图时，一个折叠对的两个成员可能分别是圈的进出口，需要用预留扩张碎片中的路把它们接回，且要求这些路边不相交、同圈内部点不相交并避开代表元端点——引理以 Aharoni–Haxell 超图匹配为核心。提升失败一条，整条商圈就断成路径，部件数失控；这是外部重定理压力最集中的一环。
问 3：位势 φ(n) = 1 − 1/√log n 为什么是全局关键？
答：分层分拆时盒子顶点集允许少量重叠，总阶膨胀 1 + O(1/log D) 倍，累积起来是 O(n/log D) 的开销。商图阶至多 D^{0.30}，其 φ 值比 φ(n) 小约 1/√log D，平方根级增益严格盖过对数级开销——这个差阶选择是全书账本能闭合的原因。
问 4：单边部件与线性阶为什么都动不了？
答：森林不含圈，单边部件是必需的；n 顶点的树需 n−1 块，给出阶的下界；引言还援引 Bucić–Montgomery 论文第六节：完全二部图需要 (3/2−o(1))n 块。故 Cn 的阶最优，剩的只是常数 C 的真值问题，论文未给出显式 C。
问 5：与覆盖版结果（Pyber 的 n−1）有什么本质区别？
答：覆盖允许边重复使用，Pyber 1985 年证 n−1 块即可覆盖，Akbari 等改进到 n−2；但删去重复边会把圈打碎成许多路径，覆盖不给出划分。本文要求边不交划分，每条原始边全程保有单独指派——这是问题更难的原因，也是”Erdős–Gallai 猜想”的本来面目。
问 6：AI 生成证明最可能出错的模式？
答：主定理已 Lean 形式化（可信度栏注明），组合核心获机器背书。风险残余在推论与外部接口：Euler 推论的证明把单边块拆圈（偶度论证），拟随机推论整体转引 Girão–Granet–Kühn–Osthus 的等价命题——引用陈述与原文是否逐字一致不在形式化范围内。证明中的概率步骤（随机配对、随机边染色、顶点采样）只服务存在性，不影响确定性结论。
问 7：谁会用到它？
答：图分解社区直接入账：Euler 图线性圈分解与主猜想等价（GGKO 记录），拟随机 Euler 图的 Δ/2 + δn 分解逼近”每圈至多用某顶点两条邻边”的平凡下界；对组合优化中边划分、通信网络环覆盖等应用，这是从”近线性”到”线性”的定性收官。
总评
近六十年猜想的解决，多尺度记账与配对折叠的设计堪称精巧，且主定理经形式化；最大残余风险在重定理接口与推论转述，但核心已属可信度最高档。