AI 中文总结
本文证明了$n\ge123$时，$2(n-2)$条边的$n$顶点有限简单图中，完全二部图$K_{2,n-2}$使代数连通性最大，同时完成了含小$n$范围的Lean形式化。
AI 中文摘要
Kolokolnikov提出猜想：在具有恰好$2(n-2)$条边的$n$顶点有限简单图中，完全二部图$K_{2,n-2}$使代数连通性达到最大。本文证明了该猜想对所有$n\ge123$成立：所有此类图的代数连通性至多为2，而$K_{2,n-2}$的代数连通性恰好为2。证明过程首先使用显式瑞利商证书排除假设反例中的若干局部构型；随后通过全局度数计数控制度数至少为5的顶点的数量和总超出量，并界定度数至多为4的顶点诱导子图的边超出量；再利用摩尔型广度优先搜索准则，通过该超出量保证存在短圈，同时用谱准则排除相同长度范围内的圈；最后通过显式算术估计表明，当$n\ge123$时这两个准则可同时适用。此外，已使用MerLean完成覆盖所有$n\ge4$（包括互补范围$4\le n\le122$）的Lean形式化，并由Lean内核核验，本文则给出了大阶分量的自包含数学阐述。
英文摘要
Kolokolnikov conjectured that, among all simple graphs on \(n\) vertices with exactly \(2(n-2)\) edges, the complete bipartite graph maximizes algebraic connectivity. This paper proves the conjecture. The underlying Lean~4 formalization was generated with MerLean and checked by the Lean kernel.
