2607.19268v1 / README.md
all files
# Boots--Royle/Cao--Vince reproduction report
## Verdict
**Partial.** This directory does not contain a Lean proof of Theorem 1.1.
It contains a zero-`sorry`, project-axiom-free formalization of the spectral
foundation and several exact algebraic parts of the proof, together with an
independent exhaustive numerical audit of the finite cases. The central
planar extremal theorem is therefore **not claimed**.
The paper's central statement is:
> For every `n ≥ 3`, except `n = 7, 8`, the unique `n`-vertex planar graph
> maximizing the largest adjacency eigenvalue is `K₂ ∨ P_(n-2)`; for orders
> 7 and 8 the two graphs displayed in Figure 2 are the maximizers.
The original Boots--Royle/Cao--Vince conjecture is the restriction to
`n ≥ 9`.
## What is kernel-checked
The root module is [`BootsRoyle.lean`](BootsRoyle.lean).
### Spectral layer
[`BootsRoyle/Spectral.lean`](BootsRoyle/Spectral.lean) defines the real
adjacency operator and defines its largest eigenvalue by the maximum Rayleigh
quotient:
```lean
noncomputable def adjacencySpectralRadius (G : SimpleGraph V) : ℝ :=
⨆ x : {x : EuclideanSpace ℝ V // x ≠ 0},
⟪adjacencyOperator G x, x⟫_ℝ / ‖x‖ ^ 2
```
The file proves the sanity results needed to identify this with the quantity
used by the paper:
* the adjacency operator is symmetric;
* the variational maximum is an adjacency eigenvalue;
* a finite connected graph has a strictly positive eigenvector at this
eigenvalue;
* that vector may be normalized so its coordinate sum is one;
* adding an edge cannot decrease the eigenvalue, and strictly increases it
when the smaller graph is connected.
Mathlib has symmetric-operator and Rayleigh-quotient theory but did not expose
the required Perron--Frobenius theorem. The positivity result is therefore
proved here from scratch: maximize on the unit sphere, replace a maximizer by
its coordinatewise absolute value, and propagate a zero coordinate along
walks.
### Perron identities
[`BootsRoyle/Identities.lean`](BootsRoyle/Identities.lean) proves, for the
paper's `ℓ¹`-normalized Perron data:
* the coordinate eigenvector equation;
* `λ = ∑_v d(v)x_v`, equation (3.3);
* `λ = 4 + E - L`, the first identity in (3.2);
* `∑_v max(0,d(v)-4) = 2n-12+k` for a triangulation with minimum degree
three, the second identity in (3.2);
* `r_v = 1-(λ+1)x_v`, the last assertion of Lemma 3.3.
The edge-count hypothesis in the second identity is stated explicitly as
`|E(G)| = 3|V(G)|-6`; it is not disguised as a definition of planarity.
### Scalar layer
[`BootsRoyle/Arithmetic.lean`](BootsRoyle/Arithmetic.lean) defines
* `r_n = (3 + √(8n-19))/2`,
* the paper's `L₀`, `α_k`, `γ_k`, and outerplanar `γ'_k`,
and proves `r_n²-3r_n=2n-7`, the bounds on `r_n` and `L₀` used in the
large-order proof, a generic certificate for the positive-slope branch of the
two-variable optimization, its boundary intersection calculation, and the
selected-face averaging algebra behind Lemma 3.6. These are exact real-number
proofs, not floating-point checks.
### Axiom and build audit
Run:
```text
cd repro
lake build BootsRoyle
lake env lean BootsRoyle/Audit.lean
rg -n '\bsorry\b|\badmit\b' --glob '*.lean' BootsRoyle BootsRoyle.lean
```
[`BootsRoyle/Audit.lean`](BootsRoyle/Audit.lean) asks Lean to print the axioms
of representative results. The output is only:
```text
[propext, Classical.choice, Quot.sound]
```
These are mathlib's ordinary foundations. There is no declared project
axiom and no `sorry`.
## Independent finite audit
The paper delegates every order through 14 to Sage code, but that code is not
present in the supplied text, PDF, JSON, or PDF attachments. I independently
used plantri 5.8 to generate all unlabelled 3-connected plane triangulations
and checked their adjacency radii. This is a correctness audit only: neither
plantri's completeness nor floating-point power iteration is imported into
Lean's kernel.
The reusable readers are:
* [`tools/check_finite.py`](tools/check_finite.py), a transparent graph6
reader and pure-Python power iteration;
* [`tools/check_finite.c`](tools/check_finite.c), the same calculation in C
for the 339,722 graphs of order 14.
The tooling downloads, made under the run's tooling-only network exception,
were:
```text
https://users.cecs.anu.edu.au/~bdm/plantri/plantri58.tar.gz
https://ziglang.org/download/0.14.1/zig-x86_64-linux-0.14.1.tar.xz
```
Zig was needed only because the container had no C system headers. A typical
reproduction is:
```text
plantri -g 14 /tmp/tri14.g6
zig cc -O3 -o /tmp/check_finite tools/check_finite.c -lm
/tmp/check_finite 14 /tmp/tri14.g6
```
The audit results were:
| `n` | triangulations | maximizer relative to `K₂ ∨ P_(n-2)` | gap to relevant competitor |
|---:|---:|:---|---:|
| 4 | 1 | target | -- |
| 5 | 1 | target | -- |
| 6 | 2 | target | `0.119026675526` |
| 7 | 5 | exception `F~f]G` | exception is higher by `0.006740310639` |
| 8 | 14 | exception `G~f]Ig` | exception is higher by `0.015564349215` |
| 9 | 50 | target | `0.023187972834` |
| 10 | 233 | target | `0.044243494012` |
| 11 | 1,249 | target | `0.052702728770` |
| 12 | 7,595 | target | `0.058812716937` |
| 13 | 49,566 | target | `0.062982378920` |
| 14 | 339,722 | target | `0.065886819752` |
For order 3, every simple graph is a subgraph of `K₃`, so strict spectral
monotonicity gives the stated maximizer directly. The graph6 exception at
order 7 has degree sequence `(6,5,5,5,3,3,3)`; the one at order 8 has degree
sequence `(6,6,6,6,3,3,3,3)`, agreeing with Figure 2.
## Exact obstruction
The first non-algebraic step needed for the theorem is not available in the
local mathlib checkout: mathlib has no definition or theory of planar or
outerplanar simple graphs. In particular, it has no kernel-checked route to
the following facts used by the paper:
1. an extremal planar graph can be completed to a plane triangulation and
hence has `3n-6` edges;
2. facial triangles, support faces, and the operation of relocating a cubic
vertex inside a face (Lemmas 3.2--3.6);
3. the `K₃,₃` obstruction used in Lemmas 3.8--3.9;
4. deletion of a universal vertex produces a maximal outerplanar graph with
an outer Hamilton cycle (Section 5);
5. the planar edge bound on the subgraph `K₂ ∨ C_ℓ` in the final step.
General tooling searches, deliberately excluding the paper, its authors, and
any discussion or formalization of it, did not locate a Lean 4 development
providing this bridge. Three replacement designs were examined:
* **Topological embedding:** define vertices and noncrossing Jordan arcs in
the sphere. This immediately requires a formal Jordan-curve/face theory
and a proof of Euler's formula.
* **Rotation systems:** define a cellular combinatorial map and genus-zero
face permutation. This makes Euler counting tractable, but showing that it
is equivalent to ordinary graph planarity is the Heffter--Edmonds
representation theorem, itself a substantial missing formalization.
* **Excluded minors:** define planarity by absence of `K₅` and `K₃,₃`
minors. Mathlib also lacks graph-minor theory, and relating this definition
to the paper requires a formal Wagner/Kuratowski theorem.
Defining “planar” to mean only the five consequences above was rejected:
that would satisfy the proof while failing the required semantic obligation.
Taking all of those consequences as hypotheses was also rejected as
non-minimal and as merely packaging the paper's difficult graph-theoretic
content into assumptions.
Even after a planarity foundation, substantial work remains. The Liu--Weng
degree-sequence spectral bound used to obtain two cubic vertices, the
face-incidence arguments of Lemmas 3.2--3.9, and both complete optimization
lemmas must still be formalized. The analytic estimates genuinely start at
`n = 15`; exploratory linear optimization with the paper's constraints does
not close all orders 9--14, so the missing finite proof cannot be eliminated
by simply extending that interval.
## Paper audit
The exhaustive audit found no counterexample to Theorem 1.1, and numerical
checks of the displayed one-variable polynomial signs agreed with the paper
on `r_n ≥ r_15`.
I found three presentational slips, none of which supplied a counterexample:
* Lemma 2.2 writes `λ(H) > ρ(Q)` where interlacing directly gives
`λ(H) ≥ ρ(Q)`; its preceding strict inequality `ρ(Q) > r_n` is sufficient
for the intended conclusion.
* In the exactly-one-cubic-vertex branch of Lemma 3.1, the displayed
degree-sum equality has a missing degree term. The radicand subsequently
displayed is larger, so it still yields a valid (looser) upper bound.
* The sentence after Lemma 5.2 rewrites the coefficient from Lemma 3.9 with
denominator `2k` instead of `3k`; Lemma 5.3 replaces that estimate and the
typo is not used in the final bound.
There is also an omitted `-L` in one intermediate displayed upper bound in
the prose of Proposition 5.1. The identity immediately before it is
`λ-4=E-L`, and the next line uses `L>L₀`, so the intended chain retains the
term and is clear.
## Why this is partial
The checked files establish honest prerequisites, not the theorem. A
complete result would need both a faithful formal planarity foundation and
the remaining structural/optimization proof, plus a kernel-certified finite
enumeration (or a new uniform argument). No deep theorem is declared as a
hypothesis in this development: the available “single hypotheses” would have
bundled several provable lemmas or essentially restated the missing result,
contrary to the run's minimal-hypothesis condition.