Trace — 2607.19268v1

DECLARATION: Central claim: for every n >= 3 other than 7 and 8, the unique n-vertex planar simple graph maximizing adjacency spectral radius is the join K2 ∨ P_(n-2), with specific exceptional maximizers at n = 7 and n = 8; in particular this completely proves the Boots–Royle/Cao–Vince conjecture for all n >= 9. Declared target: R1 (statement) — faithfully formalize in Lean 4/mathlib the central n >= 9 uniqueness theorem using mathlib's actual simple-graph planarity, join, path, adjacency-matrix, and spectral-radius notions. I will then attempt to climb into R2/R3 without lowering this declaration.

API inspection: mathlib provides SimpleGraph.pathGraph, completeGraph, graph isomorphisms, real adjacency matrices, and ordered Hermitian-matrix eigenvalues. It has no graph-planarity predicate, no graph-minor API, and no graph-join constructor in this checkout.

R1 approach: define planarity faithfully by a crossing-free topological drawing in R^2 (injective vertex placement and injective continuous edge arcs meeting only at common endpoints), define the graph join directly on a sum type, and define adjacency spectral radius as the largest ordered real eigenvalue of the Hermitian adjacency matrix. State uniqueness up to SimpleGraph.Iso, not literal labeled equality.

R1 compiled: `lake env lean Repro.lean` exited 0. `#print axioms CentralClaim` reports only mathlib/core foundations `[propext, Classical.choice, Quot.sound]`; there is no `sorryAx`. Declared target R1 is achieved.

Continued climbing to R2. The PDF skill was used because text extraction loses Figure 2. Rendered and visually inspected PDF page 2 at high resolution; reconstructed the n=7 and n=8 exceptional maximal planar graphs from their edge drawings. Checked local executables: SageMath, plantri, and nauty `geng` are unavailable.

R2 Lean structural checks: `FiniteChecks.lean` defines labeled H_n and both Figure 2 graphs. `native_decide` verifies edge counts 15/18 and degree sequences [5,5,3,6,3,3,5] and [6,6,3,6,3,3,6,3]. Initial attempt to `#eval` mathlib characteristic polynomials died because `Matrix.charpoly` is noncomputable; removed that dead end and used an independent numerical eigensolver for root checks.

Independent NumPy checks: rho(H_7)=4.504664353588047 while rho(exception_7)=4.511404664226755; rho(H_8)=4.838537617034654 while rho(exception_8)=4.8541019662496865. Integer characteristic-polynomial coefficient checks were [1,0,-15,-26,3,28,11,-2] vs [1,0,-15,-26,3,24,2,-6] at n=7 and [1,0,-18,-32,15,60,21,-16,-7] vs [1,0,-18,-32,15,48,-10,-24,9] at n=8.

Because no graph generator was installed and the paper's Sage code was absent, implemented an independent spherical-triangulation generator in `repro/triangulation_search.cpp`: recursive topological vertex splitting from K4, rotation-system canonical labeling over every directed root edge and both orientations, and Perron power iteration. This was a distinct replacement approach, not paper code.

Exhaustive R2 enumeration succeeded. Unlabeled triangulation counts for n=4..14 were exactly 1,1,2,5,14,50,233,1249,7595,49566,339722. Winners: H_n for n=4,5,6,9,10,11,12,13,14; Figure 2(a) for n=7; Figure 2(b) for n=8. Winner spectral radii for n=3..14 were approximately 2,3,3.645751311065,4.119026675526,4.511404664227,4.854101966250,5.137793510080,5.411801176471,5.666284480139,5.905046089761,6.130771829068,6.345446852691. The printed winner edge sets at n>=9 have exactly two universal vertices and a path after their deletion, confirming isomorphism to H_n.

R2 achieved for every finite order explicitly delegated by the paper to Sage (n<=14). Restriction to triangulations is valid because a spectral maximizer is connected and adding any missing planar edge strictly raises the Perron root; every planar graph extends to a triangulation.

Numerical audit of core optimization constraints found no boundary counterexample to Lemma 4.1 or Lemma 5.4 for every integer n=15..2000 and every admissible k. The proof text after Lemma 5.2 prints 2(k-6)/(2k), whereas direct substitution from Lemma 3.9 gives 2(k-6)/(3k); this is a non-substantive denominator typo because Lemma 5.3 supplies the correctly used sharper coefficient independently.

R3 approach 1: formalize omitted/core algebra. `CoreAlgebra.lean` proves the polynomial sign assertions used in Lemma 4.1 by positive expansions about t=13/2, defines the exact F_t(theta) from Lemma 5.4, and proves the omitted n=15, k=5,6,7 substitutions. Early denominator-clearing proof attempts had direction/noncomputability elaboration errors; rewriting with `eq_div_iff`, explicit positive denominators, and the identity t^2-3t=23 resolved them.

R3 approach 2: formalize the paper's Lemma 3.3. `CoreLemma.lean` proves all three identities faithfully for finite simple graphs: lambda=4+E-L from the normalized adjacency eigenvector equation, sum c_v=2n-12+k from the triangulation edge count, and r_v=1-(lambda+1)x_v. Initial attempts hit adjacency-symmetry dependent-rewrite and Nat/Int cast issues; explicit case splits, Matrix.mulVec, and an integer degree-sum argument resolved them.

Final Lean audit: `lake env lean Repro.lean`, `FiniteChecks.lean`, `CoreAlgebra.lean`, and `CoreLemma.lean` all exit 0. Grep finds no `sorry` or `admit`. `#print axioms` for CentralClaim, omitted_n15_checks, and all three Lemma 3.3 theorems reports only core/mathlib foundations propext, Classical.choice, and Quot.sound; no sorryAx or added axioms.

STOP: declared R1 was fully achieved, R2 was fully overshot for all paper-stated finite cases, and R3 was overshot via a complete proof of Lemma 3.3 plus core algebraic sublemmas/omitted checks. R4 is genuinely beyond this run: it would require formalizing plane triangulations/outerplanarity, Perron-Frobenius extremality, relocation arguments, Lemmas 3.4-3.9 and 4.1/5.4 in full, and Propositions 4.1/5.1 before the central theorem. No evidence that the paper's theorem is wrong was found.