结果族 173：Seymour’s second-neighborhood conjecture · 学科：Combinatorics · 验证状态：主结果已 Lean 形式化
把”单向关注”画成一张图。每个人看两类人：你直接关注的一步圈，和”你关注的人所关注、但你没直接关注”的两步圈。Seymour 猜想：任何单向关系网中，总有一个人他的两步圈不小于一步圈。这个 1995 年被正式记录的猜想，本文给出了完整证明。
关键词卡片
@@M@@N_1^+@@：一步直接指向的顶点集合@@M@@N_2^+@@：恰好两步才能到达的顶点集合看个具体例子
这个 6 顶点小网中，@@M@@v@@ 的一步圈是 @@M@@\{a,b\}@@ 共 2 人，两步圈是 @@M@@\{c,d,e\}@@ 共 3 人，@@M@@2\le 3@@。定理保证：无论网多大、方向多刁钻，好顶点必然存在；加权版也对——按任意非负”人气权”加权，仍有人一步圈权重不超过两步圈。它还顺带导出若干有向圈推论，例如最小入度、出度都不低于 @@M@@n/3@@ 的定向图必含有向三角形。
为什么值得关心
一般定向图情形悬置三十年，此前所有结果都要附加结构假设或放松结论；本文无条件解决，且已通过机器核验。
已 Lean 形式化
第一级台阶
入门导读把问题画成”单向关注网”：关系只许单向，不许互相关注；每个人看两类对象——一步直接关注的，和”关注的人所关注、自己却没直接关注”的两步圈。猜想说：任何这样的网中总有一个人，两步圈不小于一步圈。入门导读的 6 顶点小例里 @@M@@v@@ 的一步圈 2 人、两步圈 3 人；定理保证这样的好顶点在任何网中必然存在。
第二级台阶
用本科语言精确化：定向图是给简单图每条边定向所得的有向图——无环、无重弧、无反向弧对。对顶点 @@M@@v@@，出邻域 @@M@@N_1^+(v)@@ 是一步直接指向的顶点集；第二邻域 @@M@@N_2^+(v)@@ 是有向距离恰为二的顶点集——排除 @@M@@v@@ 自身与一步已到达者。主定理：每个非空有限定向图必有 @@M@@v@@ 使 @@M@@|N_1^+(v)|\le|N_2^+(v)|@@，不带任何连通性或度数假设。
第三级台阶
证明走反证三步。先取顶点数最少、弧数其次最少的反例，经删弧论证与”字典积膨胀”（每个顶点换成一大块传递竞赛图）得到对所有非空真子集一致的严格不等式 @@M@@|U|+|F^2(U)|<2|F(U)|@@，其中 @@M@@F@@ 是一步像算子；再用对任意有限二元关系成立的剪枝引理修复两族有序对的相容性；最后在含对角线的相容族对上极大化目标 @@M@@M+d@@，取补构造的新族严格增大目标，与极大性矛盾。”恰为二”的排除是猜想的灵魂：它使结论非平凡。
论文正面证明了 Seymour 第二邻域猜想：任何非空有限定向图中必有顶点 @@M@@v@@ 满足 @@M@@|N_1^+(v)|\le|N_2^+(v)|@@，即有向距离恰为二的顶点数不少于出邻点数。这一自 1995 年记录以来悬置三十余年的有向图基本问题就此解决，主结果并已通过 Lean 形式化验证。
定向图（oriented graph）是给简单图的每条边各指定一个方向所得的有向图：无环、无重弧、也无反向弧对。对顶点 @@M@@v@@，记 @@M@@N_1^+(v)@@ 为出邻域（out-neighborhood），@@M@@N_2^+(v)@@ 为有向距离恰为二的顶点集——两步可达、且排除 @@M@@v@@ 自身与一步已到达者。Seymour 第二邻域猜想断言：总存在 @@M@@v@@ 使 @@M@@|N_1^+(v)|\le|N_2^+(v)|@@。猜想由 Dean 与 Latka 于 1995 年记录。最著名的竞赛图（tournament，任意两顶点间恰有一弧）特例即 Dean 猜想，由 Fisher 于 1996 年借助 Farkas 引理构造的概率分布证明，Havet 与 Thomassé 后以局部中位序给出纯组合证明；此后 Fidler–Yuster 等处理了缺一个匹配、星形或团的近竞赛图，Kaneko–Locke 证明了最小出度不超过 6 的情形（近期计算机辅助工作推进到 7），Chen–Shen–Yuster 与 Huang–Peng 分别给出约 0.657 与 0.716 的普遍比例下界，随机图取向与稠密情形亦有专题研究。但这些成果均依赖附加结构或放松结论，一般猜想始终未决。
主定理（定理 1.1）：每个非空有限定向图都有顶点 @@M@@v@@ 使 @@M@@|N_1^+(v)|\le|N_2^+(v)|@@，不带任何连通性或度数假设；汇点平凡地满足结论。论文又经 Seacrest 的等价性导出加权形式（第 5 节推论）：对任意非负顶点权 @@M@@\eta@@，存在 @@M@@v@@ 使 @@M@@\eta(N_1^+(v))\le\eta(N_2^+(v))@@；存在总质量为 1 的非负权使每个顶点都满足该不等式；并有相应的弧加权（arc-weighted）形式。第 6 节给出有向圈推论：无有向三角形的图中必有顶点出度不超过其非邻点数（Thomassé 非邻点命题的定向图形式）；最小入、出度均不低于 @@M@@n/3@@ 的定向图必含有向三角形；@@M@@r@@-正则且最短有向圈长（directed girth）为 4 的图至少有 @@M@@3r+1@@ 个顶点，即 Behzad–Chartrand–Wall 最小阶猜想的围长 4 情形。
全文反证，三步走。先做约化（第 2 节）：设存在反例，取顶点数最少、弧数其次最少者 @@M@@D@@，可证 @@M@@D@@ 强连通且每点入度为正。核心是把 Seacrest 引理 4 的删弧思想加强为子集亏损：对非空真子集 @@M@@S@@，记 @@M@@I=F(S)\cap S@@、@@M@@E=F(S)\setminus S@@，每轮删去从 @@M@@S@@ 指向 @@M@@E\setminus T@@ 的全部弧，极小性迫使删弧后的图中某顶点满足邻域不等式；比较删弧前后的邻域变化并累加增量估计，得 @@M@@|F^2(S)\setminus F(S)|<|F(S)\setminus S|@@。再做字典积膨胀：把每个顶点换成 @@M@@m>n@@ 个顶点的传递竞赛图（transitive tournament），块内像集的初等估计使每单位亏损放大 @@M@@m@@ 倍、块内误差至多按基顶点各计 1，于是对所有非空真子集 @@M@@U@@ 一致得到严格不等式 @@M@@|U|+|F^2(U)|<2|F(U)|@@，且每点入度为正。
其次是剪枝引理（第 3 节），它对任意有限二元关系成立，与定向性无关。两族有序点对 @@M@@\mathcal R,\mathcal C@@ 中，@@M@@(p,j)@@ 与 @@M@@(i,s)@@ 冲突指 @@M@@p\to i@@ 且 @@M@@s\to j@@，冲突生成点集 @@M@@Z@@ 与 @@M@@H@@。引理断言：可删去部分成员使剩余两族无冲突、原先无冲突者全部保留，且删除总数不超过 @@M@@|H|@@ 加上删完后仍无成员覆盖的 @@M@@Z@@ 中点数——代价须对”事后未覆盖点”记账，这正是末步所要。证明先建增广二部图（左部 @@M@@\mathcal R\sqcup Z_L@@、右部 @@M@@\mathcal C\sqcup Z_R@@），把问题化为匹配（matching）大小不超过 @@M@@|Z|+|H|@@；再利用 Edmonds 关于泛型秩（generic rank）等于最大匹配数的经典对应，选取一组系数使四个线性映射同时满足交换关系 @@M@@NL=AB@@ 与三个秩条件，并配合”最大支撑秩矩阵的左、右核（kernel）向量在允许位置逐坐标正交”的代数引理完成匹配界，最后以 König 定理的交替路构造把匹配界化为删除集。
最后是极值矛盾（第 4 节）：设 @@M@@G@@ 满足上述严格不等式，在 @@M@@X\times X@@ 上定义坐标像算子 @@M@@F_1,F_2@@，称 @@M@@P,Q@@ 相容若 @@M@@F_1P\cap F_2Q=\varnothing@@。对角线 @@M@@\Delta@@ 自身相容，故可在含 @@M@@\Delta@@ 的相容对中取 @@M@@M+d@@ 最大者（@@M@@M@@ 为两族大小之和，@@M@@d@@ 为未覆盖点数）。@@M@@P@@ 的每一列、@@M@@Q@@ 的每一行都是非空真子集，逐列逐行求和严格不等式得纤维和不等式；取补集构造新族，其总大小严格大于 @@M@@M+2d@@。新族未必相容，但对角线成员仍无冲突且被剪枝引理保留，且冲突集 @@M@@H@@ 完全落入旧未覆盖点集，即 @@M@@|H|\le d@@。于是剪枝至多删除 @@M@@d+d'@@ 个成员（@@M@@d'@@ 为新族未覆盖点数），新目标值严格大于 @@M@@M+2d-(d+d')+d'=M+d@@，与极大性矛盾，定理得证。
主结果已由 Lean 形式化证明验证，这是最强的可信度背书；加权与有向圈推论由主定理经 Seacrest 等价性与初等论证导出。本文为结果族 173 的唯一论文，独立完成猜想的完整解决；方法上建立在 Brantner–Brockman–Kay–Snively 的极小反例与图乘积技术、以及 Seacrest 的子集视角之上。按 OpenAI 官方声明，未经形式化的结果可能存在问题，相关推论仍宜以社区核验为准。
问 1：证明最关键、也最脆弱的一步在哪？
（答：剪枝引理。它对任意有限二元关系成立：可删去两族有序对的部分成员使剩余无冲突、原先无冲突者全保留，代价不超过冲突点数 @@M@@|H|@@ 加上删完后仍无成员覆盖的点数。全文最险处恰是这个计费结构：末步中冲突集完全落入旧未覆盖点集（@@M@@|H|\le d@@），删除至多 @@M@@d+d'@@，目标值严格大于 @@M@@M+2d-(d+d')+d'=M+d@@——若代价不按”事后未覆盖点”记账，这串不等式拼不拢。）
问 2：为什么必须”恰为两步”、排除一步已到者？
（答：若 @@M@@N_2@@ 允许包含一步顶点，@@M@@|N_1|\le|\text{至多两步可达}|@@ 平凡成立，猜想失去内容；引言明言”removing vertices already reached in one step is essential”。也因这一排除，等式 @@M@@N_2^+(v)=F^2(\{v\})\setminus F(\{v\})@@ 依赖定向图中没有从顶点出发长为二又回到自身的有向走径。）
问 3：与三十年来的部分结果相比，新意何在？
（答：此前全是带条件结果：竞赛图情形（Fisher 用 Farkas 引理、Havet–Thomassé 用局部中位序）、缺匹配/星/团的近竞赛图、最小出度 @@M@@\le6@@（Kaneko–Locke）及计算机辅助的 7、@@M@@0.657@@ 与 @@M@@0.716@@ 的比例下界。本文无条件覆盖一切定向图。技术上承接 Brantner–Brockman–Kay–Snively 的极小反例与图乘积、Seacrest 的子集视角，新部件是剪枝引理。）
问 4：”定向”（无反向弧对）这个假设为什么撤不掉？
（答：定向性保证像集分解与删弧归约成立；若允许 2-循环，@@M@@F^2(\{v\})\setminus F(\{v\})@@ 不再等于第二邻域，子集不等式与膨胀步骤全部失效。对带反向弧对的一般有向图，相应命题论文未讨论。）
问 5：剪枝引理的证明为什么绕道线性代数？
（答：先建增广二部图，把删除问题化为匹配大小的界；再用 Edmonds”泛型秩等于最大匹配数”的经典对应，选一组系数使四个线性映射满足交换关系 @@M@@NL=AB@@ 与秩条件，靠最大支撑秩矩阵左、右核向量在允许位置的逐坐标正交控制匹配，最后以 König 交替路把匹配界化为删除集。绕道是为了把冲突结构变成可用秩估计的对象。）
问 6：最可能出错的模式？机器核验覆盖到哪？
（答：主定理已 Lean 形式化，主链风险压到最低——这在 AI 生成证明中是最强的可信度信号。未形式化的是加权与有向圈推论，但它们经 Seacrest 等价性与初等论证从主定理导出，风险较低。）
问 7：谁会用到它？
（答：有向图理论社区直接受益：最小入、出度均 @@M@@\ge n/3@@ 的定向图必含有向三角形（与 Caccetta–Häggkvist 型问题同味）；无有向三角形的图必有顶点出度不超过其非邻点数；@@M@@r@@-正则、有向围长 4 的图至少 @@M@@3r+1@@ 个顶点，即 Behzad–Chartrand–Wall 最小阶猜想的围长 4 情形。）
总评
三十年猜想的无条件解决且主定理经 Lean 核验，剪枝引理是真正的新工具；可信度极高，残余风险仅在未形式化的推论细节。