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 claims that, except at orders 7 and 8, K_2 \vee P_{n-2} uniquely maximizes adjacency spectral radius among n-vertex planar graphs — resolving a conjecture dating to 1991 and identifying the exact spectral extremizer at every order.
Reproduction
~ partially reproduced
Attempted: With no declared hypotheses or project axioms, the Lean development proves the required Perron–Frobenius/Rayleigh theory, strict spectral monotonicity, the paper's principal Perron-vector identities, and several exact scalar inequalities. It does not prove the central planar extremal theorem.
All files build without sorry; the axiom audit reports only propext, Classical.choice, Quot.sound. An independent plantri audit confirmed every finite case through n = 14, including the exceptions at 7 and 8 (not kernel-certified). Completion stopped at the one remaining wall: no faithful planarity/outerplanarity theory supporting Euler counts, facial relocation, maximal outerplanar structure, or certified enumeration exists in mathlib or any located tooling project. Topological embeddings, rotation systems, and excluded-minor encodings were each investigated; every route requires a substantial foundational formalization, and assuming only the paper's needed consequences would be circular. Several nonfatal typographical slips are documented in the run's README. Notably, the Perron–Frobenius layer — a named blocker in all three previous runs — was built from scratch this run. Independent re-verification: all five modules elaborate cleanly, kernel-checked.
trace (319 events) · code (9 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.