Maximizing Algebraic Connectivity with $2(n-2)$ Edges: The Large Vertex Number Case

Abstract

Kolokolnikov conjectured that, among finite simple graphs on $n$ vertices with exactly $2(n-2)$ edges, the complete bipartite graph $K_{2,n-2}$ maximizes algebraic connectivity. We prove the conjectured statement for every $n\ge 123$: every such graph has algebraic connectivity at most $2$, while $K_{2,n-2}$ attains $2$. The proof begins with explicit Rayleigh-quotient certificates that exclude several local configurations from a hypothetical counterexample. A global degree count then controls the number and total excess of vertices of degree at least $5$ and bounds the edge excess of the subgraph induced by vertices of degree at most $4$. A Moore-type breadth-first-search criterion uses this excess to guarantee a short cycle, while a spectral criterion excludes cycles in the same length range. An explicit arithmetic estimate shows that the two criteria apply simultaneously once $n\ge 123$. A Lean formalization covering every $n\ge 4$, including the complementary range $4\le n\le 122$, has been produced with MerLean and checked by the Lean kernel; the present paper gives a self-contained mathematical account of the large-order component.

Preliminary version. The manuscript gives a self-contained proof for the large-order case $n\ge 123$. A Lean formalization covers all $n\ge 4$; the human-readable treatment of the remaining finite range $4\le n\le 122$ is still undergoing verification, organization, and polishing and will be included in a future revision