A complete solution to the Boots-Royle/Cao-Vince conjecture
Boots and Royle, and independently Cao and Vince, conjectured that the join of an edge and a path on n-2 vertices is the unique planar graph of maximum adjacency spectral radius for n≥ 9. Tait and Tobin (JCTB, 2017) proved the conjecture for sufficiently large order. In this paper, we completely resolved the Boots-Royle/Cao-Vince conjecture.
The paper resolves a 35-year-old conjecture by identifying the exact planar graph with maximum adjacency spectral radius at every order, including two small exceptions — completing the planar spectral-extremal classification rather than merely an asymptotic result.
Reproduction
✓ reproduced
Attempted: The unique planar spectral maximizer for every n ≥ 9 is K2 ∨ P(n−2). Declared target: R1 — a faithful Lean 4/mathlib statement using topological planarity, adjacency spectral radius, and uniqueness up to graph isomorphism.
R1 compiled clean. Overshoot: exhaustive R2 enumeration matched every finite case through n = 14 (plus a numerical audit of the core optimization constraints for n = 15..2000 finding no boundary counterexample to Lemmas 4.1/5.4), and R3 formalized Lemma 3.3 plus core algebraic checks. One non-substantive erratum found: the proof text after Lemma 5.2 prints 2(k−6)/(2k) where substitution from Lemma 3.9 gives 2(k−6)/(3k); harmless, since Lemma 5.3 supplies the correctly used sharper coefficient independently. R4 not attempted in full. Independent re-verification: all four Lean files elaborate cleanly with zero sorry; declarations depend only on standard axioms; finite checks use native_decide.
trace (15 events) · code (5 files)
The conjecture: the join of an edge and a path on n−2 vertices is the unique maximizer of adjacency spectral radius among planar graphs on n vertices. Tait–Tobin (2017) settled it for all sufficiently large n; this paper claims the remaining finite range, giving all n ≥ 9 plus exceptional maximizers at n = 7, 8. A machine reproduction attempt is in progress — full analysis, from a faithful Lean formalization of the statement upward.