Trace — 2607.19268v1
**Planning project formalization and inspection**
I’ll first reconstruct the exact central theorem and proof dependency graph from the local paper, then map those dependencies against mathlib before committing to definitions. I’ll keep the final response to the exact JSON object requested; all proof artifacts and the audit trail will go in `repro/README.md`.
$ /bin/bash -lc "pwd && rg --files -g 'AGENTS.md' -g 'paper.txt' -g 'paper.pdf' -g 'paper.json' -g 'README*' -g 'lean-toolchain' -g 'lakefile.*' | sed -n '1,160p'" /work paper.json paper.txt paper.pdf repro/scripts/SideSkimmer/lakefile.lean repro/scripts/README.md repro/DownstreamTest/lakefile.toml repro/DownstreamTest/README.md repro/Cache/README.md repro/lean-toolchain repro/scripts/bench/size/README.md repro/scripts/bench/lint/README.md repro/lakefile.lean repro/README.md repro/scripts/bench/build/README.md repro/scripts/bench/open-mathlib/README.md repro/scripts/bench/README.md repro/Mathlib/Probability/Combinatorics/README.md repro/Mathlib/Algebra/Notation/README.md repro/widget/src/penrose/README.md repro/Archive/Wiedijk100Theorems/README.md repro/Archive/Imo/README.md repro/Archive/README.md repro/Mathlib/Algebra/README.md repro/Mathlib/Analysis/Convex/Cone/README.md repro/Mathlib/Analysis/Convex/README.md repro/Mathlib/Order/README.md repro/Mathlib/Geometry/Group/Growth/README.md repro/Mathlib/Geometry/Group/README.md repro/Mathlib/Geometry/Convex/Cone/README.md repro/Mathlib/Geometry/Convex/README.md
**Inspecting title abstract theorem**
$ /bin/bash -lc "sed -n '1,260p' paper.txt && rg -n \""'^(Theorem|Lemma|Corollary|Proposition|Conjecture|Definition|Main theorem)|Boots|Royle|Cao|Vince" paper.txt | sed -n '"'1,240p'" A complete solution to the Boots-Royle/Cao-Vince conjecture Lele Liu∗ Bo Ning† Yi Wang‡ Abstract arXiv:2607.19268v1 [math.CO] 21 Jul 2026 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. Keywords: Spectral radius; Planar graph; Perron vector; Spectral extremal graph theory. AMS Classification: 05C35; 05C50; 15A18 1. Introduction Let G be a simple graph, and let λ(G) denote the spectral radius of its adjacency matrix. A classical problem at the intersection of spectral graph theory and topological graph theory is to determine how large λ(G) can be when G is planar, and, more ambitiously, to characterize all graphs attaining the maximum. The study of this problem goes back at least to Schwenk and √ Wilson [13]. In 1988, Hong [9] proved that every planar graph of order n satisfies λ(G) ≤ 5n − 11 by using the famous Hong’s spectral inequality and Euler formula. Cao and Vince [3] subsequently √ improved this estimate to λ(G) < 4 + 3n − 9. Further improvements were obtained by √ Hong [10, 11], and Ellingham and Zha [6] later established the bound λ(G) ≤ 2 + 2n − 6. These results progressively narrowed the gap between the known upper bounds and the natural planar constructions K2 ∨ Pn−2 , where ∨ denotes the graph join. They also shifted attention from merely estimating the spectral radius to the more delicate problem of determining the exact extremal graph. There are two famous conjectures in the related area. The first concerns outerplanar graphs. In their 1990 survey [4], Cvetković and Rowlinson conjectured that K1 ∨ Pn−1 attains the maximum spectral radius among all outerplanar graphs of order n. Following partial results of Rowlinson, Cao and Vince [3], Tait and Tobin
**Planning inspection of theorem proof sections**
$ /bin/bash -lc "sed -n '200,1385p' paper.txt"
gives
q · det(rn I − Qn ) = qrn (rn − 1)(rn − 2) − 4qrn − 2q 2 rn + 2(rn − 1)2 − 8
= 4q − 4 − rn (q − 2).
Consequently, det(rn I − Qn ) < 0.
The two negative eigenvalues of Qn contribute positive factors to det(rn I − Qn ). Hence
det(rn I − Qn ) < 0 forces the unique positive eigenvalue of Qn to be larger than rn . Combining
this with λ(Hn ) > ρ(Qn ) proves λ(Hn ) > rn .
3. Cubic vertices in an extremal triangulation
Throughout the remainder of the paper, let G be a planar graph of order n ≥ 15 having
maximum spectral radius, and put λ := λ(G). Let x = (xv )v∈V (G) be a nonnegative Perron
vector, normalized by ∥x∥1 = 1. Since Hn is planar, extremality and Lemma 2.2 imply λ > rn .
Two consequences of G being planar that we will use frequently are that G has at most
3n − 6 edges and G does not contain K3,3 as a subgraph. Since every planar graph on the same
vertex set is contained in a maximal planar graph, it follows that G is itself connected and
edge-maximal. We therefore take a plane triangulation of G, which gives e(G) = 3n − 6.
Cubic vertices are essential to the extremal structure; accordingly, we establish some results
concerning such vertices.
Lemma 3.1. The graph G has at least two cubic vertices.
Proof. We first show that G has at least one cubic vertex. If not, the minimum degree is δ ≥ 4.
Since a planar graph has a vertex of degree at most five, δ ∈ {4, 5}. Applying Theorem 2.1 with
P
j = n, and using i di = 6n − 12, gives
p
δ − 1 + (δ + 1)2 + 4(6n − 12 − nδ)
λ≤
.
2
4
√
For δ = 4, the right-hand side of the above inequality becomes (3 + 8n − 23)/2, which is strictly
√
less than rn . For δ = 5, it becomes 2 + n − 3, which is no great than rn . In both cases, the
resulting bound contradicts λ > rn . Thus a cubic vertex must exist.
It remains to exclude exactly one cubic vertex. In this case let d = dn−1 . Clearly, d ≥ 4;
P
moreover d ≤ 5, since otherwise v d(v) ≥ 3 + 6(n − 1) > 6n − 12. Applying Theorem 2.1 with
j = n − 1 gives
2
2λ ≤ d − 1 + d + 1) **Identifying typo in Lemma 5.2 denominator**
$ /bin/bash -lc "sed -n '1,240p' README.md 2>/dev/null; sed -n '1,240p' repro/README.md; sed -n '1,220p' repro/lakefile.lean; cat repro/lean-toolchain; git -C repro status --short" # mathlib4  [](https://mathlib-bors-ca18eefec4cb.herokuapp.com/repositories/16) [](https://leanprover.zulipchat.com) [](https://gitpod.io/#https://github.com/leanprover-community/mathlib4) [Mathlib](https://leanprover-community.github.io) is a user maintained library for the [Lean theorem prover](https://leanprover.github.io). It contains both programming infrastructure and mathematics, as well as tactics that use the former and allow to develop the latter. ## Installation You can find detailed instructions to install Lean, mathlib, and supporting tools on [our website](https://leanprover-community.github.io/get_started.html). Alternatively, click on one of the buttons below to open a GitHub Codespace or a Gitpod workspace containing the project. [](https://codespaces.new/leanprover-community/mathlib4) [](https://gitpod.io/#https://github.com/leanprover-community/mathlib4) ## Using `mathlib4` as a dependency Please refer to [https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency](https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency) ## Experimenting Got everything installed? Why not start with the [tutorial project](https://leanprover-community.github.io/install/project.html)? For more pointers, see [Learning Lean](https://leanprover-community.github.io/learn.html). ## Documentation Besides the installation guides above and [Lean's general documentation](https://docs.lea
**Assessing planar graph definitions in mathlib**
The paper’s main theorem is stronger than the original \(n\ge 9\) conjecture: it classifies every order \(n\ge3\), with two exceptional extremizers at \(n=7,8\). The infinite proof starts only at \(n\ge15\); the paper delegates \(n\le14\) entirely to Sage, so a faithful formalization must independently certify that finite range as well as formalize substantial planar-graph and spectral machinery. I’m now auditing what mathlib already exposes and checking the paper’s algebraic steps before choosing the proof boundary.
$ /bin/bash -lc "rg -n \"def .*Planar|PlanarGraph|IsPlanar|planar graph|Euler.*planar|three.*n.*six|3 \\*.*- 6|IsOuterplanar|Outerplanar|maximal outerplanar\" Mathlib | sed -n '1,260p'; rg -n \"spectralRadius|spectral radius|IsPerron|Perron|Rayleigh|largest eigenvalue|eigenvalues.*Hermitian|IsHermitian.*eigen\" Mathlib | sed -n '1,300p'; rg -n \"def join|SimpleGraph\\.join|PathGraph|pathGraph|IsPath|cycleGraph|completeBipartiteGraph\" Mathlib/Combinatorics/SimpleGraph | sed -n '1,260p'" Mathlib/Probability/Kernel/Deterministic.lean:46:* [Moss and Perrone, *A category-theoretic proof of the ergodic decomposition theorem*][moss2023] Mathlib/CategoryTheory/MarkovCategory/Positive.lean:42:* [Moss and Perrone, *A category-theoretic proof of the ergodic decomposition theorem*][moss2023] Mathlib/NumberTheory/Rayleigh.lean:12:# Rayleigh's theorem on Beatty sequences Mathlib/NumberTheory/Rayleigh.lean:14:This file proves Rayleigh's theorem on Beatty sequences. We start by proving `compl_beattySeq`, Mathlib/NumberTheory/Rayleigh.lean:15:which is a generalization of Rayleigh's theorem, and eventually prove Mathlib/NumberTheory/Rayleigh.lean:16:`Irrational.beattySeq_symmDiff_beattySeq_pos`, which is Rayleigh's theorem. Mathlib/NumberTheory/Rayleigh.lean:118:/-- Generalization of Rayleigh's theorem on Beatty sequences. Let `r` be a real number greater Mathlib/NumberTheory/Rayleigh.lean:137:/-- Generalization of Rayleigh's theorem on Beatty sequences. Let `r` be a real number greater Mathlib/NumberTheory/Rayleigh.lean:175:/-- **Rayleigh's theorem** on Beatty sequences. Let `r` be an irrational number greater than 1, and Mathlib/Analysis/Normed/Algebra/GelfandFormula.lean:25:* `spectrum.pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius`: Gelfand's formula for the Mathlib/Analysis/Normed/Algebra/GelfandFormula.lean:26: spectral radius in Banach algebras over `ℂ`. Mathlib/Analysis/Normed/Algebra/GelfandFormula.lean:83:differentiable on any closed ball centered at zero of radius `r < (spectralRadius 𝕜 a)⁻¹`. -/ Mathlib/Analysis/Normed/Algebra/GelfandFormula.lean:86: (hr : (r : ℝ≥0∞) < (spectralRadius 𝕜 a)⁻¹) : Mathlib/Analysis/Normed/Algebra/GelfandFormula.lean:102:/-- The `limsup` relationship for the spectral radius used to prove `spectrum.gelfand_formula`. -/ Mathlib/Analysis/Normed/Algebra/GelfandFormula.lean:103:theorem limsup_pow_nnnorm_pow_one_div_le_spectralRadius (a : A) : Mathlib/Analysis/Normed/Algebra/GelfandFormula.lean:104: limsup (fun n : ℕ =>
**Planning targeted search for planarity**
$ /bin/bash -lc "rg -n -i \"planar|outerplanar|kuratowski|embedding.*sphere|sphere.*embedding\" Mathlib/Combinatorics Mathlib/Topology | sed -n '1,300p'; rg -n \"def join|theorem.*join|namespace.*join|join_adj\" Mathlib/Combinatorics/SimpleGraph | sed -n '1,240p'; rg -n \"adjMatrix|adjacencyMatrix|IsHermitian.*adj|eigenvalues.*adj|spectral\" Mathlib/Combinatorics/SimpleGraph Mathlib/Analysis/Matrix | sed -n '1,300p'" Mathlib/Combinatorics/SimpleGraph/Coloring/Vertex.lean:53: * Planar graphs Mathlib/Topology/MetricSpace/GromovHausdorff.lean:13:public import Mathlib.Topology.MetricSpace.Kuratowski Mathlib/Topology/MetricSpace/GromovHausdorff.lean:31:embedding called the Kuratowski embedding. Mathlib/Topology/MetricSpace/GromovHausdorff.lean:51:open BoundedContinuousFunction Nat Int kuratowskiEmbedding Mathlib/Topology/MetricSpace/GromovHausdorff.lean:65:Using the Kuratowski embedding, we get a canonical map `toGHSpace` mapping any nonempty Mathlib/Topology/MetricSpace/GromovHausdorff.lean:91: ⟦NonemptyCompacts.kuratowskiEmbedding X⟧ Mathlib/Topology/MetricSpace/GromovHausdorff.lean:106: have f := (kuratowskiEmbedding.isometry X).isometryEquivOnRange.trans e Mathlib/Topology/MetricSpace/GromovHausdorff.lean:111: ((kuratowskiEmbedding.isometry X).isometryEquivOnRange.symm.trans Mathlib/Topology/MetricSpace/GromovHausdorff.lean:113: have E : (range Ψ ≃ᵢ NonemptyCompacts.kuratowskiEmbedding X) Mathlib/Topology/MetricSpace/GromovHausdorff.lean:114: = (p ≃ᵢ range (kuratowskiEmbedding X)) := by Mathlib/Topology/MetricSpace/GromovHausdorff.lean:115: dsimp only [NonemptyCompacts.kuratowskiEmbedding]; rw [rangeΨ]; rfl Mathlib/Topology/MetricSpace/GromovHausdorff.lean:150: (NonemptyCompacts.kuratowskiEmbedding X ≃ᵢ NonemptyCompacts.kuratowskiEmbedding Y) = Mathlib/Topology/MetricSpace/GromovHausdorff.lean:151: (range (kuratowskiEmbedding X) ≃ᵢ range (kuratowskiEmbedding Y)) := by Mathlib/Topology/MetricSpace/GromovHausdorff.lean:152: dsimp only [NonemptyCompacts.kuratowskiEmbedding]; rfl Mathlib/Topology/MetricSpace/GromovHausdorff.lean:153: have f := (kuratowskiEmbedding.isometry X).isometryEquivOnRange Mathlib/Topology/MetricSpace/GromovHausdorff.lean:154: have g := (kuratowskiEmbedding.isometry Y).isometryEquivOnRange.symm Mathlib/Topology/MetricSpace/GromovHausdorff.lean:158: have f := (kuratowskiEmbedding.isometry X).isometryEquivOnRang
**Planning combinatorial planarity definition** **Considering named hypothesis for planar facts**
$ /bin/bash -lc "python3 - <<'PY'
import json
p=json.load(open('/work/paper.json'))
print(type(p))
if isinstance(p,dict): print(p.keys())
print(str(p)[:5000])
PY
pdfinfo paper.pdf | sed -n '1,80p'; find . -maxdepth 2 -type f -not -path './repro/*' -printf '%p %s bytes\\n'"
Title: A complete solution to the Boots-Royle/Cao-Vince conjecture
Author: Lele Liu; Bo Ning; Yi Wang
Creator: arXiv GenPDF (tex2pdf:8def8d8)
Producer: pikepdf 8.15.1
Custom Metadata: yes
Metadata Stream: yes
Tagged: no
UserProperties: no
Suspects: no
Form: none
JavaScript: no
Pages: 19
Encrypted: no
Page size: 612 x 792 pts (letter)
Page rot: 0
File size: 388634 bytes
Optimized: no
PDF version: 1.7
./.git/description 73 bytes
./.git/HEAD 23 bytes
./.git/config 147 bytes
./codex.err 15006 bytes
./paper.pdf 388634 bytes
./PROMPT.txt 3634 bytes
./paper.txt 44299 bytes
./paper.json 805 bytes
./codex-events.jsonl 154312 bytes**Inspecting PDF figures and attachments**
$ /bin/bash -lc 'pdfdetach -list paper.pdf; mkdir -p /tmp/boots_royle_pages && pdftoppm -f 2 -l 2 -png -r 160 paper.pdf /tmp/boots_royle_pages/page >/dev/null 2>&1 && ls -lh /tmp/boots_royle_pages' total 316K -rw-r--r-- 1 root root 315K Jul 23 13:49 page-02.png
**Mapping universal vertex connections** **Verifying planar edge count contradictions** **Identifying lemma interlacing typo**
**Assessing maximal planar graph lemmas** **Analyzing face weight inequalities in lemmas** **Confirming occupied face average inequality**
**Verifying common neighbor bounds in lemmas** **Analyzing cubic support face contributions**
**Verifying polynomial positivity with CAS** **Calculating polynomial roots for validation**
$ /bin/bash -lc "python3 - <<'PY'
import sympy as s
t=s.symbols('t', real=True)
polys={
'A':17*t**3-127*t**2+321*t-390,
'B':5*t**3-46*t**2+120*t-174,
'C':5*t**4-26*t**3-43*t**2+96*t-480,
'D':47*t**6-516*t**5+988*t**4+5652*t**3-25720*t**2+39744*t-26244,
'E':3*t**3-29*t**2+117*t-222,
'F':t**3-8*t**2+16*t-29,
'G':28*t**3+4*t**2-180*t+264,
'H':75*t**3-573*t**2+905*t-1318}
for k,p in polys.items():
print(k, 'at6.5=',s.N(p.subs(t,s.Rational(13,2))), 'roots=',[r for r in s.nroots(p,maxsteps=200) if abs(s.im(r))<1e-8])
PY"
Traceback (most recent call last):
File "<stdin>", line 1, in <module>
ModuleNotFoundError: No module named 'sympy'**Verifying Python scientific libraries availability**
$ /bin/bash -lc "command -v sage || true; python3 - <<'PY'
import numpy as np
ps={
'A':[17,-127,321,-390],
'B':[5,-46,120,-174],
'C':[5,-26,-43,96,-480],
'D':[47,-516,988,5652,-25720,39744,-26244],
'E':[3,-29,117,-222],
'F':[1,-8,16,-29],
'G':[28,4,-180,264],
'H':[75,-573,905,-1318]}
for k,c in ps.items():
print(k, np.polyval(c,6.5), np.roots(c))
PY"
Traceback (most recent call last):
File "<stdin>", line 1, in <module>
ModuleNotFoundError: No module named 'numpy'**Deciding efficient numeric computation methods**
$ /bin/bash -lc "python3 - <<'PY'
ps={
'A':[17,-127,321,-390],
'B':[5,-46,120,-174],
'C':[5,-26,-43,96,-480],
'D':[47,-516,988,5652,-25720,39744,-26244],
'E':[3,-29,117,-222],
'F':[1,-8,16,-29],
'G':[28,4,-180,264],
'H':[75,-573,905,-1318]}
for x in [6.5,6.6,6.7,7,8,10,20,100]:
print('t',x, {k:round(__import__('functools').reduce(lambda a,b:a*x+b,c),3) for k,c in ps.items()})
PY"
t 6.5 {'A': 999.375, 'B': 35.625, 'C': 112.312, 'D': 18832.484, 'E': 137.125, 'F': 11.625, 'G': 6952.5, 'H': 952.125}
t 6.6 {'A': 1083.912, 'B': 51.72, 'C': 292.992, 'D': 38034.067, 'E': 149.448, 'F': 15.616, 'G': 7300.128, 'H': 1257.32}
t 6.7 {'A': 1172.641, 'B': 68.875, 'C': 488.652, 'D': 61211.641, 'E': 162.379, 'F': 19.843, 'G': 7658.924, 'H': 1580.755}
t 7 {'A': 1465, 'B': 127, 'C': 1172, 'D': 159599, 'E': 205, 'F': 34, 'G': 8804, 'H': 2665}
t 8 {'A': 2754, 'B': 402, 'C': 4704, 'D': 998780, 'E': 394, 'F': 99, 'G': 13416, 'H': 7650}
t 10 {'A': 7120, 'B': 1426, 'C': 20180, 'D': 8731196, 'E': 1048, 'F': 331, 'G': 26864, 'H': 25432}
t 20 {'A': 91230, 'B': 23826, 'C': 576240, 'D': 1550576636, 'E': 14518, 'F': 5091, 'G': 222264, 'H': 387582}
t 100 {'A': 15761710, 'B': 4551826, 'C': 473579120, 'D': 41944198748156, 'E': 2721478, 'F': 921571, 'G': 28022264, 'H': 69359182}**Verifying lemma inequality conditions** **Analyzing propositions and lemmas in graph section**
**Analyzing neighbor constraints in outerplanar graphs** **Verifying coefficient positivity conditions**
**Verifying proof constraints for n≥15** **Planning planar graph enumeration with plantri**
$ /bin/bash -lc "command -v plantri || true; command -v nauty-geng || command -v geng || true; command -v sage || true; command -v gap || true; command -v ghc || true; command -v cargo || true; command -v cmake || true; command -v cc || true; find /usr /opt -iname '*plantri*' -o -iname 'geng' 2>/dev/null | sed -n '1,100p'"
**Planning web search for Lean planar graph**
**Assessing formal proof frameworks for planar maps** **Planning formalization amid theorem limitations** **Verifying Lemma 3.1 degree sequence bound**
**Identifying discrepancy in degree sum formula** **Confirming looser upper bound validity**
**Verifying positive determinant of Q** **Analyzing edge addition effects on spectral radius**
**Verifying face support properties** **Confirming cubic vertex intersection limits** **Analyzing cubic vertex adjacency constraints**
**Verifying polynomial optimization lemmas** **Verifying polynomial identities and discriminants**
**Verifying derivative endpoint numerically**
$ /bin/bash -lc "python3 - <<'PY'
from math import sqrt
for n in [15]:
t=(3+sqrt(8*n-19))/2
for k in [5,6,7]:
th=k/(2*n-4)
F=(((2*n-4)*th-1)/(t-2))*((t+2)/(t+1)-2*th/3+8/(3*(2*n-4))) +(n-6-(((2*n-4)*th-1)*t)/(t-2))*((1-5*th/11)/(t+1)) +(n-5)/(t+1)-th-(t-4))
print(n,t,k,F)
PY"
File "<stdin>", line 6
F=(((2*n-4)*th-1)/(t-2))*((t+2)/(t+1)-2*th/3+8/(3*(2*n-4))) +(n-6-(((2*n-4)*th-1)*t)/(t-2))*((1-5*th/11)/(t+1)) +(n-5)/(t+1)-th-(t-4))
^
SyntaxError: unmatched ')'$ /bin/bash -lc "python3 - <<'PY' from math import sqrt n=15;t=(3+sqrt(8*n-19))/2 for k in [5,6,7]: th=k/(2*n-4) a=((2*n-4)*th-1)/(t-2) F=a*((t+2)/(t+1)-2*th/3+8/(3*(2*n-4))) F+=(n-6-a*t)*((1-5*th/11)/(t+1)) F+=(n-5)/(t+1)-th-(t-4) print(n,t,k,F) PY" 15 6.524937810560445 5 -0.01756903356473427 15 6.524937810560445 6 -0.01870077593279995 15 6.524937810560445 7 -0.024465415341659025
**Validating K33 subgraph planarity contradiction**
The hand proof is internally coherent so far; several displayed equalities contain harmless typographical slips, but the corresponding inequalities remain valid. The main library gap is more serious: this mathlib checkout has adjacency matrices and finite-dimensional spectral theory, but no definition or theory of planar/outerplanar graphs. I’m checking whether a reusable Lean planar-map development is available as permitted tooling; if not, I’ll need to make the planarity interface and its faithfulness theorem part of the development rather than silently weakening “planar.”
**Planning equivalence proof for planar characterization** **Outlining combinatorial map implementation for planarity** **Connecting planarity bounds with spectral radius**
**Confirming Perron-Frobenius relevance**
$ /bin/bash -lc "rg -n -i \"perron.?frobenius|irreducible.*matrix|matrix.*irreducible|positive eigenvector|nonnegative matrix.*eigen|eigenvector.*nonneg|spectral radius.*nonnegative\" Mathlib | sed -n '1,300p'; sed -n '300,390p' Mathlib/Analysis/InnerProductSpace/Rayleigh.lean; sed -n '40,120p' Mathlib/Analysis/Matrix/Spectrum.lean"
Mathlib/LinearAlgebra/RootSystem/CartanMatrix.lean:230:lemma induction_on_cartanMatrix [P.IsReduced] [P.IsIrreducible]
Mathlib/LinearAlgebra/Matrix/Irreducible/Defs.lean:26:* `Matrix.IsIrreducible A`: A matrix `A` is defined as irreducible if it is entrywise nonnegative
Mathlib/LinearAlgebra/Matrix/Irreducible/Defs.lean:28: `Matrix.isIrreducible_iff_exists_pow_pos` proves this graph-theoretic definition is equivalent
Mathlib/LinearAlgebra/Matrix/Irreducible/Defs.lean:39:* `Matrix.isIrreducible_iff_exists_pow_pos`: Shows the equivalence between the graph-theoretic
Mathlib/LinearAlgebra/Matrix/Irreducible/Defs.lean:42:* `Matrix.IsPrimitive.to_IsIrreducible`: Proves that a primitive matrix is also irreducible
Mathlib/LinearAlgebra/Matrix/Irreducible/Defs.lean:44:* `Matrix.IsIrreducible.transpose`: Shows that the irreducibility property is preserved under
Mathlib/LinearAlgebra/Matrix/Irreducible/Defs.lean:64:matrix, nonnegative, positive, power, quiver, graph, irreducible, primitive, perron-frobenius
Mathlib/LinearAlgebra/Matrix/Irreducible/Defs.lean:80:/-- A matrix `A` is irreducible if it is entrywise nonnegative and
Mathlib/LinearAlgebra/Matrix/Irreducible/Defs.lean:82:@[mk_iff] structure IsIrreducible (A : Matrix n n R) : Prop where
Mathlib/LinearAlgebra/Matrix/Irreducible/Defs.lean:181:/-- If a nonnegative square matrix `A` is primitive, then `A` is irreducible. -/
Mathlib/GroupTheory/Coxeter/Matrix.lean:23:Coxeter group (`CoxeterMatrix.coxeterGroup`) is finite and irreducible, although we do not prove
have hx₀'' : x₀ ∈ sphere (0 : E) ‖x₀‖ := by simp
rw [T.iInf_rayleigh_eq_iInf_rayleigh_sphere hx₀']
refine IsMinOn.iInf_eq hx₀'' ?_
intro x hx
dsimp
have : ‖x‖ = ‖x₀‖ := by simpa using hx
simp only [ContinuousLinearMap.rayleighQuotient]
rw [this]
gcongr
exact hextr hx
end CompleteSpace
end IsSelfAdjoint
section FiniteDimensional
variable [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E}
namespace LinearMap
namespace IsSymmetric
/-- The supremum of th**Focusing on PF definitions without theorems**
$ /bin/bash -lc "find Mathlib/LinearAlgebra/Matrix/Irreducible -type f -maxdepth 2 -print; rg -n \"theorem|lemma\" Mathlib/LinearAlgebra/Matrix/Irreducible | tail -120; rg -n \"eigenvalues₀.*0|eigenvalues_antitone|iSup.*eigenvalues|rayleigh.*eigenvalues\" Mathlib/Analysis/Matrix Mathlib/LinearAlgebra | sed -n '1,260p'" Mathlib/LinearAlgebra/Matrix/Irreducible/Defs.lean Mathlib/LinearAlgebra/Matrix/Irreducible/Defs.lean:27: and its associated quiver `toQuiver A` is strongly connected. The theorem Mathlib/LinearAlgebra/Matrix/Irreducible/Defs.lean:95:lemma IsIrreducible.exists_pos [Nontrivial n] Mathlib/LinearAlgebra/Matrix/Irreducible/Defs.lean:115:theorem pow_apply_pos_iff_nonempty_path Mathlib/LinearAlgebra/Matrix/Irreducible/Defs.lean:159:theorem isIrreducible_iff_exists_pow_pos Mathlib/LinearAlgebra/Matrix/Irreducible/Defs.lean:182:theorem IsPrimitive.isIrreducible Mathlib/LinearAlgebra/Matrix/Irreducible/Defs.lean:206:theorem IsIrreducible.transpose (hA : IsIrreducible A) : IsIrreducible Aᵀ := by Mathlib/LinearAlgebra/Matrix/Irreducible/Defs.lean:223:theorem isIrreducible_transpose_iff : Mathlib/Analysis/Matrix/Spectrum.lean:62: LinearMap.IsSymmetric.eigenvalues_antitone ..
**Reconstructing Rayleigh proof for spectral bound** **Exploring spectral bounds using degree sequences** **Deciding to apply theorem for n≥15 only**
**Planning numeric verification for inequalities**
$ /bin/bash -lc "python3 - <<'PY' from math import sqrt,floor def alpha(k): return 0 if k<=2 else (2*k-5)/(2*k+1) def gamma(k): return max(0,2*(k-6)/(3*k)) def gammap(k): return max(0,2*(k-4)/(3*k)) def l0(n,k,t): return k/(2*n-k-4+3*k/t) # maximize a*s+b*z over polygon s>=0,z>=0,z<=s/2,(t+1)s<=A,t*s+(t-2)z<=B # enumerate intersections of lines from itertools import combinations def lp(a,b,lines): # lines p*s+q*z<=r, includes lower pts=[] for l1,l2 in combinations(lines,2): p,q,r=l1;u,v,w=l2; det=p*v-q*u if abs(det)<1e-9: continue s=(r*v-q*w)/det;z=(p*w-r*u)/det if all(p*s+q*z<=r+1e-8 for p,q,r in lines): pts.append((s,z)) return max((a*s+b*z,s,z) for s,z in pts) for n in range(6,16): t=(3+sqrt(8*n-19))/2 bad4=[] for k in range(2,floor((2*n-4)/3)+1): L=l0(n,k,t); A=2-alpha(k)*L; B=2-gamma(k)*L val,s,z=lp(n-6,k,[(-1,0,0),(0,-1,0),(-.5,1,0),(t+1,0,A),(t,t-2,B)]) if val-L >= t-4-1e-9: bad4.append((k,val-L-(t-4),s,z,L)) bad5=[] for k in range(2,floor((n-1)/2)+1): L=l0(n,k,t); A=1-alpha(k)*L;B=(t+2)/(t+1)-gammap(k)*L val,y,z=lp(n-6,k-1,[(-1,0,0),(0,-1,0),(-1,1,0),(t+1,0,A),(t,t-2,B)]) # z<=y since x2>=x3 expr=(n-5)/(t+1)+val-L if expr >= t-4-1e-9: bad5.append((k,expr-(t-4),y,z,L)) print(n,'t',round(t,4),'bad4',bad4,'bad5',bad5) PY" 6 t 4.1926 bad4 [] bad5 [] 7 t 4.5414 bad4 [] bad5 [] 8 t 4.8541 bad4 [(4, 0.03758354228952454, 0.3184128799473286, 0.1592064399736643, 0.38196601125010515)] bad5 [] 9 t 5.1401 bad4 [(4, 0.02594883928895131, 0.29805893217418683, 0.14902946608709342, 0.3242908769417241)] bad5 [(4, 0.02975875486830959, 0.14044076801407165, 0.14044076801407165, 0.3242908769417241)] 10 t 5.4051 bad4 [(4, 0.0018963774136944167, 0.2813854813392361, 0.14069274066961804, 0.2812916726683953), (5, 0.060908179786290706, 0.2813854813392361, 0.14069274066961804, 0.3629726109654167)] bad5 [(4, 0.012783374145088011, 0.13122499639896282, 0.13122499639896282, 0.2812916726683953)] 11 t 5.6533 bad4 [(5, 0.032623048379773145, 0.26738082669468755, 0.13369041334734377, 0.31942122037134624), (6, 0.09058122132201185, 0.26738082669468755, 0.13369041334734377, 0.39515346077645114)] bad5 [(5, 0.00028934653730505744, 0.11902399892212476, 0.11902399892212476, 0.31942122037134624)] 12 t 5.8875 bad4 [(6, 0.05925443447073975, 0.2553879420619924, 0.1276939710309962, 0.35175485039113025)] bad5 [] 13 t 6.1098 bad4 [(6, 0.02312189044433488, 0.24495819861490442, 0.12247909930745221, 0.3166878670582655), (7, 0.03611844013466037, 0.24052948373955665, 0.12026474186977833, 0.3796689104842412)] bad5 [] 14 t 6.3218 bad4 [(7, 0.0006318904126958458, 0.23190561014779212, 0.11595280507389606, 0.3444572457904362), (8, 0.008056064253252782, 0.22783299153398423, 0.11391649576699212, 0.40411445365808013)] bad5 [] 15 t 6.5249 bad4 [] bad5 []
**Planning enumeration of maximal planar triangulations** **Evaluating formal enumeration feasibility in Lean** **Designing planar certificate in abstract graph theory**
**Designing PlaneTriangulation abstraction** **Planning combinatorial planarity framework** **Incorporating Tait-Tobin hypothesis**
**Assessing spectral radius examples**
$ /bin/bash -lc "sed -n '1,260p' /work/codex.err; tail -120 /work/codex.err; git log -1 --oneline --decorate"
Reading additional input from stdin...
2026-07-23T13:48:14.741175Z INFO shell_snapshot{thread_id=019f8f3b-e3dd-7582-82f8-e1c86f1a7d96}: codex_core::shell_snapshot: Shell snapshot successfully created: /root/.codex/shell_snapshots/019f8f3b-e3dd-7582-82f8-e1c86f1a7d96.tmp-1784814494691293248
2026-07-23T13:48:14.747017Z INFO codex.exec{otel.kind="internal" thread.id="019f8f3b-e3dd-7582-82f8-e1c86f1a7d96"}: codex_exec: Codex initialized with event: SessionConfiguredEvent { session_id: SessionId { uuid: 019f8f3b-e3dd-7582-82f8-e1c86f1a7d96 }, thread_id: ThreadId { uuid: 019f8f3b-e3dd-7582-82f8-e1c86f1a7d96 }, forked_from_id: None, parent_thread_id: None, thread_source: Some(User), thread_name: None, model: "gpt-5.6-sol", model_provider_id: "openai", service_tier: None, approval_policy: Never, approvals_reviewer: User, permission_profile: Managed { file_system: Restricted { entries: [FileSystemSandboxEntry { path: Special { value: Root }, access: Read }, FileSystemSandboxEntry { path: Path { path: AbsolutePathBuf("/work") }, access: Write }, FileSystemSandboxEntry { path: Special { value: SlashTmp }, access: Write }, FileSystemSandboxEntry { path: Special { value: Tmpdir }, access: Write }, FileSystemSandboxEntry { path: Path { path: AbsolutePathBuf("/work/.git") }, access: Read }, FileSystemSandboxEntry { path: Path { path: AbsolutePathBuf("/work/.agents") }, access: Read }, FileSystemSandboxEntry { path: Path { path: AbsolutePathBuf("/work/.codex") }, access: Read }], glob_scan_max_depth: None }, network: Enabled }, active_permission_profile: None, cwd: AbsolutePathBuf("/work"), reasoning_effort: Some(XHigh), initial_messages: None, network_proxy: None, rollout_path: Some("/root/.codex/sessions/2026/07/23/rollout-2026-07-23T13-48-14-019f8f3b-e3dd-7582-82f8-e1c86f1a7d96.jsonl") }
2026-07-23T13:48:14.805868Z INFO codex.exec{otel.kind="internal" thread.id="019f8f3b-e3dd-7582-82f8-e1c86f1a7d96"}: codex_exec: Sent prompt with event ID: 019f8f3b-e423-74d0-b56a-2d2a3337ae56**Planning central theorem implementation** **Outlining BootsRoyle theorem formalization** **Checking plantri package availability**
$ /bin/bash -lc 'command -v git; command -v curl; command -v wget; command -v clang; command -v gcc; command -v g++; command -v make; command -v python3; ls /usr/bin/cc /usr/bin/gcc /usr/bin/clang 2>/dev/null || true' /usr/bin/git /usr/bin/curl /usr/bin/python3
**Evaluating compilation and tooling options** **Investigating exceptional graphs code availability**
$ /bin/bash -lc 'rg -n -i "code|sage|github|http|ancillary|repository" paper.txt paper.json' paper.json:16: "arxiv_url": "https://arxiv.org/abs/2607.19268v1", paper.json:17: "pdf_url": "https://arxiv.org/pdf/2607.19268v1", paper.txt:1314:Proof of Theorem 1.1. For n ≤ 14, we use SageMath software to find the extremal planar graphs paper.txt:1315:(see the code). In the following we assume n ≥ 15. Let v1 , v2 be the two universal vertices paper.txt:1330:The authors used ChatGPT to generate code for searching the extremal planar graphs for
**Assessing theorem proof verifiability** **Planning Lean spectral radius definitions** **Verifying Rayleigh iSup behavior on empty subtypes**
**Defining spectral radius for nonempty spaces** **Defining adjacency spectral radius with eigenvector approach**
**Inspecting eigenvector theorem**
$ /bin/bash -lc "sed -n '240,360p' Mathlib/Analysis/InnerProductSpace/Rayleigh.lean; rg -n \"eigenvalues.*(zero|0)|eigenvalues.*le|le_eigenvalues|eigenvalues_le|eigenvalues_antitone|rayleigh.*le|le.*rayleigh\" Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean Mathlib/Analysis/InnerProductSpace Mathlib/Analysis/Matrix | sed -n '1,300p'; rg -n \"reApplyInnerSelf.*adjMatrix|inner.*mulVec|dotProduct.*inner|abs.*dotProduct\" Mathlib | sed -n '1,220p'"
by_cases hb : b = 0
· have : a ≠ 0 := by simpa [hb] using! h₁
refine absurd ?_ hx₀
apply smul_right_injective F this
simpa [hb] using! h₂
have hc : T x₀ = (-b⁻¹ * a) • x₀ := by
linear_combination (norm := match_scalars <;> field) b⁻¹ • h₂
set c : ℝ := -b⁻¹ * a
convert hc
simpa [field, inner_smul_left, mul_comm a] using! congr_arg (fun x => ⟪x, x₀⟫_ℝ) hc
end Real
section CompleteSpace
variable [CompleteSpace E] {T : E →L[𝕜] E}
theorem eq_smul_self_of_isLocalExtrOn (hT : IsSelfAdjoint T) {x₀ : E}
(hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere (0 : E) ‖x₀‖) x₀) :
T x₀ = (T.rayleighQuotient x₀ : 𝕜) • x₀ := by
let := InnerProductSpace.rclikeToReal 𝕜 E
let hSA := hT.isSymmetric.restrictScalars.toSelfAdjoint.prop
exact hSA.eq_smul_self_of_isLocalExtrOn_real hextr
/-- For a self-adjoint operator `T`, a local extremum of the Rayleigh quotient of `T` on a sphere
centred at the origin is an eigenvector of `T`. -/
theorem hasEigenvector_of_isLocalExtrOn (hT : IsSelfAdjoint T) {x₀ : E} (hx₀ : x₀ ≠ 0)
(hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere (0 : E) ‖x₀‖) x₀) :
HasEigenvector (T : E →ₗ[𝕜] E) (T.rayleighQuotient x₀) x₀ := by
refine ⟨?_, hx₀⟩
rw [Module.End.mem_eigenspace_iff]
exact hT.eq_smul_self_of_isLocalExtrOn hextr
/-- For a self-adjoint operator `T`, a maximum of the Rayleigh quotient of `T` on a sphere centred
at the origin is an eigenvector of `T`, with eigenvalue the global supremum of the Rayleigh
quotient. -/
theorem hasEigenvector_of_isMaxOn (hT : IsSelfAdjoint T) {x₀ : E} (hx₀ : x₀ ≠ 0)
(hextr : IsMaxOn T.reApplyInnerSelf (sphere (0 : E) ‖x₀‖) x₀) :
HasEigenvector (T : E →ₗ[𝕜] E) (⨆ x : { x : E // x ≠ 0 }, T.rayleighQuotient x : ℝ) x₀ := by
convert! hT.hasEigenvector_of_isLocalExtrOn hx₀ (Or.inr hextr.localize)
have hx₀' : 0 < ‖x₀‖ := by simp [hx₀]
have hx₀'' : x₀ ∈ sphere (0 : E) ‖x₀‖ := by simp
rw [T.iSup_rayleigh_eq_iSup_rayleigh_sphere hx₀']
refine IsMaxOn.iSup_eq hx₀'' ?_
**Prototyping adjacency operator definitions**
$ /bin/bash -lc "sed -n '1,80p' Mathlib/Analysis/Matrix/Spectrum.lean; rg -n \"def toLpLin|theorem toLpLin_apply|isSelfAdjoint_toLpLin|isSymmetric_toEuclideanLin_iff|isSelfAdjoint.*toLp\" Mathlib/Analysis/Matrix Mathlib | sed -n '1,180p'"
/-
Copyright (c) 2022 Alexander Bentkamp. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Alexander Bentkamp
-/
module
public import Mathlib.Algebra.Star.UnitaryStarAlgAut
public import Mathlib.Analysis.InnerProductSpace.Spectrum
public import Mathlib.Analysis.Matrix.Hermitian
public import Mathlib.LinearAlgebra.Eigenspace.Matrix
public import Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs
public import Mathlib.LinearAlgebra.Matrix.Rank
/-! # Spectral theory of Hermitian matrices
This file proves the spectral theorem for matrices. The proof of the spectral theorem is based on
the spectral theorem for linear maps (`LinearMap.IsSymmetric.eigenvectorBasis_apply_self_apply`).
## Tags
spectral theorem, diagonalization theorem -/
@[expose] public section
open WithLp
namespace Matrix
variable {𝕜 : Type*} [RCLike 𝕜] {n : Type*} [Fintype n]
variable {A B : Matrix n n 𝕜}
lemma finite_real_spectrum [DecidableEq n] : (spectrum ℝ A).Finite := by
rw [← spectrum.preimage_algebraMap 𝕜]
exact A.finite_spectrum.preimage (FaithfulSMul.algebraMap_injective ℝ 𝕜).injOn
instance [DecidableEq n] : Finite (spectrum ℝ A) := A.finite_real_spectrum
/-- The spectrum of a matrix `A` coincides with the spectrum of `toLpLin p p A`. -/
theorem spectrum_toLpLin [DecidableEq n] (p : ENNReal) :
spectrum 𝕜 (toLpLin p p A) = spectrum 𝕜 A :=
AlgEquiv.spectrum_eq (Matrix.toLinAlgEquiv (PiLp.basisFun p 𝕜 n)) _
/-- The spectrum of a matrix `A` coincides with the spectrum of `toEuclideanLin A`. -/
@[deprecated spectrum_toLpLin (since := "2026-01-21")]
theorem spectrum_toEuclideanLin [DecidableEq n] : spectrum 𝕜 (toEuclideanLin A) = spectrum 𝕜 A :=
spectrum_toLpLin 2
namespace IsHermitian
section DecidableEq
variable [DecidableEq n]
variable (hA : A.IsHermitian) (hB : B.IsHermitian)
/-- The eigenvalues of a Hermitian matrix, indexed by `Fin (Fintype.card n)` where `n` is the index
type of the matrix. -/
noncomputable def eigenvalues₀ :**Analyzing Rayleigh quotient and eigenvector sign adjustment** **Planning to prove eigenvector existence via continuity**
**Compiling with absolute path patch**
$ /bin/bash -lc 'lake env lean BootsRoyle/Spectral.lean' BootsRoyle/Spectral.lean:25:3: error(lean.synthInstanceFailed): failed to synthesize instance of type class DecidableRel G.Adj Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command. BootsRoyle/Spectral.lean:39:51: error(lean.synthInstanceFailed): failed to synthesize instance of type class DecidableRel G.Adj Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command. BootsRoyle/Spectral.lean:42:28: error(lean.synthInstanceFailed): failed to synthesize instance of type class DecidableRel G.Adj Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
**Expanding Perron witness with HasEigenvalue**
$ /bin/bash -lc "rg -n \"def HasEigenvalue|abbrev HasEigenvalue|structure HasEigenvector|def HasEigenvector|theorem hasEigenvalue_iff\" Mathlib/LinearAlgebra Mathlib | sed -n '1,160p'; rg -n \"toContinuousLinearMap|continuousLinearMap.*ofFinite|LinearMap.*continuous\" Mathlib/Analysis/Normed/Module/FiniteDimension.lean Mathlib/Analysis/InnerProductSpace | sed -n '1,200p'"
Mathlib/LinearAlgebra/Eigenspace/Minpoly.lean:95:theorem hasEigenvalue_iff_isRoot : f.HasEigenvalue μ ↔ (minpoly R f).IsRoot μ :=
Mathlib/LinearAlgebra/Eigenspace/Basic.lean:425:abbrev HasEigenvalue (f : End R M) (a : R) : Prop :=
Mathlib/LinearAlgebra/Eigenspace/Basic.lean:507:theorem hasEigenvalue_iff_mem_spectrum [FiniteDimensional K V] {f : End K V} {μ : K} :
Mathlib/LinearAlgebra/Eigenspace/Minpoly.lean:95:theorem hasEigenvalue_iff_isRoot : f.HasEigenvalue μ ↔ (minpoly R f).IsRoot μ :=
Mathlib/LinearAlgebra/Eigenspace/Basic.lean:425:abbrev HasEigenvalue (f : End R M) (a : R) : Prop :=
Mathlib/LinearAlgebra/Eigenspace/Basic.lean:507:theorem hasEigenvalue_iff_mem_spectrum [FiniteDimensional K V] {f : End K V} {μ : K} :
Mathlib/Analysis/Normed/Operator/Compact/FredholmAlternative.lean:221:theorem hasEigenvalue_iff_mem_spectrum (hT : IsCompactOperator T) (hμ : μ ≠ 0) :
Mathlib/Analysis/Normed/Module/FiniteDimension.lean:51:`LinearMap.continuous_of_finiteDimensional`. This gives the desired norm equivalence.
Mathlib/Analysis/Normed/Module/FiniteDimension.lean:175: let fL : E →L[𝕜] F := f.linear.toContinuousLinearMap
Mathlib/Analysis/Normed/Module/FiniteDimension.lean:182:theorem ContinuousLinearMap.continuous_det : Continuous fun f : E →L[𝕜] E => f.det := by
Mathlib/Analysis/Normed/Module/FiniteDimension.lean:193: (ContinuousLinearMap.coeLM 𝕜)).continuous_of_finiteDimensional
Mathlib/Analysis/Normed/Module/FiniteDimension.lean:204: max (‖A.symm.toContinuousLinearMap‖₊ * ‖A.toContinuousLinearMap‖₊) 1
Mathlib/Analysis/Normed/Module/FiniteDimension.lean:222: have LA : LipschitzWith ‖A.toContinuousLinearMap‖₊ A := by apply A.lipschitz
Mathlib/Analysis/Normed/Module/FiniteDimension.lean:223: have L : LipschitzOnWith (‖A.toContinuousLinearMap‖₊ * K) (A ∘ f) s :=
Mathlib/Analysis/Normed/Module/FiniteDimension.lean:226: ∃ g : α → ι → ℝ, LipschitzWith (‖A.toContinuousLinearMap‖₊ * K) g ∧ EqOn (A ∘ f) g s :=
Mathlib/Analysis/Normed/Module/FiniteDimension.lean:$ /bin/bash -lc "sed -n '400,450p' Mathlib/LinearAlgebra/Eigenspace/Basic.lean; sed -n '740,770p' Mathlib/Analysis/InnerProductSpace/Adjoint.lean; sed -n '35,75p' Mathlib/Analysis/Matrix/Hermitian.lean"
on_goal 2 => apply isNilpotent_restrict_genEigenspace_nat f μ (maxUnifEigenspaceIndex f μ)
rw [genEigenspace_top_eq_maxUnifEigenspaceIndex]
/-- The submodule `eigenspace f μ` for a linear map `f` and a scalar `μ` consists of all vectors `x`
such that `f x = μ • x`. (Def 5.52 of [axler2024]). -/
abbrev eigenspace (f : End R M) (μ : R) : Submodule R M :=
f.genEigenspace μ 1
lemma eigenspace_def {f : End R M} {μ : R} :
f.eigenspace μ = LinearMap.ker (f - μ • 1) := by
rw [eigenspace, genEigenspace_one]
@[simp]
theorem eigenspace_zero (f : End R M) : f.eigenspace 0 = LinearMap.ker f := by
simp only [eigenspace, ← Nat.cast_one (R := ℕ∞), genEigenspace_zero_nat, pow_one]
/-- A nonzero element of an eigenspace is an eigenvector. (Def 5.8 of [axler2024]) -/
abbrev HasEigenvector (f : End R M) (μ : R) (x : M) : Prop :=
HasUnifEigenvector f μ 1 x
lemma hasEigenvector_iff {f : End R M} {μ : R} {x : M} :
f.HasEigenvector μ x ↔ x ∈ f.eigenspace μ ∧ x ≠ 0 := Iff.rfl
/-- A scalar `μ` is an eigenvalue for a linear map `f` if there are nonzero vectors `x`
such that `f x = μ • x`. (Def 5.5 of [axler2024]). -/
abbrev HasEigenvalue (f : End R M) (a : R) : Prop :=
HasUnifEigenvalue f a 1
lemma hasEigenvalue_iff {f : End R M} {μ : R} :
f.HasEigenvalue μ ↔ f.eigenspace μ ≠ ⊥ := Iff.rfl
/-- The eigenvalues of the endomorphism `f`, as a subtype of `R`. -/
abbrev Eigenvalues (f : End R M) : Type _ :=
UnifEigenvalues f 1
@[coe]
abbrev Eigenvalues.val (f : Module.End R M) : Eigenvalues f → R := UnifEigenvalues.val f 1
@[simp]
lemma Eigenvalues.val_mk {f : End R M} {μ : R} (h : f.HasEigenvalue μ) :
Eigenvalues.val f ⟨μ, h⟩ = μ := rfl
@[simp]
lemma Eigenvalues.mk_val {f : End R M} (μ : Eigenvalues f) : ⟨μ.val, μ.property⟩ = μ := rfl
theorem hasEigenvalue_of_hasEigenvector {f : End R M} {μ : R} {x : M} (h : HasEigenvector f μ x) :
HasEigenvalue f μ :=
h.hasUnifEigenvalue
theorem mem_eigenspace_iff {f : End R M} {μ : R} {x : M} : x ∈ eigenspace f μ ↔**Planning eigenvector lemma and Rayleigh bound** **Establishing boundedness of Rayleigh quotient**
$ /bin/bash -lc "sed -n '45,140p' Mathlib/Analysis/InnerProductSpace/Rayleigh.lean"
open scoped NNReal
open Module.End Metric RCLike InnerProductSpace
namespace ContinuousLinearMap
variable (T : E →L[𝕜] E)
/-- The *Rayleigh quotient* of a continuous linear map `T` (over `ℝ` or `ℂ`) at a vector `x` is
the quantity `re ⟪T x, x⟫ / ‖x‖ ^ 2`. -/
noncomputable abbrev rayleighQuotient (x : E) := T.reApplyInnerSelf x / ‖(x : E)‖ ^ 2
theorem rayleigh_smul (x : E) {c : 𝕜} (hc : c ≠ 0) :
rayleighQuotient T (c • x) = rayleighQuotient T x := by
by_cases hx : x = 0
· simp [hx]
simp [field, norm_smul, T.reApplyInnerSelf_smul]
theorem rayleighQuotient_add (S : E →L[𝕜] E) {x : E} :
(T + S).rayleighQuotient x = T.rayleighQuotient x + S.rayleighQuotient x := by
simp [rayleighQuotient, reApplyInnerSelf_apply, inner_add_left, add_div]
@[simp]
theorem rayleighQuotient_zero_apply (x : E) : rayleighQuotient (0 : E →L[𝕜] E) x = 0 := by
simp [reApplyInnerSelf_apply]
@[simp]
theorem rayleighQuotient_apply_zero : rayleighQuotient T 0 = 0 := by
simp [reApplyInnerSelf_apply]
@[simp]
theorem rayleighQuotient_neg_apply (x : E) : rayleighQuotient (-T) x = -rayleighQuotient T x := by
simp [rayleighQuotient, reApplyInnerSelf_apply, neg_div]
@[simp]
theorem rayleighQuotient_apply_neg (x : E) : rayleighQuotient T (-x) = rayleighQuotient T x := by
simp [rayleighQuotient, reApplyInnerSelf_apply]
theorem image_rayleigh_eq_image_rayleigh_sphere {r : ℝ} (hr : 0 < r) :
rayleighQuotient T '' {0}ᶜ = rayleighQuotient T '' sphere 0 r := by
ext a
constructor
· rintro ⟨x, hx : x ≠ 0, hxT⟩
let c : 𝕜 := ‖x‖⁻¹ * r
have : c ≠ 0 := by simp [c, hx, hr.ne']
refine ⟨c • x, ?_, ?_⟩
· simp [field, c, norm_smul, abs_of_pos hr]
· rw [T.rayleigh_smul x this]
exact hxT
· rintro ⟨x, hx, hxT⟩
exact ⟨x, ne_zero_of_mem_sphere hr.ne' ⟨x, hx⟩, hxT⟩
theorem iSup_rayleigh_eq_iSup_rayleigh_sphere {r : ℝ} (hr : 0 < r) :
⨆ x : { x : E // x ≠ 0 }, rayleighQuotient T x =
⨆ x : sphere (0 : E) r, rayleighQuotient T x :=
show ⨆ x : ({0}ᶜ**Defining adjacency operator as continuous linear map** **Planning eigenvector existence proof for adjacency operator**
$ /bin/bash -lc "rg -n \"inner.*EuclideanSpace|EuclideanSpace.*inner|real_inner_pi|inner_pi|inner_eq.*dotProduct|norm.*abs.*Pi|norm_abs\" Mathlib/Analysis/InnerProductSpace Mathlib | sed -n '1,260p'" Mathlib/Analysis/InnerProductSpace/PiL2.lean:42: finite-dimensional inner product space, `E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι`. Mathlib/Analysis/InnerProductSpace/PiL2.lean:215:theorem inner_eq_star_dotProduct (x y : EuclideanSpace 𝕜 ι) : Mathlib/Analysis/InnerProductSpace/PiL2.lean:320:theorem EuclideanSpace.inner_single_left (i : ι) (a : 𝕜) (v : EuclideanSpace 𝕜 ι) : Mathlib/Analysis/InnerProductSpace/PiL2.lean:324:theorem EuclideanSpace.inner_single_right (i : ι) (a : 𝕜) (v : EuclideanSpace 𝕜 ι) : Mathlib/Analysis/InnerProductSpace/PiL2.lean:325: ⟪v, EuclideanSpace.single i (a : 𝕜)⟫ = a * conj (v i) := by simp [PiLp.inner_apply] Mathlib/Analysis/InnerProductSpace/PiL2.lean:353: simp_rw [orthonormal_iff_ite, EuclideanSpace.inner_single_left, map_one, one_mul, Mathlib/Analysis/InnerProductSpace/PiL2.lean:445: rw [← b.repr.inner_map_map (b i) v, b.repr_self i, EuclideanSpace.inner_single_left] Mathlib/Analysis/InnerProductSpace/PiL2.lean:454: EuclideanSpace.inner_single_left, PiLp.single_apply, map_one, one_mul] Mathlib/Analysis/InnerProductSpace/PiL2.lean:815:theorem basisFun_inner (x : EuclideanSpace 𝕜 ι) (i : ι) : ⟪basisFun ι 𝕜 i, x⟫ = x i := by Mathlib/Analysis/InnerProductSpace/PiL2.lean:819:theorem inner_basisFun_real (x : EuclideanSpace ℝ ι) (i : ι) : Mathlib/Analysis/InnerProductSpace/Coalgebra.lean:48: simp [TensorProduct.ext_iff_inner_left, adjoint_inner_right, inner_eq_star_dotProduct] Mathlib/Analysis/InnerProductSpace/Coalgebra.lean:57: adjoint_toSpanSingleton, inner_eq_star_dotProduct] Mathlib/Analysis/InnerProductSpace/Positive.lean:207: EuclideanSpace.inner_eq_star_dotProduct, Matrix.ofLp_toLpLin, Matrix.toLin'_apply, Mathlib/Probability/Moments/CovarianceBilinDual.lean:262: simp only [ENNReal.coe_toReal, Real.norm_eq_abs, Pi.add_apply] Mathlib/Probability/Moments/IntegrableExpMul.lean:69: · simp only [norm_eq_abs, abs_exp, Pi.add_apply] Mathlib/Probability/Distributions/Gaussian/HasGaussianLaw/Independence.lean:253: EuclideanSpace
**Planning quadratic form inequality lemma** **Formulating adjacency inequality lemma**
$ /bin/bash -lc 'lake env lean BootsRoyle/Spectral.lean' BootsRoyle/Spectral.lean:25:3: error(lean.synthInstanceFailed): failed to synthesize instance of type class DecidableRel G.Adj Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command. BootsRoyle/Spectral.lean:39:51: error(lean.synthInstanceFailed): failed to synthesize instance of type class DecidableRel G.Adj Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command. BootsRoyle/Spectral.lean:42:28: error(lean.synthInstanceFailed): failed to synthesize instance of type class DecidableRel G.Adj Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command. BootsRoyle/Spectral.lean:52:27: error(lean.synthInstanceFailed): failed to synthesize instance of type class Lattice (EuclideanSpace ℝ V) Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command. BootsRoyle/Spectral.lean:52:32: error(lean.synthInstanceFailed): failed to synthesize instance of type class Lattice (EuclideanSpace ℝ V) Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command. BootsRoyle/Spectral.lean:54:24: warning: This simp argument is unused: SimpleGraph.adjMatrix_apply Hint: Omit it from the simp argument list. [apply] simp only [adjacencyOperator_apply, EuclideanSpace.inner_eq_star_dotProduct, star_trivial, dotProduct, mulVec] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
**Clarifying DecidableRel usage and classical reasoning** **Defining pointwise absolute vector function**
$ /bin/bash -lc "sed -n '190,230p' Mathlib/Analysis/InnerProductSpace/PiL2.lean; rg -n \"def toLp|toLp_apply|ofLp|equiv.*WithLp|WithLp.*equiv\" Mathlib/Analysis/Normed/Lp | sed -n '1,200p'; sed -n '1,100p' Mathlib/Analysis/Normed/Lp/WithLp.lean 2>/dev/null || true"
have : (0 : ℝ) ≤ ∑ i, x i ^ 2 := Finset.sum_nonneg fun _ _ => sq_nonneg _
simp_rw [mem_ofPred, mem_sphere_zero_iff_norm, norm_eq, norm_eq_abs, sq_abs,
Real.sqrt_eq_iff_eq_sq this hr]
section
instance EuclideanSpace.infinite [Nonempty ι] : Infinite (EuclideanSpace 𝕜 ι) :=
Module.Free.infinite 𝕜 _
variable [Fintype ι]
@[simp]
theorem finrank_euclideanSpace :
Module.finrank 𝕜 (EuclideanSpace 𝕜 ι) = Fintype.card ι := by
convert! (WithLp.linearEquiv 2 𝕜 (ι → 𝕜)).finrank_eq
simp
theorem finrank_euclideanSpace_fin {n : ℕ} :
Module.finrank 𝕜 (EuclideanSpace 𝕜 (Fin n)) = n := by simp
namespace EuclideanSpace
scoped instance (n : ℕ) : Fact (Module.finrank 𝕜 (EuclideanSpace 𝕜 (Fin n)) = n) :=
⟨finrank_euclideanSpace_fin⟩
theorem inner_eq_star_dotProduct (x y : EuclideanSpace 𝕜 ι) :
⟪x, y⟫ = ofLp y ⬝ᵥ star (ofLp x) := rfl
lemma inner_toLp_toLp (x y : ι → 𝕜) :
⟪toLp 2 x, toLp 2 y⟫ = dotProduct y (star x) := rfl
section restrict₂
variable {I J : Finset ι'}
/-- The restriction from `EuclideanSpace 𝕜 J` to `EuclideanSpace 𝕜 I` when `I ⊆ J`. -/
noncomputable
def restrict₂ (hIJ : I ⊆ J) :
EuclideanSpace 𝕜 J →L[𝕜] EuclideanSpace 𝕜 I where
toFun x := toLp 2 (Finset.restrict₂ («π» := fun _ ↦ 𝕜) hIJ x.ofLp)
map_add' x y := by ext; simp
Mathlib/Analysis/Normed/Lp/WithLp.lean:29:* `WithLp.ofLp`: the canonical inclusion from `WithLp p V` to `V`.
Mathlib/Analysis/Normed/Lp/WithLp.lean:54: ofLp : V
Mathlib/Analysis/Normed/Lp/WithLp.lean:60:/-- This prevents `toLp p x` being printed as `{ ofLp := x }` by `delabStructureInstance`. -/
Mathlib/Analysis/Normed/Lp/WithLp.lean:70:/-- `WithLp.ofLp` and `WithLp.toLp` as an equivalence. -/
Mathlib/Analysis/Normed/Lp/WithLp.lean:72:protected def equiv : WithLp p V ≃ V where
Mathlib/Analysis/Normed/Lp/WithLp.lean:73: toFun := ofLp
Mathlib/Analysis/Normed/Lp/WithLp.lean:79:lemma equiv_symm_apply : ⇑(WithLp.equiv p V).symm = toLp p := rfl
Mathlib/Analysis/Normed/Lp/WithLp.lean:83:instance instNontrivial [**Defining vector absolute value function**
$ /bin/bash -lc "rg -n \"theorem norm_eq|lemma norm_eq\" Mathlib/Analysis/InnerProductSpace/PiL2.lean | sed -n '1,80p'; sed -n '130,200p' Mathlib/Analysis/InnerProductSpace/PiL2.lean"
457:lemma norm_eq_one (b : OrthonormalBasis ι 𝕜 E) (i : ι) :
/-- Unexpander for the `!₂[x, y, ...]` notation. -/
@[app_delab WithLp.toLp]
meta def EuclideanSpace.delabVecNotation : Delab :=
whenNotPPOption getPPExplicit <| whenPPOption getPPNotation <| withOverApp 3 do
-- check that the `WithLp.toLp _` is present
let p : Term ← withNaryArg 0 <| delab
-- to be conservative, only allow subscripts which are numerals
guard <| p matches `($_:num)
let `(![$elems,*]) ← withNaryArg 2 delab | failure
`(!$p[$elems,*])
end Notation
theorem EuclideanSpace.nnnorm_eq {𝕜 : Type*} [RCLike 𝕜] {n : Type*} [Fintype n]
(x : EuclideanSpace 𝕜 n) : ‖x‖₊ = NNReal.sqrt (∑ i, ‖x i‖₊ ^ 2) :=
PiLp.nnnorm_eq_of_L2 x
theorem EuclideanSpace.norm_eq {𝕜 : Type*} [RCLike 𝕜] {n : Type*} [Fintype n]
(x : EuclideanSpace 𝕜 n) : ‖x‖ = √(∑ i, ‖x i‖ ^ 2) := by
simpa only [Real.coe_sqrt, NNReal.coe_sum] using! congr_arg ((↑) : ℝ≥0 → ℝ) x.nnnorm_eq
theorem EuclideanSpace.norm_sq_eq {𝕜 : Type*} [RCLike 𝕜] {n : Type*} [Fintype n]
(x : EuclideanSpace 𝕜 n) : ‖x‖ ^ 2 = ∑ i, ‖x i‖ ^ 2 :=
PiLp.norm_sq_eq_of_L2 _ x
theorem EuclideanSpace.real_norm_sq_eq {n : Type*} [Fintype n] (x : EuclideanSpace ℝ n) :
‖x‖ ^ 2 = ∑ i, (x i) ^ 2 := by
simp [EuclideanSpace.norm_sq_eq]
@[wikidata Q847073]
theorem EuclideanSpace.dist_eq {𝕜 : Type*} [RCLike 𝕜] {n : Type*} [Fintype n]
(x y : EuclideanSpace 𝕜 n) : dist x y = √(∑ i, dist (x i) (y i) ^ 2) :=
PiLp.dist_eq_of_L2 x y
theorem EuclideanSpace.dist_sq_eq {𝕜 : Type*} [RCLike 𝕜] {n : Type*} [Fintype n]
(x y : EuclideanSpace 𝕜 n) : dist x y ^ 2 = ∑ i, dist (x i) (y i) ^ 2 :=
PiLp.dist_sq_eq_of_L2 x y
theorem EuclideanSpace.nndist_eq {𝕜 : Type*} [RCLike 𝕜] {n : Type*} [Fintype n]
(x y : EuclideanSpace 𝕜 n) : nndist x y = NNReal.sqrt (∑ i, nndist (x i) (y i) ^ 2) :=
PiLp.nndist_eq_of_L2 x y
theorem EuclideanSpace.edist_eq {𝕜 : Type*} [RCLike 𝕜] {n : Type*} [Fintype n]
(x y : EuclideanSpace 𝕜 n) : edist x y **Refining norm absolute value proof**
$ /bin/bash -lc 'lake env lean BootsRoyle/Spectral.lean' BootsRoyle/Spectral.lean:45:28: error(lean.synthInstanceFailed): failed to synthesize instance of type class DecidableRel G.Adj Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command. BootsRoyle/Spectral.lean:58:8: warning: automatically included section variable(s) unused in theorem `BootsRoyle.vectorAbs_apply`: [Fintype V] [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` BootsRoyle/Spectral.lean:61:8: warning: automatically included section variable(s) unused in theorem `BootsRoyle.norm_vectorAbs`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` BootsRoyle/Spectral.lean:65:6: warning: declaration uses `sorry` BootsRoyle/Spectral.lean:74:2: warning: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` BootsRoyle/Spectral.lean:75:2: warning: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` BootsRoyle/Spectral.lean:76:2: warning: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` BootsRoyle/Spectral.lean:80:2: warning: this tactic is never executed Note: This linter can be disabled with `set_option linter.unreachableTactic false` BootsRoyle/Spectral.lean:73:2: warning: 'apply Finset.sum_le_sum' tactic does nothing Note: This linter can be disabled with `set_option linter.unusedTactic false` BootsRoyle/Spectral.lean:74:2: warning: 'intro j _' tactic does nothing Note: This linter can be di
**Adding decidable relation constraint to lemma**
$ /bin/bash -lc "nl -ba BootsRoyle/Spectral.lean | sed -n '35,95p'"
35 noncomputable def adjacencySpectralRadius (G : SimpleGraph V) : ℝ :=
36 ⨆ x : {x : EuclideanSpace ℝ V // x ≠ 0},
37 ⟪adjacencyOperator G x, x⟫_ℝ / ‖(x : EuclideanSpace ℝ V)‖ ^ 2
38
39 lemma adjacencyOperator_isSymmetric (G : SimpleGraph V) :
40 (adjacencyOperator G).IsSymmetric := by
41 classical
42 exact Matrix.isSymmetric_toEuclideanLin_iff.mpr (G.isHermitian_adjMatrix (R := ℝ))
43
44 lemma adjacencyOperator_apply (G : SimpleGraph V) (x : EuclideanSpace ℝ V) :
45 adjacencyOperator G x = G.adjMatrix ℝ *ᵥ x := by
46 classical
47 rfl
48
49 /-- The variationally defined adjacency spectral radius is an eigenvalue. -/
50 theorem hasEigenvalue_adjacencySpectralRadius [Nonempty V] (G : SimpleGraph V) :
51 Module.End.HasEigenvalue (adjacencyOperator G) (adjacencySpectralRadius G) := by
52 exact (adjacencyOperator_isSymmetric G).hasEigenvalue_iSup_of_finiteDimensional
53
54 /-- Coordinatewise absolute value on a real Euclidean space. -/
55 def vectorAbs (x : EuclideanSpace ℝ V) : EuclideanSpace ℝ V :=
56 WithLp.toLp 2 fun i ↦ |x i|
57
58 @[simp] lemma vectorAbs_apply (x : EuclideanSpace ℝ V) (i : V) :
59 vectorAbs x i = |x i| := rfl
60
61 @[simp] lemma norm_vectorAbs (x : EuclideanSpace ℝ V) :
62 ‖vectorAbs x‖ = ‖x‖ := by
63 simp only [EuclideanSpace.norm_eq, vectorAbs_apply, Real.norm_eq_abs, abs_abs]
64
65 lemma adjacency_quadraticForm_le_abs (G : SimpleGraph V) (x : EuclideanSpace ℝ V) :
66 ⟪adjacencyOperator G x, x⟫_ℝ ≤
67 ⟪adjacencyOperator G (vectorAbs x), vectorAbs x⟫_ℝ := by
68 classical
69 simp only [adjacencyOperator_apply, EuclideanSpace.inner_eq_star_dotProduct, star_trivial,
70 dotProduct, mulVec, vectorAbs_apply]
71 apply Finset.sum_le_sum
72 intro i _
73 apply Finset.sum_le_sum
74 intro j _
75 split_ifs
76 · rw [one_mul**Refactoring adjacencyOperator to adjacencyMatrix function**
**Exploring proof relation and reducibility**
$ /bin/bash -lc 'lake env lean BootsRoyle/Spectral.lean'
BootsRoyle/Spectral.lean:53:28: error(lean.synthInstanceFailed): failed to synthesize instance of type class
Decidable (G.Adj i j)
Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
BootsRoyle/Spectral.lean:66:8: warning: automatically included section variable(s) unused in theorem `BootsRoyle.vectorAbs_apply`:
[Fintype V]
[DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
omit [Fintype V] [DecidableEq V] in theorem ...
Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
BootsRoyle/Spectral.lean:69:8: warning: automatically included section variable(s) unused in theorem `BootsRoyle.norm_vectorAbs`:
[DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
omit [DecidableEq V] in theorem ...
Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
BootsRoyle/Spectral.lean:81:2: error: Tactic `apply` failed: could not unify the conclusion of `@Finset.sum_le_sum`
∑ i ∈ ?s, ?f i ≤ ∑ i ∈ ?s, ?g i
with the goal
x.ofLp i * ∑ x_1, adjacencyMatrix G i x_1 * x.ofLp x_1 ≤ |x.ofLp i| * ∑ i_1, adjacencyMatrix G i i_1 * |x.ofLp i_1|
Note: The full type of `@Finset.sum_le_sum` is
∀ {ι : Type ?u.46} {N : Type ?u.45} [inst : AddCommMonoid N] [inst_1 : Preorder N] {f g : ι → N} {s : Finset ι}
[AddLeftMono N], (∀ i ∈ s, f i ≤ g i) → ∑ i ∈ s, f i ≤ ∑ i ∈ s, g i
V : Type u_1
inst✝¹ : Fintype V
inst✝ : DecidableEq V
G : SimpleGraph V
x : EuclideanSpace ℝ V
i : V
a✝ : i ∈ Finset.univ
⊢ x.ofLp i * ∑ x_1, adjacencyMatrix G i x_1 * x.ofLp x_1 ≤ |x.ofLp i| * ∑ i_1, adjacencyMatrix G i i_1 * |x.ofLp i_1|**Refining adjacency matrix simplification**
$ /bin/bash -lc 'lake env lean BootsRoyle/Spectral.lean' BootsRoyle/Spectral.lean:61:8: warning: automatically included section variable(s) unused in theorem `BootsRoyle.vectorAbs_apply`: [Fintype V] [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` BootsRoyle/Spectral.lean:64:8: warning: automatically included section variable(s) unused in theorem `BootsRoyle.norm_vectorAbs`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` BootsRoyle/Spectral.lean:82:6: error: invalid 'calc' step, left-hand side is x.ofLp j * x.ofLp i : (fun x => ℝ) j but is expected to be x.ofLp i * x.ofLp j : ℝ BootsRoyle/Spectral.lean:83:6: error: invalid 'calc' step, right-hand side is |x.ofLp j| * |x.ofLp i| : (fun x => ℝ) j but is expected to be |x.ofLp i| * |x.ofLp j| : ℝ
**Implementing swap function**
$ /bin/bash -lc 'lake env lean BootsRoyle/Spectral.lean' BootsRoyle/Spectral.lean:61:8: warning: automatically included section variable(s) unused in theorem `BootsRoyle.vectorAbs_apply`: [Fintype V] [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` BootsRoyle/Spectral.lean:64:8: warning: automatically included section variable(s) unused in theorem `BootsRoyle.norm_vectorAbs`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
**Formulating Perron vector theorem using max eigenvalue**
$ /bin/bash -lc "rg -n \"def IsSymmetric|abbrev IsSymmetric|def IsSelfAdjoint|theorem.*isSelfAdjoint.*isSymmetric|IsSymmetric.*toSelfAdjoint\" Mathlib/Analysis/InnerProductSpace | sed -n '1,180p'; sed -n '120,190p' Mathlib/Analysis/InnerProductSpace/Adjoint.lean; sed -n '190,245p' Mathlib/Analysis/InnerProductSpace/Adjoint.lean"
Mathlib/Analysis/InnerProductSpace/Symmetric.lean:59:def IsSymmetric (T : E →ₗ[𝕜] E) : Prop :=
Mathlib/Analysis/InnerProductSpace/Adjoint.lean:363:theorem _root_.ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric {A : E →L[𝕜] E} :
Mathlib/Analysis/InnerProductSpace/Adjoint.lean:511:def IsSymmetric.toSelfAdjoint (hT : IsSymmetric T) : selfAdjoint (E →L[𝕜] E) :=
Mathlib/Analysis/InnerProductSpace/Adjoint.lean:514:theorem IsSymmetric.coe_toSelfAdjoint (hT : IsSymmetric T) : (hT.toSelfAdjoint : E →ₗ[𝕜] E) = T :=
Mathlib/Analysis/InnerProductSpace/Adjoint.lean:517:theorem IsSymmetric.toSelfAdjoint_apply (hT : IsSymmetric T) {x : E} :
open InnerProduct
/-- The fundamental property of the adjoint. -/
theorem adjoint_inner_left (A : E →L[𝕜] F) (x : E) (y : F) : ⟪(A†) y, x⟫ = ⟪y, A x⟫ :=
adjointAux_inner_left A x y
/-- The fundamental property of the adjoint. -/
theorem adjoint_inner_right (A : E →L[𝕜] F) (x : E) (y : F) : ⟪x, (A†) y⟫ = ⟪A x, y⟫ :=
adjointAux_inner_right A x y
/-- The adjoint is involutive. -/
@[simp]
theorem adjoint_adjoint (A : E →L[𝕜] F) : A†† = A :=
adjointAux_adjointAux A
/-- The adjoint of the composition of two operators is the composition of the two adjoints
in reverse order. -/
@[simp]
theorem adjoint_comp (A : F →L[𝕜] G) (B : E →L[𝕜] F) : (A ∘L B)† = B† ∘L A† := by
ext v
refine ext_inner_left 𝕜 fun w => ?_
simp [adjoint_inner_right]
theorem apply_norm_sq_eq_inner_adjoint_left (A : E →L[𝕜] F) (x : E) :
‖A x‖ ^ 2 = re ⟪(A† ∘L A) x, x⟫ := by
have h : ⟪(A† ∘L A) x, x⟫ = ⟪A x, A x⟫ := by rw [← adjoint_inner_left]; rfl
rw [h, ← inner_self_eq_norm_sq (𝕜 := 𝕜) _]
theorem apply_norm_eq_sqrt_inner_adjoint_left (A : E →L[𝕜] F) (x : E) :
‖A x‖ = √(re ⟪(A† ∘L A) x, x⟫) := by
rw [← apply_norm_sq_eq_inner_adjoint_left, Real.sqrt_sq (norm_nonneg _)]
theorem apply_norm_sq_eq_inner_adjoint_right (A : E →L[𝕜] F) (x : E) :
‖A x‖ ^ 2 = re ⟪x, (A† ∘L A) x⟫ := by
have h : ⟪x, (A† ∘L A) x⟫ = ⟪A x, A x⟫ := by rw [← adjoint_inner_right]**Planning eigenvector proof coding** **Defining continuous adjacency operator**
$ /bin/bash -lc "sed -n '350,372p' Mathlib/Analysis/InnerProductSpace/Adjoint.lean; sed -n '50,75p' Mathlib/Analysis/InnerProductSpace/Symmetric.lean; rg -n \"exists_mem_ne_zero_of_ne_bot|exists_ne_zero_mem\" Mathlib/LinearAlgebra | head -20"
theorem conj_adjoint {T : E →L[𝕜] E} (hT : IsSelfAdjoint T) (S : E →L[𝕜] F) :
IsSelfAdjoint (S ∘L T ∘L S.adjoint) := by
rw [isSelfAdjoint_iff'] at hT ⊢
simp only [hT, adjoint_comp, adjoint_adjoint]
exact ContinuousLinearMap.comp_assoc _ _ _
/-- Conjugating preserves self-adjointness. -/
theorem adjoint_conj {T : E →L[𝕜] E} (hT : IsSelfAdjoint T) (S : F →L[𝕜] E) :
IsSelfAdjoint (S.adjoint ∘L T ∘L S) := by
rw [isSelfAdjoint_iff'] at hT ⊢
simp only [hT, adjoint_comp, adjoint_adjoint]
exact ContinuousLinearMap.comp_assoc _ _ _
theorem _root_.ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric {A : E →L[𝕜] E} :
IsSelfAdjoint A ↔ (A : E →ₗ[𝕜] E).IsSymmetric :=
⟨fun hA => hA.isSymmetric, fun hA =>
ext fun x => ext_inner_right 𝕜 fun y => (A.adjoint_inner_left y x).symm ▸ (hA x y).symm⟩
theorem _root_.LinearMap.IsSymmetric.isSelfAdjoint {A : E →L[𝕜] E}
(hA : (A : E →ₗ[𝕜] E).IsSymmetric) : IsSelfAdjoint A := by
rwa [← ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric] at hA
/-- The orthogonal projection is self-adjoint. -/
local notation "⟪" x ", " y "⟫" => inner 𝕜 x y
namespace LinearMap
/-! ### Symmetric operators -/
/-- A (not necessarily bounded) operator on an inner product space is symmetric, if for all
`x`, `y`, we have `⟪T x, y⟫ = ⟪x, T y⟫`. -/
def IsSymmetric (T : E →ₗ[𝕜] E) : Prop :=
∀ x y, ⟪T x, y⟫ = ⟪x, T y⟫
section Real
/-- An operator `T` on an inner product space is symmetric if and only if it is
`LinearMap.IsSelfAdjoint` with respect to the sesquilinear form given by the inner product. -/
theorem isSymmetric_iff_sesqForm (T : E →ₗ[𝕜] E) :
T.IsSymmetric ↔ LinearMap.IsSelfAdjoint (R := 𝕜) (M := E) (LinearMap.flip (innerₛₗ 𝕜)) T :=
⟨fun h x y => (h y x).symm, fun h x y => (h y x).symm⟩
end Real
theorem IsSymmetric.conj_inner_sym {T : E →ₗ[𝕜] E} (hT : IsSymmetric T) (x y : E) :
conj ⟪T x, y⟫ = ⟪T y, x⟫ := by rw [hT x y, inner_conj_symm]
@[simp]
Mathlib/LinearAlgebra/Eigenspace/Basic.lean:205: Submodule.ex**Adding CLM definition** **Refining eigenvector proof details**
**Compiling codebase**
$ /bin/bash -lc 'lake env lean BootsRoyle/Spectral.lean' BootsRoyle/Spectral.lean:66:8: warning: automatically included section variable(s) unused in theorem `BootsRoyle.vectorAbs_apply`: [Fintype V] [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` BootsRoyle/Spectral.lean:69:8: warning: automatically included section variable(s) unused in theorem `BootsRoyle.norm_vectorAbs`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
**Analyzing positivity conditions for eigenvectors** **Tracing connectivity propagation for zero eigenvector entries**
$ /bin/bash -lc "rg -n \"def Connected|abbrev Connected|Connected.*exists.*Walk|Preconnected|preconnected_iff|Connected.*walk|exists_walk\" Mathlib/Combinatorics/SimpleGraph/Connectivity.lean | sed -n '1,260p'; rg -n \"sum_eq_zero_iff_of_nonneg|sum_eq_zero_iff\" Mathlib/Algebra/Order Mathlib | head -60" rg: Mathlib/Combinatorics/SimpleGraph/Connectivity.lean: IO error for operation on Mathlib/Combinatorics/SimpleGraph/Connectivity.lean: No such file or directory (os error 2) Mathlib/Algebra/Order/Ring/GeomSum.lean:138:lemma geom_sum_eq_zero_iff_neg_one (hn : n ≠ 0) : ∑ i ∈ range n, x ^ i = 0 ↔ x = -1 ∧ Even n := by Mathlib/Algebra/Order/Ring/GeomSum.lean:149: or_congr (geom_sum_pos_iff hn) (geom_sum_eq_zero_iff_neg_one hn), ← Nat.not_even_iff_odd, ← Mathlib/MeasureTheory/Integral/MeanInequalities.lean:201: simpa [hi₀, h2i₀, sum_eq_zero_iff_of_nonneg (fun i hi ↦ h2p i <| mem_insert_of_mem hi)] Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean:132: [lapMatrix_toLinearMap₂', sum_eq_zero_iff_of_nonneg, sub_eq_zero] Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean:86: rw [sum_eq_zero_iff_of_nonneg fun _ _ ↦ mul_self_nonneg _] Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean:132: simpa [(sum_eq_zero_iff_of_nonneg hg).1 h i hi] using ht i hi Mathlib/Algebra/Order/BigOperators/Group/Finset.lean:192:@[to_additive sum_eq_zero_iff_of_nonneg] Mathlib/Algebra/Order/BigOperators/Group/Finset.lean:212:@[to_additive sum_eq_zero_iff_of_nonpos] Mathlib/Algebra/Order/BigOperators/Expect.lean:38: simp +contextual [expect, sum_eq_zero_iff_of_nonneg hf] Mathlib/Algebra/Order/BigOperators/Expect.lean:42: simp +contextual [expect, sum_eq_zero_iff_of_nonpos hf] Mathlib/Combinatorics/SetFamily/FourFunctions.lean:355: · simp only [Pi.zero_apply, sum_const_zero, eq_comm, Fintype.sum_eq_zero_iff_of_nonneg hg] at hfg Mathlib/Combinatorics/SetFamily/FourFunctions.lean:358: · simp only [Pi.zero_apply, sum_const_zero, Fintype.sum_eq_zero_iff_of_nonneg hf.le] at hfg Mathlib/MeasureTheory/Measure/MeasureSpace.lean:1206: ENNReal.summable.tsum_eq_zero_iff.2 _, add_zero] Mathlib/Combinatorics/Enumerative/Partition/Basic.lean:96: have lz : (l.filter (· = 0)).sum = 0 := by simp [sum_eq_zero_iff] Mathlib/Combinatorics/Enumerative/Partition/Basic.lean:173: eq_zero_of_
**Searching for files**
$ /bin/bash -lc "rg -n \"def Connected|structure Connected|abbrev Connected|def Preconnected|structure Preconnected|Connected.*Walk|Preconnected.*Walk|exists_walk\" Mathlib/Combinatorics/SimpleGraph | sed -n '1,300p'"
Mathlib/Combinatorics/SimpleGraph/Prod.lean:277: have ⟨wG, hwG⟩ := exists_walk_of_edist_ne_top rGH.1
Mathlib/Combinatorics/SimpleGraph/Prod.lean:278: have ⟨wH, hwH⟩ := exists_walk_of_edist_ne_top rGH.2
Mathlib/Combinatorics/SimpleGraph/Prod.lean:286: · have ⟨w, hw⟩ := exists_walk_of_edist_ne_top h
Mathlib/Combinatorics/SimpleGraph/Metric.lean:62:protected theorem Reachable.exists_walk_length_eq_edist (hr : G.Reachable u v) :
Mathlib/Combinatorics/SimpleGraph/Metric.lean:66:protected theorem Connected.exists_walk_length_eq_edist (hconn : G.Connected) (u v : V) :
Mathlib/Combinatorics/SimpleGraph/Metric.lean:68: (hconn u v).exists_walk_length_eq_edist
Mathlib/Combinatorics/SimpleGraph/Metric.lean:95:lemma exists_walk_of_edist_ne_top (h : G.edist u v ≠ ⊤) :
Mathlib/Combinatorics/SimpleGraph/Metric.lean:97: (reachable_of_edist_ne_top h).exists_walk_length_eq_edist
Mathlib/Combinatorics/SimpleGraph/Metric.lean:106: obtain ⟨p, hp⟩ := exists_walk_of_edist_ne_top huv
Mathlib/Combinatorics/SimpleGraph/Metric.lean:107: obtain ⟨q, hq⟩ := exists_walk_of_edist_ne_top hvw
Mathlib/Combinatorics/SimpleGraph/Metric.lean:116:lemma exists_walk_of_edist_eq_coe {k : ℕ} (h : G.edist u v = k) :
Mathlib/Combinatorics/SimpleGraph/Metric.lean:119: have ⟨p, hp⟩ := exists_walk_of_edist_ne_top this
Mathlib/Combinatorics/SimpleGraph/Metric.lean:134: · obtain ⟨w, hw⟩ := exists_walk_of_edist_ne_top <| by rw [h]; simp
Mathlib/Combinatorics/SimpleGraph/Metric.lean:151: · obtain ⟨w, hw⟩ := exists_walk_of_edist_eq_coe h
Mathlib/Combinatorics/SimpleGraph/Metric.lean:193: · obtain ⟨_, hw⟩ := hr.exists_walk_length_eq_edist
Mathlib/Combinatorics/SimpleGraph/Metric.lean:218:protected theorem Reachable.exists_walk_length_eq_dist (hr : G.Reachable u v) :
Mathlib/Combinatorics/SimpleGraph/Metric.lean:222:protected theorem Connected.exists_walk_length_eq_dist (hconn : G.Connected) (u v : V) :
Mathlib/Combinatorics/SimpleGraph/Metric.lean:224: dist_eq_sInf ▸ (hconn u v).exists_walk_len$ /bin/bash -lc "sed -n '210,340p' Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean; rg -n \"Reachable.*induction|reachable.*induction|Walk.*propagate|IsPreconnected.*induction|Preconnected.*eq\" Mathlib/Combinatorics/SimpleGraph/Connectivity Mathlib/Combinatorics/SimpleGraph/Paths.lean | sed -n '1,220p'"
lemma not_reachable_of_neighborSet_right_eq_empty {G : SimpleGraph V} {u v : V} (huv : u ≠ v)
(hv : G.neighborSet v = ∅) : ¬G.Reachable u v :=
fun r ↦ not_reachable_of_neighborSet_left_eq_empty huv.symm hv r.symm
lemma not_reachable_of_left_degree_zero {G : SimpleGraph V} {u v : V} [Fintype (G.neighborSet u)]
(huv : u ≠ v) (hu : G.degree u = 0) : ¬G.Reachable u v :=
(Reachable.degree_pos_left huv).mt (by simp [hu])
lemma not_reachable_of_right_degree_zero {G : SimpleGraph V} {u v : V} [Fintype (G.neighborSet v)]
(huv : u ≠ v) (hu : G.degree v = 0) : ¬G.Reachable u v := by
rw [reachable_comm]
exact not_reachable_of_left_degree_zero huv.symm hu
/-- The equivalence relation on vertices given by `SimpleGraph.Reachable`. -/
@[instance_reducible]
def reachableSetoid : Setoid V := Setoid.mk _ G.reachable_is_equivalence
/-- A graph is preconnected if every pair of vertices is reachable from one another. -/
def Preconnected : Prop := ∀ u v : V, G.Reachable u v
theorem Preconnected.map {G : SimpleGraph V} {H : SimpleGraph V'} (f : G →g H) (hf : Surjective f)
(hG : G.Preconnected) : H.Preconnected :=
hf.forall₂.2 fun _ _ => Nonempty.map (Walk.map _) <| hG _ _
@[gcongr, mono]
protected lemma Preconnected.mono {G G' : SimpleGraph V} (h : G ≤ G') (hG : G.Preconnected) :
G'.Preconnected := fun u v => (hG u v).mono h
lemma preconnected_iff_reachable_eq_top : G.Preconnected ↔ G.Reachable = ⊤ := by
aesop (add simp Preconnected)
lemma preconnected_bot_iff_subsingleton : (⊥ : SimpleGraph V).Preconnected ↔ Subsingleton V := by
refine ⟨fun h ↦ ?_, fun h ↦ by simp [Preconnected]⟩
contrapose! h
simp [nontrivial_iff.mp h, Preconnected, reachable_bot]
lemma preconnected_bot [Subsingleton V] : (⊥ : SimpleGraph V).Preconnected :=
preconnected_bot_iff_subsingleton.mpr ‹_›
lemma not_preconnected_bot [Nontrivial V] : ¬(⊥ : SimpleGraph V).Preconnected :=
preconnected_bot_iff_subsingleton.not.mpr <| not_subsingleton_iff_nontrivial.mpr ‹_›
@[simp]**Proving vertex zero propagation lemma** **Inductively proving positivity on walks**
**Compiling project**
$ /bin/bash -lc 'lake env lean BootsRoyle/Spectral.lean' BootsRoyle/Spectral.lean:66:8: warning: automatically included section variable(s) unused in theorem `BootsRoyle.vectorAbs_apply`: [Fintype V] [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` BootsRoyle/Spectral.lean:69:8: warning: automatically included section variable(s) unused in theorem `BootsRoyle.norm_vectorAbs`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` BootsRoyle/Spectral.lean:158:33: error: Application type mismatch: The argument hx_eigen has type (adjacencyOperator G) x = μ • x but is expected to have type ((adjacencyOperator G) x).ofLp = (μ • x).ofLp in the application congr_fun hx_eigen BootsRoyle/Spectral.lean:174:37: error: Application type mismatch: The argument hv_ne has type 0 = x.ofLp v but is expected to have type ¬x.ofLp v ≠ 0 in the application not_ne_iff.mp hv_ne BootsRoyle/Spectral.lean:181:17: error: Application type mismatch: The argument eigenvector_zero_propagates G hx_nonneg hx_eigen huz hv has type x.ofLp z = 0 but is expected to have type 0 = x.ofLp z in the application ih (eigenvector_zero_propagates G hx_nonneg hx_eigen huz hv)
**Simplifying inequality proof with lt_of_le_of_ne**
**Verifying induction usage in goal compilation**
$ /bin/bash -lc 'lake env lean BootsRoyle/Spectral.lean' BootsRoyle/Spectral.lean:66:8: warning: automatically included section variable(s) unused in theorem `BootsRoyle.vectorAbs_apply`: [Fintype V] [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` BootsRoyle/Spectral.lean:69:8: warning: automatically included section variable(s) unused in theorem `BootsRoyle.norm_vectorAbs`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` BootsRoyle/Spectral.lean:182:8: error: Type mismatch ih (Eq.symm (eigenvector_zero_propagates G hx_nonneg hx_eigen huz hv)) has type x.ofLp z = 0 → x.ofLp w = 0 but is expected to have type x.ofLp w = 0
**Analyzing induction hypothesis structure** **Writing recursive local lemma with induction**
$ /bin/bash -lc 'lake env lean BootsRoyle/Spectral.lean' BootsRoyle/Spectral.lean:66:8: warning: automatically included section variable(s) unused in theorem `BootsRoyle.vectorAbs_apply`: [Fintype V] [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` BootsRoyle/Spectral.lean:69:8: warning: automatically included section variable(s) unused in theorem `BootsRoyle.norm_vectorAbs`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
**Establishing positivity and normalization definitions**
$ /bin/bash -lc 'rg -n "theorem sum_pos|lemma sum_pos" Mathlib/Algebra/Order/BigOperators Mathlib | head -80'
Mathlib/NumberTheory/Padics/PadicVal/Basic.lean:345:theorem sum_pos_of_pos {n : ℕ} {F : ℕ → ℚ} (hF : ∀ i, i < n → 0 < padicValRat p (F i))
Mathlib/Data/Finsupp/Order.lean:64:theorem sum_pos (h : ∀ i ∈ f.support, 0 < g i (f i)) (hf : f ≠ 0) : 0 < f.sum g :=
Mathlib/Data/Finsupp/Order.lean:67:theorem sum_pos' (h : ∀ i ∈ f.support, 0 ≤ g i (f i)) (hf : ∃ i ∈ f.support, 0 < g i (f i)) :**Planning normalization and positivity proofs**
$ /bin/bash -lc 'lake env lean BootsRoyle/Spectral.lean' BootsRoyle/Spectral.lean:66:8: warning: automatically included section variable(s) unused in theorem `BootsRoyle.vectorAbs_apply`: [Fintype V] [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` BootsRoyle/Spectral.lean:69:8: warning: automatically included section variable(s) unused in theorem `BootsRoyle.norm_vectorAbs`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
**Analyzing spectral radius monotonicity under edge addition** **Planning proofs for spectral identities and arithmetic lemmas**
**Defining alpha and setting lemma constraints** **Planning denominator positivity and graph formalization**
$ /bin/bash -lc "rg -n \"join\" Mathlib/Combinatorics/SimpleGraph/Operations.lean Mathlib/Combinatorics/SimpleGraph | grep -E \"def |theorem |lemma |Join|join\" | sed -n '1,240p'; rg -n \"pathGraph\" Mathlib/Combinatorics/SimpleGraph | head -80"
Mathlib/Combinatorics/SimpleGraph/Operations.lean:99:lemma disjoint_sdiff_neighborFinset_image :
Mathlib/Combinatorics/SimpleGraph/Operations.lean:100: Disjoint (G.edgeFinset \ G.incidenceFinset t) ((G.neighborFinset s).image (s(·, t))) := by
Mathlib/Combinatorics/SimpleGraph/Operations.lean:101: rw [disjoint_iff_ne]
Mathlib/Combinatorics/SimpleGraph/Operations.lean:114: card_union_of_disjoint G.disjoint_sdiff_neighborFinset_image, card_sdiff_of_subset inc,
Mathlib/Combinatorics/SimpleGraph/Operations.lean:125: card_union_of_disjoint G.disjoint_sdiff_neighborFinset_image, card_sdiff_of_subset inc,
Mathlib/Combinatorics/SimpleGraph/Operations.lean:189:lemma disjoint_edge {u v : V} : Disjoint G (edge u v) ↔ ¬G.Adj u v := by
Mathlib/Combinatorics/SimpleGraph/Operations.lean:193: simp [← disjoint_edgeSet, edgeSet_edge_of_ne h]
Mathlib/Combinatorics/SimpleGraph/Operations.lean:196: simp [disjoint_edge, h]
Mathlib/Combinatorics/SimpleGraph/Operations.lean:201: exact Set.disjoint_left.mpr G.edgeSet_subset_compl_diagSet |>.sdiff_eq_left
Mathlib/Combinatorics/SimpleGraph/DeleteEdges.lean:81:@[simp] lemma deleteEdges_eq_self : G.deleteEdges s = G ↔ Disjoint G.edgeSet s := by
Mathlib/Combinatorics/SimpleGraph/DeleteEdges.lean:82: rw [deleteEdges, sdiff_eq_left, disjoint_fromEdgeSet]
Mathlib/Combinatorics/SimpleGraph/DeleteEdges.lean:132: rw [edgeSet_fromEdgeSet, sdiff_eq_left, ← Set.subset_compl_iff_disjoint_right]
Mathlib/Combinatorics/SimpleGraph/Regularity/Equitabilise.lean:95: refine ⟨R.extend ht.ne_empty sdiff_disjoint (sdiff_sup_cancel hts), ?_, ?_, ?_⟩
Mathlib/Combinatorics/SimpleGraph/Regularity/Equitabilise.lean:114: ⟨R.extend ht.ne_empty sdiff_disjoint (sdiff_sup_cancel <| htu.trans <| P.le hu₁), ?_, ?_, ?_⟩
Mathlib/Combinatorics/SimpleGraph/Regularity/Equitabilise.lean:134: (disjoint_of_subset_right htu <|
Mathlib/Combinatorics/SimpleGraph/Regularity/Equitabilise.lean:135: P.disjoint (mem_of_mem_erase hx) hu₁ <| ne_of_mem_erase**Planning join implementation**
The tooling search found no reusable Lean planar-graph development. I have therefore started with the spectral side and now have a compiled, axiom-free Perron–Frobenius layer: the adjacency spectral radius is defined variationally, shown to be an eigenvalue, shown to admit a nonnegative eigenvector, strengthened to strict positivity for connected graphs, and normalized exactly as the paper’s \(\ell^1\)-Perron vector. This closes one genuine mathlib gap; next I’m testing whether the paper’s optimization core can be isolated and kernel-checked before investing in the much larger combinatorial-map layer.
**Formalizing Rayleigh bound lemma** **Identifying strict graph inequality edge**
$ /bin/bash -lc "rg -n \"le_iff.*Adj|not_le.*Adj|exists.*Adj.*not|lt_iff.*Adj|ssubset.*edgeSet\" Mathlib/Combinatorics/SimpleGraph/Basic.lean Mathlib/Combinatorics/SimpleGraph | sed -n '1,220p'; rg -n \"quadraticForm.*(add|sub)|inner.*adjMatrix|sum.*edge.*x\" Mathlib/Combinatorics/SimpleGraph | sed -n '1,160p'"
Mathlib/Combinatorics/SimpleGraph/Basic.lean:216:lemma le_iff_adj {G H : SimpleGraph V} : G ≤ H ↔ ∀ v w, G.Adj v w → H.Adj v w := .rfl
Mathlib/Combinatorics/SimpleGraph/Basic.lean:492:theorem edgeSet_ssubset_edgeSet : edgeSet G₁ ⊂ edgeSet G₂ ↔ G₁ < G₂ := by simp
Mathlib/Combinatorics/SimpleGraph/Basic.lean:499:@[gcongr] alias ⟨_, edgeSet_strict_mono⟩ := edgeSet_ssubset_edgeSet
Mathlib/Combinatorics/SimpleGraph/Paths.lean:326:theorem cons_isCycle_iff {u v : V} (p : G.Walk v u) (h : G.Adj u v) :
Mathlib/Combinatorics/SimpleGraph/Operations.lean:165:lemma edge_le_iff {v w : V} : edge v w ≤ G ↔ v = w ∨ G.Adj v w := by
Mathlib/Combinatorics/SimpleGraph/Subgraph.lean:950:theorem subgraphOfAdj_le_iff {u v : V} (h : G.Adj u v) (H : G.Subgraph) :
Mathlib/Combinatorics/SimpleGraph/Clique.lean:319:theorem is3Clique_triple_iff : G.IsNClique 3 {a, b, c} ↔ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c := by
Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean:768:theorem IsBridge.reachable_iff_adj (h : G.IsBridge s(u, v)) : G.Reachable u v ↔ G.Adj u v := by
Mathlib/Combinatorics/SimpleGraph/Basic.lean:216:lemma le_iff_adj {G H : SimpleGraph V} : G ≤ H ↔ ∀ v w, G.Adj v w → H.Adj v w := .rfl
Mathlib/Combinatorics/SimpleGraph/Basic.lean:492:theorem edgeSet_ssubset_edgeSet : edgeSet G₁ ⊂ edgeSet G₂ ↔ G₁ < G₂ := by simp
Mathlib/Combinatorics/SimpleGraph/Basic.lean:499:@[gcongr] alias ⟨_, edgeSet_strict_mono⟩ := edgeSet_ssubset_edgeSet
Mathlib/Combinatorics/SimpleGraph/Matching.lean:520: simp only [Walk.toSubgraph, singletonSubgraph_le_iff, subgraphOfAdj_verts, Set.mem_insert_iff,
Mathlib/Combinatorics/SimpleGraph/Acyclic.lean:352: (by simpa [deleteEdges, ← edgeSet_ssubset_edgeSet])
Mathlib/Combinatorics/SimpleGraph/Acyclic.lean:415: have ⟨e, heH, heF⟩ := Set.exists_of_ssubset <| edgeSet_strict_mono hFH
Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean:490: have := add_div_le_sum_sq_div_card t (fun x => (G.edgeDensity x.1 x.2 : ℝ))
Mathlib/Combinatorics/SimpleGraph/Regul**Planning proof for quadratic form inequality**
$ /bin/bash -lc "# use #check in a temporary lean file through stdin is unsupported; inspect declarations
rg -n \"theorem sum_lt_sum|lemma sum_lt_sum\" Mathlib/Algebra/Order/BigOperators | head -80; sed -n '55,105p' Mathlib/Algebra/Order/BigOperators/Group/Finset.lean"
`g i`, `i ∈ s`, be a nonempty finite family of elements of `M` such that `∀ i ∈ s, p (g i)`. Then
`f (∑ i ∈ s, g i) ≤ ∑ i ∈ s, f (g i)`. -/
add_decl_doc le_sum_nonempty_of_subadditive_on_pred
/-- If `f : M → N` is a submultiplicative function, `f (x * y) ≤ f x * f y` and `g i`, `i ∈ s`, is a
nonempty finite family of elements of `M`, then `f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)`. -/
@[to_additive le_sum_nonempty_of_subadditive]
theorem le_prod_nonempty_of_submultiplicative [IsOrderedMonoid N] (f : M → N)
(h_mul : ∀ x y, f (x * y) ≤ f x * f y) {s : Finset ι} (hs : s.Nonempty) (g : ι → M) :
f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i) :=
le_prod_nonempty_of_submultiplicative_on_pred f (fun _ ↦ True) (fun x y _ _ ↦ h_mul x y)
(fun _ _ _ _ ↦ trivial) g s hs fun _ _ ↦ trivial
/-- If `f : M → N` is a subadditive function, `f (x + y) ≤ f x + f y` and `g i`, `i ∈ s`, is a
nonempty finite family of elements of `M`, then `f (∑ i ∈ s, g i) ≤ ∑ i ∈ s, f (g i)`. -/
add_decl_doc le_sum_nonempty_of_subadditive
/-- Let `{x | p x}` be a subsemigroup of a commutative monoid `M`. Let `f : M → N` be a map
such that `f 1 = 1` and `f` is submultiplicative on `{x | p x}`, i.e.,
`p x → p y → f (x * y) ≤ f x * f y`. Let `g i`, `i ∈ s`, be a finite family of elements of `M` such
that `∀ i ∈ s, p (g i)`. Then `f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)`. -/
@[to_additive le_sum_of_subadditive_on_pred]
theorem le_prod_of_submultiplicative_on_pred [IsOrderedMonoid N] (f : M → N) (p : M → Prop)
(h_one : f 1 ≤ 1) (h_mul : ∀ x y, p x → p y → f (x * y) ≤ f x * f y)
(hp_mul : ∀ x y, p x → p y → p (x * y)) (g : ι → M) {s : Finset ι} (hs : ∀ i ∈ s, p (g i)) :
f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i) := by
rcases eq_empty_or_nonempty s with (rfl | hs_nonempty)
· simp [h_one]
· exact le_prod_nonempty_of_submultiplicative_on_pred f p h_mul hp_mul g s hs_nonempty hs
/-- Let `{x | p x}` be a subsemigroup of a commutative additive monoid `M`. Let `f : M → N` be a map
such that `f 0 = 0` and `f` **Planning sum inequality proof** **Postponing Perron eigenvalue comparison**
$ /bin/bash -lc 'lake env lean BootsRoyle/Arithmetic.lean' BootsRoyle/Arithmetic.lean:20:4: error(lean.dependsOnNoncomputable): failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Real.instDivInvMonoid', which is 'noncomputable' BootsRoyle/Arithmetic.lean:24:4: error(lean.dependsOnNoncomputable): failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Real.instDivInvMonoid', which is 'noncomputable' BootsRoyle/Arithmetic.lean:28:4: error(lean.dependsOnNoncomputable): failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Real.instDivInvMonoid', which is 'noncomputable' BootsRoyle/Arithmetic.lean:32:4: error(lean.dependsOnNoncomputable): failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Real.instDivInvMonoid', which is 'noncomputable' BootsRoyle/Arithmetic.lean:41:6: error(lean.unknownIdentifier): Unknown identifier `sq_sqrt` BootsRoyle/Arithmetic.lean:40:46: error: unsolved goals n : ℕ hn : 3 ≤ n ⊢ √(8 * ↑n - 19) ^ 2 = 8 * ↑n - 19 BootsRoyle/Arithmetic.lean:49:34: warning: Variable name `hn` is not explicitly referenced. Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning: [apply] _hn Note: This linter can be disabled with `set_option linter.unusedVariables false`
**Marking Real.sq_sqrt as noncomputable**
$ /bin/bash -lc 'lake env lean BootsRoyle/Arithmetic.lean' BootsRoyle/Arithmetic.lean:49:34: warning: Variable name `hn` is not explicitly referenced. Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning: [apply] _hn Note: This linter can be disabled with `set_option linter.unusedVariables false`
**Proving theorem bounds for parameters** **Formalizing inequalities with field simplifications**
**Resolving Nat subtraction and cast constraints**
$ /bin/bash -lc 'lake env lean BootsRoyle/Arithmetic.lean' BootsRoyle/Arithmetic.lean:49:34: warning: Variable name `hn` is not explicitly referenced. Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning: [apply] _hn Note: This linter can be disabled with `set_option linter.unusedVariables false` BootsRoyle/Arithmetic.lean:107:4: error: mod_cast has type 3 * k ≤ 2 * n - 4 but is expected to have type ↑(3 * k) ≤ Int.subNatNat (2 * n) 4
**Analyzing Nat subtraction casting issues**
$ /bin/bash -lc "nl -ba BootsRoyle/Arithmetic.lean | sed -n '98,116p'"
98 gammaOuter k = 2 * ((k : ℝ) - 4) / (3 * k) := by
99 simp [gammaOuter, show ¬k ≤ 4 by omega]
100
101 lemma cubicWeightLowerBound_bounds {n k : ℕ} {t : ℝ}
102 (hk : 0 < k) (hkmax : 3 * k ≤ 2 * n - 4) (ht : 3 < t) :
103 (k : ℝ) / (2 * n - 4) < cubicWeightLowerBound n k t ∧
104 cubicWeightLowerBound n k t < 1 / 2 := by
105 have hkR : (0 : ℝ) < k := by exact_mod_cast hk
106 have hkmax' : (3 : ℝ) * k ≤ 2 * n - 4 := by
107 exact_mod_cast hkmax
108 have ht0 : 0 < t := lt_trans (by norm_num) ht
109 let D : ℝ := 2 * n - k - 4 + 3 * k / t
110 have hfracpos : 0 < (3 : ℝ) * k / t := div_pos (mul_pos (by norm_num) hkR) ht0
111 have hfraclt : (3 : ℝ) * k / t < k := by
112 rw [div_lt_iff₀ ht0]
113 nlinarith
114 have hDpos : 0 < D := by
115 dsimp [D]
116 nlinarith**Adding cast_sub with hn4 for norm_num**
$ /bin/bash -lc 'lake env lean BootsRoyle/Arithmetic.lean' BootsRoyle/Arithmetic.lean:49:34: warning: Variable name `hn` is not explicitly referenced. Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning: [apply] _hn Note: This linter can be disabled with `set_option linter.unusedVariables false`
**Formalizing polynomial positivity proof** **Expanding polynomial positivity with substitutions** **Defining PlaneEmbedding with face axioms**
**Formalizing Rayleigh lemma proof** **Adding eigen quotient lemma prototype**
$ /bin/bash -lc 'lake env lean BootsRoyle/Spectral.lean' BootsRoyle/Spectral.lean:66:8: warning: automatically included section variable(s) unused in theorem `BootsRoyle.vectorAbs_apply`: [Fintype V] [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` BootsRoyle/Spectral.lean:69:8: warning: automatically included section variable(s) unused in theorem `BootsRoyle.norm_vectorAbs`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` BootsRoyle/Spectral.lean:244:13: error(lean.unknownIdentifier): Unknown constant `RCLike.conj_trivial` BootsRoyle/Spectral.lean:244:2: error: `simp` made no progress
**Removing redundant code and compiling**
$ /bin/bash -lc 'lake env lean BootsRoyle/Spectral.lean' BootsRoyle/Spectral.lean:66:8: warning: automatically included section variable(s) unused in theorem `BootsRoyle.vectorAbs_apply`: [Fintype V] [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` BootsRoyle/Spectral.lean:69:8: warning: automatically included section variable(s) unused in theorem `BootsRoyle.norm_vectorAbs`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` BootsRoyle/Spectral.lean:241:50: error: unsolved goals V : Type u_1 inst✝¹ : Fintype V inst✝ : DecidableEq V G : SimpleGraph V x : EuclideanSpace ℝ V μ : ℝ hx : x ≠ 0 heigen : (adjacencyOperator G) x = μ • x hnorm : ‖x‖ ^ 2 ≠ 0 ⊢ μ * ↑‖x‖ ^ 2 = μ * ‖x‖ ^ 2
**Refining norm coercion simplification**
$ /bin/bash -lc 'lake env lean BootsRoyle/Spectral.lean' BootsRoyle/Spectral.lean:66:8: warning: automatically included section variable(s) unused in theorem `BootsRoyle.vectorAbs_apply`: [Fintype V] [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` BootsRoyle/Spectral.lean:69:8: warning: automatically included section variable(s) unused in theorem `BootsRoyle.norm_vectorAbs`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` BootsRoyle/Spectral.lean:241:50: error: unsolved goals V : Type u_1 inst✝¹ : Fintype V inst✝ : DecidableEq V G : SimpleGraph V x : EuclideanSpace ℝ V μ : ℝ hx : x ≠ 0 heigen : (adjacencyOperator G) x = μ • x hnorm : ‖x‖ ^ 2 ≠ 0 ⊢ μ * ↑(‖x‖ ^ 2) = μ * ‖x‖ ^ 2
**Refining inner product norm proof**
$ /bin/bash -lc 'rg -n "real_inner_self|inner_self_eq_norm_sq" Mathlib/Analysis/InnerProductSpace | head -80' Mathlib/Analysis/InnerProductSpace/TensorProduct.lean:487: ← inner_self_eq_norm_sq (𝕜 := 𝕜), inner_sum, sum_inner, inner_tmul, ← hA, sub_mul, Mathlib/Analysis/InnerProductSpace/LinearMap.lean:236: rw [← sq, inner_self_eq_norm_sq_to_K, norm_pow, norm_ofReal, abs_norm] Mathlib/Analysis/InnerProductSpace/LinearMap.lean:367: simp only [IsIdempotentElem, mul_def, comp_rankOne, rankOne_apply, inner_self_eq_norm_sq_to_K, Mathlib/Analysis/InnerProductSpace/Calculus.lean:142: exact (inner_self_eq_norm_sq _).symm Mathlib/Analysis/InnerProductSpace/MulOpposite.lean:36: norm_sq_eq_re_inner x := (inner_self_eq_norm_sq x.unop).symm Mathlib/Analysis/InnerProductSpace/Reproducing.lean:307: ← inner_self_eq_norm_sq (𝕜 := 𝕜), inner_self_re_eq_norm] Mathlib/Analysis/InnerProductSpace/Orientation.lean:282: simp only [hb, inner_smul_left, real_inner_self_eq_norm_mul_norm, RCLike.conj_to_real] Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean:100: · rw [RCLike.ofReal_pow, ← inner_self_eq_norm_sq_to_K, div_mul_cancel₀, sub_self] Mathlib/Analysis/InnerProductSpace/Adjoint.lean:146: rw [h, ← inner_self_eq_norm_sq (𝕜 := 𝕜) _] Mathlib/Analysis/InnerProductSpace/Adjoint.lean:155: rw [h, ← inner_self_eq_norm_sq (𝕜 := 𝕜) _] Mathlib/Analysis/InnerProductSpace/Adjoint.lean:401: inner_self_eq_norm_sq_to_K, ← adjoint_inner_right T, inner_self_eq_norm_sq_to_K, Mathlib/Analysis/InnerProductSpace/Adjoint.lean:751: simp only [Module.End.mul_apply, adjoint_inner_right, inner_self_eq_norm_sq_to_K] Mathlib/Analysis/InnerProductSpace/Adjoint.lean:758: simp only [adjoint_inner_right, inner_self_eq_norm_sq_to_K] Mathlib/Analysis/InnerProductSpace/ProdL2.lean:186: norm_sq_eq_re_inner y := by rw [inner_self_eq_norm_sq, LinearIsometryEquiv.norm_map] Mathlib/Analysis/InnerProductSpace/TwoDim.lean:199: rw [← real_inner_self_eq_norm_mul_norm, o.inner_rightAngleRotationAux₁_left] Mathlib/Analysis/InnerProductSpace/TwoDim.lean:362: simpa [sq, real_inner_self_eq_norm_sq] usi
**Patching real_inner_self_eq_norm_sq**
$ /bin/bash -lc 'lake env lean BootsRoyle/Spectral.lean' BootsRoyle/Spectral.lean:66:8: warning: automatically included section variable(s) unused in theorem `BootsRoyle.vectorAbs_apply`: [Fintype V] [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` BootsRoyle/Spectral.lean:69:8: warning: automatically included section variable(s) unused in theorem `BootsRoyle.norm_vectorAbs`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
**Adding nonstrict quadratic monotone lemma**
$ /bin/bash -lc 'lake env lean BootsRoyle/Spectral.lean' BootsRoyle/Spectral.lean:66:8: warning: automatically included section variable(s) unused in theorem `BootsRoyle.vectorAbs_apply`: [Fintype V] [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` BootsRoyle/Spectral.lean:69:8: warning: automatically included section variable(s) unused in theorem `BootsRoyle.norm_vectorAbs`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` BootsRoyle/Spectral.lean:262:6: error: Type mismatch mul_nonneg (hx i) (hx j) has type 0 ≤ x.ofLp i * x.ofLp j but is expected to have type x.ofLp i * 0 ≤ x.ofLp i * (1 * x.ofLp j) BootsRoyle/Spectral.lean:263:6: error: Type mismatch le_rfl has type ?m.88 ≤ ?m.88 but is expected to have type x.ofLp i * 0 ≤ x.ofLp i * (0 * x.ofLp j)
**Adding simpa for simplification**
$ /bin/bash -lc 'lake env lean BootsRoyle/Spectral.lean' BootsRoyle/Spectral.lean:66:8: warning: automatically included section variable(s) unused in theorem `BootsRoyle.vectorAbs_apply`: [Fintype V] [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` BootsRoyle/Spectral.lean:69:8: warning: automatically included section variable(s) unused in theorem `BootsRoyle.norm_vectorAbs`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
**Analyzing spectral monotonicity conditions**
$ /bin/bash -lc 'lake env lean BootsRoyle/Spectral.lean' BootsRoyle/Spectral.lean:66:8: warning: automatically included section variable(s) unused in theorem `BootsRoyle.vectorAbs_apply`: [Fintype V] [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` BootsRoyle/Spectral.lean:69:8: warning: automatically included section variable(s) unused in theorem `BootsRoyle.norm_vectorAbs`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
**Planning strict quadratic proof approach** **Evaluating #check usage via lake env lean**
$ /bin/bash -lc "lake env lean BootsRoyle/Spectral.lean 2>&1 | sed -n '1,24p'"
Finset.sum_lt_sum.{u_1, u_4} {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [Preorder M] [IsOrderedCancelAddMonoid M]
{f g : ι → M} {s : Finset ι} [AddLeftStrictMono M] (hle : ∀ i ∈ s, f i ≤ g i) (hlt : ∃ i ∈ s, f i < g i) :
∑ i ∈ s, f i < ∑ i ∈ s, g i
BootsRoyle/Spectral.lean:68:8: warning: automatically included section variable(s) unused in theorem `BootsRoyle.vectorAbs_apply`:
[Fintype V]
[DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
omit [Fintype V] [DecidableEq V] in theorem ...
Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
BootsRoyle/Spectral.lean:71:8: warning: automatically included section variable(s) unused in theorem `BootsRoyle.norm_vectorAbs`:
[DecidableEq V]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
omit [DecidableEq V] in theorem ...
Note: This linter can be disabled with `set_option linter.unusedSectionVars false`**Refining strict lemma expansion with edge extraction** **Simplifying double summation with adjacency mask**
**Fixing inequality direction in proof**
$ /bin/bash -lc 'lake env lean BootsRoyle/Spectral.lean' BootsRoyle/Spectral.lean:66:8: warning: automatically included section variable(s) unused in theorem `BootsRoyle.vectorAbs_apply`: [Fintype V] [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` BootsRoyle/Spectral.lean:69:8: warning: automatically included section variable(s) unused in theorem `BootsRoyle.norm_vectorAbs`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` BootsRoyle/Spectral.lean:282:24: error: Type mismatch not_le.mpr ?m.33 has type ¬@LE.le ?m.27 LinearOrder.toPartialOrder.toLE ?m.29 ?m.30 but is expected to have type ¬@LE.le (SimpleGraph V) SimpleGraph.instLE H G
**Applying hGH.not_le theorem**
$ /bin/bash -lc 'lake env lean BootsRoyle/Spectral.lean' BootsRoyle/Spectral.lean:66:8: warning: automatically included section variable(s) unused in theorem `BootsRoyle.vectorAbs_apply`: [Fintype V] [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` BootsRoyle/Spectral.lean:69:8: warning: automatically included section variable(s) unused in theorem `BootsRoyle.norm_vectorAbs`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` BootsRoyle/Spectral.lean:282:28: error(lean.invalidField): Invalid field `not_le`: The environment does not contain `And.not_le`, so it is not possible to project the field `not_le` from an expression hGH of type `G.Adj ≤ H.Adj ∧ ¬H.Adj ≤ G.Adj` BootsRoyle/Spectral.lean:284:2: warning: `push_neg` has been deprecated. Prefer using `push Not` instead. If you'd rather continue using `push_neg` in your project, you can implement it as follows: ``` open Lean.Parser.Tactic in macro "push_neg" cfg:optConfig loc:(location)? : tactic => `(tactic| push $cfg:optConfig Not $[$loc]?) ```
**Identifying reducible SimpleGraph expression**
$ /bin/bash -lc 'lake env lean BootsRoyle/Spectral.lean' BootsRoyle/Spectral.lean:66:8: warning: automatically included section variable(s) unused in theorem `BootsRoyle.vectorAbs_apply`: [Fintype V] [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` BootsRoyle/Spectral.lean:69:8: warning: automatically included section variable(s) unused in theorem `BootsRoyle.norm_vectorAbs`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` BootsRoyle/Spectral.lean:284:2: warning: `push_neg` has been deprecated. Prefer using `push Not` instead. If you'd rather continue using `push_neg` in your project, you can implement it as follows: ``` open Lean.Parser.Tactic in macro "push_neg" cfg:optConfig loc:(location)? : tactic => `(tactic| push $cfg:optConfig Not $[$loc]?) ```
**Adding strict spectral theorem**
$ /bin/bash -lc 'lake env lean BootsRoyle/Spectral.lean' BootsRoyle/Spectral.lean:66:8: warning: automatically included section variable(s) unused in theorem `BootsRoyle.vectorAbs_apply`: [Fintype V] [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` BootsRoyle/Spectral.lean:69:8: warning: automatically included section variable(s) unused in theorem `BootsRoyle.norm_vectorAbs`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` BootsRoyle/Spectral.lean:284:2: warning: `push_neg` has been deprecated. Prefer using `push Not` instead. If you'd rather continue using `push_neg` in your project, you can implement it as follows: ``` open Lean.Parser.Tactic in macro "push_neg" cfg:optConfig loc:(location)? : tactic => `(tactic| push $cfg:optConfig Not $[$loc]?) ```
**Defining rotation system formalization** **Formulating planar embedding via rotation systems** **Planning planarity via minor exclusion**
$ /bin/bash -lc "rg -n \"def IsMinor|Minor|minor\" Mathlib/Combinatorics/SimpleGraph | sed -n '1,260p'; rg -n \"TopologicalMinor|IsSubdivision|subdivision\" Mathlib/Combinatorics/SimpleGraph | sed -n '1,220p'"
**Defining planarity via minor exclusion** **Formulating combinatorial planar triangulation** **Analyzing K33 nonplanarity challenges**
**Planning spherical triangulation formalization** **Implementing Perron eigenvalue identities**
**Identifying API errors**
$ /bin/bash -lc 'lake env lean BootsRoyle/Identities.lean' BootsRoyle/Identities.lean:1:0: error: unknown module prefix 'BootsRoyle' No directory 'BootsRoyle' or file 'BootsRoyle.olean' in the search path entries: /work/repro/.lake/packages/Cli/.lake/build/lib/lean /work/repro/.lake/packages/batteries/.lake/build/lib/lean /work/repro/.lake/packages/Qq/.lake/build/lib/lean /work/repro/.lake/packages/aesop/.lake/build/lib/lean /work/repro/.lake/packages/proofwidgets/.lake/build/lib/lean /work/repro/.lake/packages/importGraph/.lake/build/lib/lean /work/repro/.lake/packages/LeanSearchClient/.lake/build/lib/lean /work/repro/.lake/packages/plausible/.lake/build/lib/lean /work/repro/.lake/build/lib/lean /opt/elan/toolchains/leanprover--lean4---v4.33.0-rc1/lib/lean /opt/elan/toolchains/leanprover--lean4---v4.33.0-rc1/lib/lean
**Adding local library to lakefile imports**
**Verifying import priority between olean and source files**
$ /bin/bash -lc 'lake env lean BootsRoyle/Identities.lean' BootsRoyle/Identities.lean:1:0: error: unknown module prefix 'BootsRoyle' No directory 'BootsRoyle' or file 'BootsRoyle.olean' in the search path entries: /work/repro/.lake/packages/Cli/.lake/build/lib/lean /work/repro/.lake/packages/batteries/.lake/build/lib/lean /work/repro/.lake/packages/Qq/.lake/build/lib/lean /work/repro/.lake/packages/aesop/.lake/build/lib/lean /work/repro/.lake/packages/proofwidgets/.lake/build/lib/lean /work/repro/.lake/packages/importGraph/.lake/build/lib/lean /work/repro/.lake/packages/LeanSearchClient/.lake/build/lib/lean /work/repro/.lake/packages/plausible/.lake/build/lib/lean /work/repro/.lake/build/lib/lean /opt/elan/toolchains/leanprover--lean4---v4.33.0-rc1/lib/lean /opt/elan/toolchains/leanprover--lean4---v4.33.0-rc1/lib/lean
**Planning spectral build command**
$ /bin/bash -lc 'lake build BootsRoyle.Spectral' ⚠ [2727/2727] Built BootsRoyle.Spectral (7.0s) warning: BootsRoyle/Spectral.lean:66:8: automatically included section variable(s) unused in theorem `BootsRoyle.vectorAbs_apply`: [Fintype V] [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` warning: BootsRoyle/Spectral.lean:69:8: automatically included section variable(s) unused in theorem `BootsRoyle.norm_vectorAbs`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` warning: BootsRoyle/Spectral.lean:284:2: `push_neg` has been deprecated. Prefer using `push Not` instead. If you'd rather continue using `push_neg` in your project, you can implement it as follows: ``` open Lean.Parser.Tactic in macro "push_neg" cfg:optConfig loc:(location)? : tactic => `(tactic| push $cfg:optConfig Not $[$loc]?) ``` Build completed successfully (2727 jobs).
$ /bin/bash -lc 'lake env lean BootsRoyle/Identities.lean' BootsRoyle/Identities.lean:28:29: error(lean.synthInstanceFailed): failed to synthesize instance of type class Fintype ↑(G.neighborSet v) Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command. BootsRoyle/Identities.lean:35:16: error(lean.synthInstanceFailed): failed to synthesize instance of type class Fintype ↑(G.neighborSet v) Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command. BootsRoyle/Identities.lean:36:12: error(lean.synthInstanceFailed): failed to synthesize instance of type class Fintype ↑(G.neighborSet v) Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command. BootsRoyle/Identities.lean:56:21: error(lean.synthInstanceFailed): failed to synthesize instance of type class Fintype ↑(G.neighborSet v) Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command. BootsRoyle/Identities.lean:59:20: error(lean.synthInstanceFailed): failed to synthesize instance of type class Fintype ↑(G.neighborSet v) Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command. BootsRoyle/Identities.lean:63:14: error(lean.synthInstanceFailed): failed to synthesize instance of type class Fintype ↑(G.neighborSet v) Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command. BootsRoyle/Identities.lean:67:8: error(lean.synthInstanceFailed): failed to synthesize instance of type class DecidablePred fun w => w ≠ v ∧ ¬G.Adj v w Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command. BootsRoyle/Identities.lean:90:6: error: Tactic `rewrite` failed: Did not find an occurrence of the pattern P.lambda * P.x.ofLp ?v
**Deciding adjacency relation for neighborFinset** **Applying noncomputable def to remoteMass**
$ /bin/bash -lc 'lake env lean BootsRoyle/Identities.lean'
BootsRoyle/Identities.lean:31:2: error: Type mismatch: After simplification, term
Eq.symm h
has type
P.lambda * P.x.ofLp v =
∑
u ∈
@SimpleGraph.neighborFinset V G v
(@Subtype.fintype V (Membership.mem (G.neighborSet v))
(fun a => @SimpleGraph.neighborSet.memDecidable V G v (fun a b => Classical.propDecidable (G.Adj a b)) a)
inst✝²),
P.x.ofLp u
but is expected to have type
P.lambda * P.x.ofLp v =
∑
x ∈
@SimpleGraph.neighborFinset V G v
(@Subtype.fintype V (Membership.mem (G.neighborSet v))
(fun a => @SimpleGraph.neighborSet.memDecidable V G v inst✝ a) inst✝²),
P.x.ofLp x
BootsRoyle/Identities.lean:40:52: error: unsolved goals
V : Type u_1
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
P : PerronData G
v : V
a✝ : v ∈ Finset.univ
⊢ ∑ x ∈ G.neighborFinset v, P.x.ofLp x = ∑ x, if G.Adj v x then P.x.ofLp x else 0
BootsRoyle/Identities.lean:48:10: error: unsolved goals
V : Type u_1
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
P : PerronData G
w : V
a✝ : w ∈ Finset.univ
⊢ (∑ x, if G.Adj w x then P.x.ofLp w else 0) = ↑(G.degree w) * P.x.ofLp w
BootsRoyle/Identities.lean:43:16: warning: This simp argument is unused:
SimpleGraph.mem_neighborFinset
Hint: Omit it from the simp argument list.
[apply] simp
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
BootsRoyle/Identities.lean:50:18: warning: This simp argument is unused:
SimpleGraph.mem_neighborFinset
Hint: Omit it from the simp argument list.
[apply] simp [G.adj_comm]
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
BootsRoyle/Identities.lean:82:8: error: Tactic `rewrite` failed: Did not find an occurrence of the pattern
∑ x ∈ ?m.94, ?m.98 x
in the target expression
(P.x.ofLp v + ∑ x ∈ G.neighborFinset v, P.x.ofLp x + ∑ a, if a ≠ v ∧ ¬G.Adj v a then P.x.ofLp **Refactoring adjacency operator using explicit sums** **Simplifying eigenvector sum expressions**
$ /bin/bash -lc "rg -n \"neighborFinset_def|card_neighborFinset_eq_degree|mem_neighborFinset\" Mathlib/Combinatorics/SimpleGraph/Finite.lean | sed -n '1,120p'; sed -n '150,180p' Mathlib/Combinatorics/SimpleGraph/Finite.lean" 170:theorem neighborFinset_def : G.neighborFinset v = (G.neighborSet v).toFinset := 178:theorem mem_neighborFinset (w : V) : w ∈ G.neighborFinset v ↔ G.Adj v w := 208:theorem card_neighborFinset_eq_degree : #(G.neighborFinset v) = G.degree v := rfl 213:lemma degree_eq_zero : G.degree v = 0 ↔ G.IsIsolated v := by simp [← card_neighborFinset_eq_degree] 214:lemma degree_pos : 0 < G.degree v ↔ ¬ G.IsIsolated v := by simp [← card_neighborFinset_eq_degree] 221: simp only [degree, card_pos, Finset.Nonempty, mem_neighborFinset] 252: simp only [mem_neighborFinset] 561: simp only [Finset.ext_iff, mem_insert, mem_neighborFinset, IsUniversal] 575: · simp [← card_neighborFinset_eq_degree, (G.neighborFinset_eq_erase_univ v).mpr h] 651: rwa [← Set.toFinset_subset_toFinset, ← neighborFinset_def, ← inter_eq_left, 658: simp_rw [← card_neighborFinset_eq_degree, section FiniteAt /-! ## Finiteness at a vertex This section contains definitions and lemmas concerning vertices that have finitely many adjacent vertices. We denote this condition by `Fintype (G.neighborSet v)`. We define `G.neighborFinset v` to be the `Finset` version of `G.neighborSet v`. Use `neighborFinset_eq_filter` to rewrite this definition as a `Finset.filter` expression. -/ variable (v) [Fintype (G.neighborSet v)] /-- `G.neighborFinset v` is the `Finset` version of `G.neighborSet v` in case `G` is locally finite at `v`. -/ def neighborFinset : Finset V := (G.neighborSet v).toFinset theorem neighborFinset_def : G.neighborFinset v = (G.neighborSet v).toFinset := rfl @[simp, norm_cast] theorem coe_neighborFinset : (G.neighborFinset v : Set V) = G.neighborSet v := Set.coe_toFinset _ @[simp] theorem mem_neighborFinset (w : V) : w ∈ G.neighborFinset v ↔ G.Adj v w := Set.mem_toFinset
$ /bin/bash -lc 'rg -n "neighborFinset_eq_filter" Mathlib/Combinatorics/SimpleGraph/Finite.lean'
160:Use `neighborFinset_eq_filter` to rewrite this definition as a `Finset.filter` expression.
359:theorem neighborFinset_eq_filter {v : V} [DecidableRel G.Adj] :
370: simp_rw [degree, neighborFinset_eq_filter, top_adj, filter_ne]$ /bin/bash -lc "sed -n '350,365p' Mathlib/Combinatorics/SimpleGraph/Finite.lean"
section Finite
variable [Fintype V]
/-- `Fintype` for `neighborSet` -/
@[deprecated inferInstance (since := "2026-04-29")]
abbrev neighborSetFintype [DecidableRel G.Adj] (v : V) : Fintype (G.neighborSet v) :=
inferInstance
theorem neighborFinset_eq_filter {v : V} [DecidableRel G.Adj] :
G.neighborFinset v = ({w | G.Adj v w} : Finset _) := by ext; simp
theorem neighborFinset_compl [DecidableEq V] [DecidableRel G.Adj] (v : V) :
Gᶜ.neighborFinset v = (G.neighborFinset v)ᶜ \ {v} := by
simp only [neighborFinset, neighborSet_compl, Set.toFinset_sdiff, Set.toFinset_compl,
Set.toFinset_singleton]**Applying sum distributive rewriting** **Refactoring sum representation with ite expressions**
**Compiling codebase**
$ /bin/bash -lc 'lake env lean BootsRoyle/Identities.lean'
BootsRoyle/Identities.lean:32:19: error(lean.unknownIdentifier): Unknown constant `Matrix.dotProduct`
BootsRoyle/Identities.lean:31:2: error: Type mismatch: After simplification, term
Eq.symm h
has type
P.lambda * P.x.ofLp v = (fun j => if G.Adj v j then 1 else 0) ⬝ᵥ P.x.ofLp
but is expected to have type
P.lambda * P.x.ofLp v = ∑ x, if G.Adj v x then P.x.ofLp x else 0
BootsRoyle/Identities.lean:44:10: error: unsolved goals
V : Type u_1
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
P : PerronData G
w : V
a✝ : w ∈ Finset.univ
⊢ (∑ x, if G.Adj w x then P.x.ofLp w else 0) = ↑{w_1 | G.Adj w w_1}.card * P.x.ofLp w**Patching dotProduct and degree calculation**
$ /bin/bash -lc 'lake env lean BootsRoyle/Identities.lean'
BootsRoyle/Identities.lean:44:10: error: unsolved goals
V : Type u_1
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
P : PerronData G
w : V
a✝ : w ∈ Finset.univ
⊢ (∑ x, if G.Adj w x then P.x.ofLp w else 0) = ↑{w_1 | G.Adj w w_1}.card * P.x.ofLp w
BootsRoyle/Identities.lean:49:6: error: No goals to be solved**Patching proof with Finset.sum_filter rewrite**
$ /bin/bash -lc 'lake env lean BootsRoyle/Identities.lean'
**Defining cubic set and degree excess** **Proving pointwise degree identity**
$ /bin/bash -lc "rg -n \"sum_degree|degree_sum|sum.*degree|card.*Dart|two_mul.*edgeFinset|card_dart\" Mathlib/Combinatorics/SimpleGraph/Finite.lean Mathlib/Combinatorics/SimpleGraph | sed -n '1,200p'" Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean:393:theorem natCast_card_dart_eq_dotProduct [NonAssocSemiring α] : Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean:394: (Fintype.card G.Dart : α) = adjMatrix α G *ᵥ 1 ⬝ᵥ 1 := by Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean:395: simp [G.dart_card_eq_sum_degrees, dotProduct_one] Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean:110: dotProduct_mulVec_adjMatrix, ← sum_sub_distrib, degree_eq_sum_if_adj, sum_mul, ite_mul, one_mul, Mathlib/Combinatorics/SimpleGraph/Matching.lean:251: rw [← two_mul, ← M.coe.sum_degrees_eq_twice_card_edges] Mathlib/Combinatorics/SimpleGraph/FiveWheelLike.lean:256:private lemma sum_degree_le_of_le_not_adj [Fintype α] [DecidableEq α] [DecidableRel G.Adj] Mathlib/Combinatorics/SimpleGraph/FiveWheelLike.lean:373: have bdW := sum_degree_le_of_le_not_adj dXle (fun y _ ↦ one_le y) Mathlib/Combinatorics/SimpleGraph/FiveWheelLike.lean:384: have bdX := sum_degree_le_of_le_not_adj xcle (fun _ _ ↦ Nat.zero_le _) Mathlib/Combinatorics/SimpleGraph/FiveWheelLike.lean:388: -- The sum of the degree sum over `W` and twice the degree sum over `s ∩ t` Mathlib/Combinatorics/SimpleGraph/CompleteMultipartite.lean:304: rw [← mul_right_inj' two_ne_zero, ← sum_degrees_eq_twice_card_edges] Mathlib/Combinatorics/SimpleGraph/Bipartite.lean:37:* `SimpleGraph.isBipartiteWith_sum_degrees_eq` is the proof that if `G.IsBipartiteWith s t`, then Mathlib/Combinatorics/SimpleGraph/Bipartite.lean:38: the sum of the degrees of the vertices in `s` is equal to the sum of the degrees of the vertices Mathlib/Combinatorics/SimpleGraph/Bipartite.lean:41:* `SimpleGraph.isBipartiteWith_sum_degrees_eq_card_edges` is the proof that if Mathlib/Combinatorics/SimpleGraph/Bipartite.lean:42: `G.IsBipartiteWith s t`, then sum of the degrees of the vertices in `s` is equal to the number of Mathlib/Combinatorics/SimpleGraph/Bipartite.lean:45: See `SimpleGraph.sum_degrees_eq_twice_card_edges` for the general version, and Mathlib/Co
**Importing DegreeSum and patching lemmas**
**Compiling spectral build**
$ /bin/bash -lc 'lake env lean BootsRoyle/Identities.lean' BootsRoyle/Identities.lean:69:8: error: Invalid field notation: Function `cubicVertices` does not have a usable parameter of type `PerronData ...` for which to substitute `P` Note: Such a parameter must be explicit, or implicit with a unique name, to be used by field notation BootsRoyle/Identities.lean:77:8: error: Invalid field notation: Function `degreeExcess` does not have a usable parameter of type `PerronData ...` for which to substitute `P` Note: Such a parameter must be explicit, or implicit with a unique name, to be used by field notation BootsRoyle/Identities.lean:81:19: error: Invalid field notation: Function `degreeExcess` does not have a usable parameter of type `PerronData ...` for which to substitute `P` Note: Such a parameter must be explicit, or implicit with a unique name, to be used by field notation BootsRoyle/Identities.lean:84:2: error: unsolved goals case pos V : Type u_1 inst✝² : Fintype V inst✝¹ : DecidableEq V G : SimpleGraph V inst✝ : DecidableRel G.Adj P : PerronData G hmin : ∀ (v : V), 3 ≤ G.degree v v : V hv : G.degree v = 3 ⊢ 3 * P.x.ofLp v = 4 * P.x.ofLp v + sorry () * P.x.ofLp v - P.x.ofLp v BootsRoyle/Identities.lean:85:36: error: omega could not prove the goal: a possible counterexample may satisfy the constraints 0 ≤ a ≤ 2 where a := ↑(G.degree v) BootsRoyle/Identities.lean:86:8: error: Failed to rewrite using equation theorems for `degreeExcess` BootsRoyle/Identities.lean:84:14: warning: This simp argument is unused: degreeExcess Hint: Omit it from the simp argument list. [apply] simp [hv] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` BootsRoyle/Identities.lean:97:27: error: Invalid field notation: Function `degreeExcess` does not have a usable parameter of type `PerronData ...` for which to substitute `P` Note: Such a parameter must be explicit, or implicit with a unique name, to be used by field notation BootsRoyle/Identities.lean:109:23: error: Failed to rewrite using equation theo
**Correcting function dependencies and notations**
**Confirming implicit parameter inference**
$ /bin/bash -lc 'lake env lean BootsRoyle/Identities.lean' BootsRoyle/Identities.lean:84:2: error: unsolved goals case pos V : Type u_1 inst✝² : Fintype V inst✝¹ : DecidableEq V G : SimpleGraph V inst✝ : DecidableRel G.Adj P : PerronData G hmin : ∀ (v : V), 3 ≤ G.degree v v : V hv : G.degree v = 3 ⊢ 3 * P.x.ofLp v = 4 * P.x.ofLp v - P.x.ofLp v
$ /bin/bash -lc 'lake env lean BootsRoyle/Identities.lean' BootsRoyle/Identities.lean:85:4: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
**Proving degree excess sum identity** **Proving degree sum with casts**
**Compiling codebase**
$ /bin/bash -lc 'lake env lean BootsRoyle/Identities.lean' BootsRoyle/Identities.lean:89:4: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` BootsRoyle/Identities.lean:118:0: warning: automatically included section variable(s) unused in theorem `BootsRoyle.PerronData.degreeExcess_cast_eq`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` BootsRoyle/Identities.lean:134:38: error: Invalid field notation: Function `cubicCount` does not have a usable parameter of type `PerronData ...` for which to substitute `P` Note: Such a parameter must be explicit, or implicit with a unique name, to be used by field notation BootsRoyle/Identities.lean:151:40: error(lean.unknownIdentifier): Unknown identifier `P.cubicCount` BootsRoyle/Identities.lean:145:39: error(lean.unknownIdentifier): Unknown identifier `P` BootsRoyle/Identities.lean:155:13: error(lean.unknownIdentifier): Unknown identifier `P.cubicCount` BootsRoyle/Identities.lean:156:12: error: Failed to rewrite using equation theorems for `cubicCount`
**Patching cubicCount call to exclude P**
$ /bin/bash -lc 'lake env lean BootsRoyle/Identities.lean' BootsRoyle/Identities.lean:89:4: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` BootsRoyle/Identities.lean:118:0: warning: automatically included section variable(s) unused in theorem `BootsRoyle.PerronData.degreeExcess_cast_eq`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
**Defining graph subtype for completion** **Exploring K33Free graph embedding**
$ /bin/bash -lc "rg -n \"completeBipartiteGraph|CompleteBipartite\" Mathlib/Combinatorics/SimpleGraph | sed -n '1,220p'; rg -n \"def induce|induce_adj|Induce\" Mathlib/Combinatorics/SimpleGraph/Basic.lean Mathlib/Combinatorics/SimpleGraph | head -100; rg -n \"maxDegree.*two|degree_le_two|IsPathGraph|connected.*pathGraph|Acyclic.*degree\" Mathlib/Combinatorics/SimpleGraph | sed -n '1,240p'"
Mathlib/Combinatorics/SimpleGraph/Coloring/Vertex.lean:529:def CompleteBipartiteGraph.bicoloring (V W : Type*) : (completeBipartiteGraph V W).Coloring Bool :=
Mathlib/Combinatorics/SimpleGraph/Coloring/Vertex.lean:535:theorem CompleteBipartiteGraph.chromaticNumber {V W : Type*} [Nonempty V] [Nonempty W] :
Mathlib/Combinatorics/SimpleGraph/Coloring/Vertex.lean:536: (completeBipartiteGraph V W).chromaticNumber = 2 := by
Mathlib/Combinatorics/SimpleGraph/Coloring/Vertex.lean:538: (by simpa using (CompleteBipartiteGraph.bicoloring V W).colorable)]
Mathlib/Combinatorics/SimpleGraph/Coloring/Vertex.lean:542: have h : (completeBipartiteGraph V W).Adj (Sum.inl v) (Sum.inr w) := by simp
Mathlib/Combinatorics/SimpleGraph/Extremal/Zarankiewicz.lean:30:number of edges in a `completeBipartiteGraph (Fin s) (Fin t)`-free bipartite graph with parts of
Mathlib/Combinatorics/SimpleGraph/Extremal/Zarankiewicz.lean:36: sup { G : SimpleGraph (Fin m ⊕ Fin n) | G ≤ completeBipartiteGraph (Fin m) (Fin n)
Mathlib/Combinatorics/SimpleGraph/Extremal/Zarankiewicz.lean:37: ∧ (completeBipartiteGraph (Fin s) (Fin t)).Free G} (#·.edgeFinset)
Mathlib/Combinatorics/SimpleGraph/Extremal/Zarankiewicz.lean:45: sup { G : SimpleGraph (V ⊕ W) | G ≤ completeBipartiteGraph V W
Mathlib/Combinatorics/SimpleGraph/Extremal/Zarankiewicz.lean:46: ∧ (completeBipartiteGraph α β).Free G} (#·.edgeFinset) := by
Mathlib/Combinatorics/SimpleGraph/Extremal/Zarankiewicz.lean:47: let e₁ := completeBipartiteGraphCongr
Mathlib/Combinatorics/SimpleGraph/Extremal/Zarankiewicz.lean:49: let K := completeBipartiteGraph (Fin s) (Fin t)
Mathlib/Combinatorics/SimpleGraph/Extremal/Zarankiewicz.lean:50: let e₂ := completeBipartiteGraphCongr
Mathlib/Combinatorics/SimpleGraph/Extremal/Zarankiewicz.lean:56: let K := completeBipartiteGraph α β
Mathlib/Combinatorics/SimpleGraph/Extremal/Zarankiewicz.lean:63: G ≤ completeBipartiteGraph _ _ ∧ K.Free G := by
Mathlib/Combinatorics/SimpleGraph/Extremal/Zarank**Defining K33-free subgraph property** **Planning max degree bounded proof**
$ /bin/bash -lc "rg -n \"Acyclic.*card.*edge|card.*edge.*Acyclic|acyclic.*connected|IsTree.*card|card_edges.*card_verts|edgeFinset.card.*Fintype.card\" Mathlib/Combinatorics/SimpleGraph/Acyclic.lean Mathlib/Combinatorics/SimpleGraph | sed -n '1,280p'; rg -n \"maxDegree|degree.*≤ 2|degree_le.*2|IsPath.*Hamiltonian|Hamiltonian.*pathGraph|isPath.*support_eq\" Mathlib/Combinatorics/SimpleGraph | sed -n '1,260p'" Mathlib/Combinatorics/SimpleGraph/Acyclic.lean:298:lemma IsTree.card_edgeFinset [Fintype V] [Fintype G.edgeSet] (hG : G.IsTree) : Mathlib/Combinatorics/SimpleGraph/Acyclic.lean:459:/-- Every acyclic subgraph of a connected graph can be extended to a spanning tree. -/ Mathlib/Combinatorics/SimpleGraph/Acyclic.lean:484: G.IsTree ↔ G.Connected ∧ Nat.card G.edgeSet + 1 = Nat.card V := by Mathlib/Combinatorics/SimpleGraph/Acyclic.lean:298:lemma IsTree.card_edgeFinset [Fintype V] [Fintype G.edgeSet] (hG : G.IsTree) : Mathlib/Combinatorics/SimpleGraph/Acyclic.lean:459:/-- Every acyclic subgraph of a connected graph can be extended to a spanning tree. -/ Mathlib/Combinatorics/SimpleGraph/Acyclic.lean:484: G.IsTree ↔ G.Connected ∧ Nat.card G.edgeSet + 1 = Nat.card V := by Mathlib/Combinatorics/SimpleGraph/Finite.lean:122:theorem edgeFinset_card : #G.edgeFinset = Fintype.card G.edgeSet := Mathlib/Combinatorics/SimpleGraph/Finite.lean:434:The key properties of this are given in `exists_maximal_degree_vertex`, `degree_le_maxDegree` Mathlib/Combinatorics/SimpleGraph/Finite.lean:435:and `maxDegree_le_of_forall_degree_le`. -/ Mathlib/Combinatorics/SimpleGraph/Finite.lean:436:def maxDegree [DecidableRel G.Adj] : ℕ := Mathlib/Combinatorics/SimpleGraph/Finite.lean:442: ∃ v, G.maxDegree = G.degree v := by Mathlib/Combinatorics/SimpleGraph/Finite.lean:443: grind [maxDegree, WithBot.unbotD_coe, max_mem_image_coe <| univ_nonempty.image (G.degree ·)] Mathlib/Combinatorics/SimpleGraph/Finite.lean:446:theorem degree_le_maxDegree [DecidableRel G.Adj] (v : V) : G.degree v ≤ G.maxDegree := Mathlib/Combinatorics/SimpleGraph/Finite.lean:450:lemma maxDegree_of_subsingleton [DecidableRel G.Adj] [Subsingleton V] : G.maxDegree = 0 := by Mathlib/Combinatorics/SimpleGraph/Finite.lean:452: simp [maxDegree, Finset.image_const] Mathlib/Combinatorics/SimpleGraph/Finite.lean:454:@[deprecated (since := "2026-06-15")] alias maxDegree_of_isEmpty := maxDegree_of_subsingleton Mathlib/Combinatorics/
**Inspecting acyclic file line equivalence**
$ /bin/bash -lc "sed -n '270,315p' Mathlib/Combinatorics/SimpleGraph/Acyclic.lean; sed -n '470,495p' Mathlib/Combinatorics/SimpleGraph/Acyclic.lean; rg -n \"def IsTree|isTree_iff\" Mathlib/Combinatorics/SimpleGraph/Acyclic.lean | head -60"
classical
refine ⟨fun h ↦ (edges_nodup_of_support_nodup <| p.isPath_def.mp h).isChain, fun h ↦ ?_⟩
induction p with
| nil => simp
| @cons u' v' _ head tail ih =>
have hcc := List.isChain_cons.mp (edges_cons _ _ ▸ h)
refine cons_isPath_iff head tail |>.mpr ⟨ih hcc.2, ?_⟩
rcases tail.length.eq_zero_or_pos with h' | h'
· simp [nil_iff_support_eq.mp (length_eq_zero_iff.mp h'), head.ne]
· by_contra hh
apply hG <| cons head (tail.takeUntil u' hh)
simp only [isCycle_def, isTrail_def, edges_cons, List.nodup_cons, ne_eq, reduceCtorEq,
not_false_eq_true, support_cons, List.tail_cons, true_and]
have : cons head (tail.takeUntil u' hh) |>.support.tail.Nodup :=
tail.isPath_def.mp (ih hcc.2) |>.sublist <| List.IsInfix.sublist
⟨[], (tail.dropUntil u' hh).support.tail, by simp [← support_append]⟩
refine ⟨⟨?_, edges_nodup_of_support_nodup this⟩, this⟩
by_contra hhh
refine hcc.1 s(u', v') ?_ rfl
rw [← tail.cons_tail_eq (by simp [not_nil_iff_lt_length, h'])]
have := IsPath.mk' this |>.eq_snd_of_mem_edges (Sym2.eq_swap ▸ hhh)
simp [this, snd_takeUntil head.ne]
theorem IsAcyclic.isPath_iff_isTrail (hG : G.IsAcyclic) {v w : V} (p : G.Walk v w) :
p.IsPath ↔ p.IsTrail :=
⟨IsPath.isTrail, fun h ↦ hG.isPath_iff_isChain p |>.mpr <| p.isTrail_def.mp h |>.isChain⟩
set_option backward.isDefEq.respectTransparency.types false in
lemma IsTree.card_edgeFinset [Fintype V] [Fintype G.edgeSet] (hG : G.IsTree) :
Finset.card G.edgeFinset + 1 = Fintype.card V := by
have := hG.connected.nonempty
inhabit V
classical
have : Finset.card ({default} : Finset V)ᶜ + 1 = Fintype.card V := by
rw [Finset.card_compl, Finset.card_singleton, Nat.sub_add_cancel Fintype.card_pos]
rw [← this, add_left_inj]
choose f hf hf' using (hG.existsUnique_path · default)
refine Eq.symm <| Finset.card_bij
(fun w hw => ((f w).firstDart <| ?notNil).edge)
(fun a ha => ?memEdges) ?in**Verifying tree equivalence theorem**
$ /bin/bash -lc "rg -n \"IsAcyclic.*card|card.*IsAcyclic|edgeSet.*<.*card|card_edge.*acyclic|card_vert.*IsAcyclic\" Mathlib/Combinatorics/SimpleGraph/Acyclic.lean | sed -n '1,160p'" 143:theorem IsAcyclic.of_card_le_two (h : ENat.card V ≤ 2) : G.IsAcyclic := by
**Planning planar graph tooling installation**
$ /bin/bash -lc 'python3 -m pip --version || true' /usr/bin/python3: No module named pip
**Formalizing arithmetic optimization lemmas** **Deriving bounds via field division and nlinarith**
**Formalizing generic theorem assumptions**
**Compiling codebase**
$ /bin/bash -lc 'lake env lean BootsRoyle/Arithmetic.lean'
BootsRoyle/Arithmetic.lean:49:34: warning: Variable name `hn` is not explicitly referenced.
Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
[apply] _hn
Note: This linter can be disabled with `set_option linter.unusedVariables false`
BootsRoyle/Arithmetic.lean:150:4: error: Type mismatch
hs
has type
(t + 1) * s ≤ A
but is expected to have type
s * (t + 1) ≤ A
Try this:
[apply] ring_nf
The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
BootsRoyle/Arithmetic.lean:164:43: error: unsolved goals
t B : ℝ
ht : 2 < t
hden : 3 * t - 2 ≠ 0
⊢ B * t * (-2 + t * 3)⁻¹ * 3 - B * (-2 + t * 3)⁻¹ * 2 = B**Patching field_simp denominator handling**
$ /bin/bash -lc 'lake env lean BootsRoyle/Arithmetic.lean'
BootsRoyle/Arithmetic.lean:49:34: warning: Variable name `hn` is not explicitly referenced.
Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
[apply] _hn
Note: This linter can be disabled with `set_option linter.unusedVariables false`
Try this:
[apply] ring_nf
The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
BootsRoyle/Arithmetic.lean:164:43: error: unsolved goals
t B : ℝ
ht : 2 < t
hden : 3 * t - 2 ≠ 0
hden' : -2 + t * 3 ≠ 0
⊢ B * t * (-2 + t * 3)⁻¹ * 3 - B * (-2 + t * 3)⁻¹ * 2 = B**Tracing denominator simplification issue** **Simplifying expression using inverse property**
$ /bin/bash -lc 'lake env lean BootsRoyle/Arithmetic.lean' BootsRoyle/Arithmetic.lean:49:34: warning: Variable name `hn` is not explicitly referenced. Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning: [apply] _hn Note: This linter can be disabled with `set_option linter.unusedVariables false`
**Formalizing abstract face averaging lemma** **Deriving inequality conditions for L**
**Compiling codebase**
$ /bin/bash -lc 'lake env lean BootsRoyle/Arithmetic.lean' BootsRoyle/Arithmetic.lean:49:34: warning: Variable name `hn` is not explicitly referenced. Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning: [apply] _hn Note: This linter can be disabled with `set_option linter.unusedVariables false` BootsRoyle/Arithmetic.lean:190:8: error: Tactic `rewrite` failed: Did not find an occurrence of the pattern ?m.130 / F ≤ ?m.132 / K in the target expression K * (lam - (lam + 3) * L) ≤ F * (lam * L) lam L K F : ℝ hlam : 0 < lam hK : 0 < K hF : 0 < F haverage : lam * L / K ≥ (lam - (lam + 3) * L) / F D : ℝ := F + K + 3 * K / lam hD : 0 < D ⊢ K * (lam - (lam + 3) * L) ≤ F * (lam * L)
**Deriving inequality using div_le_div_iff₀ theorem**
$ /bin/bash -lc 'lake env lean BootsRoyle/Arithmetic.lean' BootsRoyle/Arithmetic.lean:49:34: warning: Variable name `hn` is not explicitly referenced. Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning: [apply] _hn Note: This linter can be disabled with `set_option linter.unusedVariables false`
**Planning planar map approach**
**Evaluating planarity hypothesis approach** **Planning finite enumeration tooling**
**Planning Debian package download for plantri**
A second tooling pass confirms this is not a missed import: current Lean/mathlib has no planarity definition, and even recent Lean graph-theory discussion treats the rotation-system/Jordan-curve bridge as an open formalization gap. I’m also testing the paper’s delegated finite computation independently with a standalone planar-triangulation generator; this can audit the \(n\le14\) claim, though it cannot by itself become a kernel proof without a formally verified completeness checker.
$ /bin/bash -lc 'apt-get download plantri' E: Unable to locate package plantri
**Planning manual package installation**
$ /bin/bash -lc "apt-cache policy gcc clang tcc | sed -n '1,120p'; apt-cache search '"'^tcc$'"' | sed -n '1,40p'"
**Planning Zig and Plantri download sources**
The spectral core is now kernel-checked: I built the missing Perron–Frobenius/Rayleigh layer for simple graphs, including a strictly positive Perron vector for connected graphs and strict spectral monotonicity, plus the paper’s global eigenvector identities and several scalar certificates. I’m now testing the remaining credible escape routes: an independent finite-range enumeration and whether a trustworthy combinatorial-map planarity bridge can be assembled without smuggling the theorem into a hypothesis.
**Inspecting current files and status**
$ /bin/bash -lc "git status --short && rg -n \"sorry|axiom|admit\" BootsRoyle lakefile.lean || true && command -v leanc || true && find /opt/elan -type f \\( -name leanc -o -name 'clang*' -o -name 'gcc*' \\) 2>/dev/null | head -30" M lakefile.lean ?? BootsRoyle/ /opt/elan/bin/leanc /opt/elan/toolchains/leanprover--lean4---v4.33.0-rc1/lib/clang/22/lib/x86_64-unknown-linux-gnu/clang_rt.crtend.o /opt/elan/toolchains/leanprover--lean4---v4.33.0-rc1/lib/clang/22/lib/x86_64-unknown-linux-gnu/clang_rt.crtbegin.o /opt/elan/toolchains/leanprover--lean4---v4.33.0-rc1/bin/clang /opt/elan/toolchains/leanprover--lean4---v4.33.0-rc1/bin/leanc /opt/elan/bin/leanc
**Downloading plantri tool**
$ /bin/bash -lc 'curl -L --fail --silent --show-error https://users.cecs.anu.edu.au/~bdm/plantri/plantri58.tar.gz -o /tmp/plantri58.tar.gz && tar -tzf /tmp/plantri58.tar.gz | head -30' plantri58/ plantri58/faceorbits.c plantri58/sumlines.c plantri58/more-counts.txt plantri58/degseq.c plantri58/nft.c plantri58/maxdeg.c plantri58/fullgen.c plantri58/rng.c plantri58/LICENSE-2.0.txt plantri58/plantri-guide.txt plantri58/rng.h plantri58/allowed_deg.c plantri58/mdcount.c plantri58/makefile plantri58/adj4.c plantri58/fullgen-guide.txt plantri58/plantri.c
**Extracting and compiling Clang**
$ /bin/bash -lc 'tmpdir=$(mktemp -d /tmp/boots-plantri.XXXXXX) && tar -xzf /tmp/plantri58.tar.gz -C "$tmpdir" && /opt/elan/toolchains/leanprover--lean4---v4.33.0-rc1/bin/clang -O3 -o "$tmpdir/plantri58/plantri" "$tmpdir/plantri58/plantri.c" && "$tmpdir/plantri58/plantri" -help 2>&1 | head -40 && echo "$tmpdir"' tar: plantri58/faceorbits.c: Cannot change ownership to uid 3106, gid 3106: Invalid argument tar: plantri58/sumlines.c: Cannot change ownership to uid 3106, gid 3106: Invalid argument tar: plantri58/more-counts.txt: Cannot change ownership to uid 3106, gid 3106: Invalid argument tar: plantri58/degseq.c: Cannot change ownership to uid 3106, gid 3106: Invalid argument tar: plantri58/nft.c: Cannot change ownership to uid 3106, gid 3106: Invalid argument tar: plantri58/maxdeg.c: Cannot change ownership to uid 3106, gid 3106: Invalid argument tar: plantri58/fullgen.c: Cannot change ownership to uid 3106, gid 3106: Invalid argument tar: plantri58/rng.c: Cannot change ownership to uid 3106, gid 3106: Invalid argument tar: plantri58/LICENSE-2.0.txt: Cannot change ownership to uid 3106, gid 3106: Invalid argument tar: plantri58/plantri-guide.txt: Cannot change ownership to uid 3106, gid 3106: Invalid argument tar: plantri58/rng.h: Cannot change ownership to uid 3106, gid 3106: Invalid argument tar: plantri58/allowed_deg.c: Cannot change ownership to uid 3106, gid 3106: Invalid argument tar: plantri58/mdcount.c: Cannot change ownership to uid 3106, gid 3106: Invalid argument tar: plantri58/makefile: Cannot change ownership to uid 3106, gid 3106: Invalid argument tar: plantri58/adj4.c: Cannot change ownership to uid 3106, gid 3106: Invalid argument tar: plantri58/fullgen-guide.txt: Cannot change ownership to uid 3106, gid 3106: Invalid argument tar: plantri58/plantri.c: Cannot change ownership to uid 3106, gid 3106: Invalid argument tar: plantri58: Cannot change ownership to uid 3106, gid 3106: Invalid argument tar: Exiting with failure status due to previous errors
**Specifying tar no-same-owner option**
$ /bin/bash -lc 'tmpdir=$(mktemp -d /tmp/boots-plantri.XXXXXX) && tar --no-same-owner -xzf /tmp/plantri58.tar.gz -C "$tmpdir" && /opt/elan/toolchains/leanprover--lean4---v4.33.0-rc1/bin/clang -O3 -o "$tmpdir/plantri58/plantri" "$tmpdir/plantri58/plantri.c" && "$tmpdir/plantri58/plantri" -help 2>&1 | head -50 && echo "$tmpdir"'
/tmp/boots-plantri.DYzeII/plantri58/plantri.c:240:10: fatal error: 'stdio.h' file not found
240 | #include <stdio.h>
| ^~~~~~~~~
1 error generated.**Planning Zig compiler download**
**Confirming successful file download**
$ /bin/bash -lc 'curl -L --fail --silent --show-error https://ziglang.org/download/0.14.1/zig-x86_64-linux-0.14.1.tar.xz -o /tmp/zig-x86_64-linux-0.14.1.tar.xz && tar --no-same-owner -xJf /tmp/zig-x86_64-linux-0.14.1.tar.xz -C /tmp && /tmp/zig-x86_64-linux-0.14.1/zig version' 0.14.1
**Locating temporary directories**
$ /bin/bash -lc 'plantri_dir=$(find /tmp -maxdepth 2 -type d -path '"'*/plantri58' | tail -1) && /tmp/zig-x86_64-linux-0.14.1/zig cc -O3 -o \""'$plantri_dir/plantri" "$plantri_dir/plantri.c" && "$plantri_dir/plantri" -help 2>&1 | head -60 && echo "$plantri_dir"' error: ReadOnlyFileSystem
**Specifying custom Zig cache directory**
$ /bin/bash -lc 'plantri_dir=$(find /tmp -maxdepth 2 -type d -path '"'*/plantri58' | tail -1) && export ZIG_GLOBAL_CACHE_DIR=/tmp/boots-zig-global ZIG_LOCAL_CACHE_DIR=/tmp/boots-zig-local && /tmp/zig-x86_64-linux-0.14.1/zig cc -O3 -o \""'$plantri_dir/plantri" "$plantri_dir/plantri.c" && "$plantri_dir/plantri" -help 2>&1 | head -60 && echo "$plantri_dir"' Plantri version 5.8 - March 4, 2026 Usage: /tmp/boots-plantri.HxHvH4/plantri58/plantri [-uagsETh -Ac#txm#P#bpe#f#qQKCw -odGVX -v] n [res/mod] [outfile] See plantri-guide.txt for more information. /tmp/boots-plantri.HxHvH4/plantri58
**Planning enumeration of maximal planar triangulations**
$ /bin/bash -lc 'plantri_dir=$(find /tmp -maxdepth 2 -type d -path '"'*/plantri58' | tail -1) && rg -n \"graph6|triangulations|default|minimum degree|-g\" \""'$plantri_dir/plantri-guide.txt" | head -80' 212: triangulations with 16 vertices. In other words, it makes the 216: example). For triangulations and quadradrangulations (only) you can 218: which means 16/2+2=10 vertices for triangulations or 16+2=18 vertices 241: plantri 20 tri.20 --Send 20-vertex triangulations to file tri.20 261: PLANAR CODE is the default format. It is the preferred format if you plan 293: graphs. graph6 is one of the formats supported by Brendan McKay's 295: To select graph6 code use -g. 307: format header written by default? 311: graph6 >>graph6<< no 315: it (for portability reasons). To write a header when the default is not 328: -m4 (minimum degree at least 4) refers to the original graph and 333: Since graph6 and sparse6 formats don't encode the embedding anyway, 334: this switch is ignored for output purposes if you use -g or -s. 362: -m# Specify a lower bound on the minimum degree. In the dual graph this 363: means a lower bound on the minimum face size. The default is -m3. 366: graph will be explained in each case. The default is -c3. 375: Select eulerian triangulations, where "eulerian" means that every 376: vertex has even degree. -m is not available except for the default 377: -m4 (the minimum degree is always 4 anyway). 379: -c3 (default) 3-connected eulerian plane triangulation. 386: eulerian plane triangulations which have a triangle that is 396: -m1 The minimum degree is at least 1. 397: -m2 The minimum degree is at least 2. 398: -m3 (default) The minimum degree is a least 3. 399: -m4 The minimum degree is at least 4. 400: -m5 The minimum degree is at least 5 (and so exactly 5). 403: -c3 (default) The connectivity is at least 3. 409: If the -c switch is used but not the -m switch, the minimum degree is 419: number of edges in the dual). The default is no bounds. 4
**Planning graph6 reading and spectral audit** **Planning exception graph identification**
$ /bin/bash -lc 'rg -n -C 8 "Figure 2|n = 7|n=7|seven|exception" /work/paper.txt | head -100'
48-Foundation of China (No. 12371350) and Fundamental Research Funds for the Central Universities, Nankai
49-University (No. 63243151).
50-‡
51-School of Mathematical Sciences, Anhui University, Hefei 230601, P.R. China. E-mail: wangy@ahu.edu.cn (Y.
52-Wang). Supported by the National Natural Science Foundation of China (No. 12171002, 12331012)
53-
54-1
55-
56: the conjectured fan is extremal for every n ≥ 2, with n = 6 as the unique exception. The proof
57-p
58-is with aid of a result of Shu and Hong [14], which states that λ(G) ≤ 3/2 + n − 7/4. Thus,
59-the outerplanar spectral extremal problem is now completely understood.
60-The second and more difficult conjecture is about planar graphs. Motivated in part by the
61-use of the spectral radius as a measure of the connectivity of planar networks, Boots and Royle [2]
62-conjectured in 1991 that, for every n ≥ 9, the unique planar graph of order n with maximum
63-spectral radius is K2 ∨ Pn−2 . The same conjecture was proposed independently by Cao and
64-Vince [3].
--
80-planar conjecture holds for sufficiently large n; however, that manuscript never appeared in
81-published form (see also the introduction of Tait and Tobin [15]). In 2017, Tait and Tobin [15]
82-proved that K2 ∨ Pn−2 is indeed the unique planar graph of maximum spectral radius whenever
83-n is sufficiently large.
84-The original conjecture was formulated for n ≥ 9. The purpose of this paper is to give a
85-complete proof of the conjecture.
86-Theorem 1.1. For every n ≥ 3, except for n ∈ {7, 8}, the graph K2 ∨ Pn−2 is the unique planar
87-graph on n vertices with maximum adjacency spectral radius. For n ∈ {7, 8}, the extremal graphs
88:are the exceptional graphs shown in Figure 2.
89-
90:(a) n = 7
91-
92-(b) n = 8
93-
94:Figure 2: The planar graphs with maximum spectral radius for n = 7, 8
95-
96-The corresponding problem for graphs embeddable on surfaces of arbitrary genus provides
97-a broader setting for these results. Let spex(n, γ) denote the max**Designing graph6 parser and spectral analyzer**
**Preparing sequential n4-14 shell test**
$ /bin/bash -lc 'plantri_dir=$(find /tmp -maxdepth 2 -type d -path '"'*/plantri58' | tail -1); \""'$plantri_dir/plantri" -g 7 /tmp/tri7.g6 >/tmp/tri7.log 2>&1; python3 tools/check_finite.py 7 /tmp/tri7.g6; cat /tmp/tri7.log' n=7 count=5 target=4.504664353588 1: radius=4.511404664227 delta=+6.740310638712e-03 degrees=[6, 5, 5, 5, 3, 3, 3] graph6=b'F~f]G' 2: radius=4.504664353588 delta=+0.000000000000e+00 degrees=[6, 6, 4, 4, 4, 3, 3] graph6=b'F~e]g' 3: radius=4.475122250239 delta=-2.954210334920e-02 degrees=[6, 5, 5, 4, 4, 3, 3] graph6=b'F|nmG' /tmp/boots-plantri.HxHvH4/plantri58/plantri -g 7 /tmp/tri7.g6 5 triangulations written to /tmp/tri7.g6; cpu=0.00 sec
$ /bin/bash -lc 'plantri_dir=$(find /tmp -maxdepth 2 -type d -path '"'*/plantri58' | tail -1); \""'$plantri_dir/plantri" -g 8 /tmp/tri8.g6 >/tmp/tri8.log 2>&1; python3 tools/check_finite.py 8 /tmp/tri8.g6; cat /tmp/tri8.log' n=8 count=14 target=4.838537617035 1: radius=4.854101966250 delta=+1.556434921503e-02 degrees=[6, 6, 6, 6, 3, 3, 3, 3] graph6=b'G~f]Ig' 2: radius=4.838537617035 delta=+0.000000000000e+00 degrees=[7, 7, 4, 4, 4, 4, 3, 3] graph6=b'G|}K]S' 3: radius=4.821583421593 delta=-1.695419544211e-02 degrees=[7, 6, 5, 5, 4, 3, 3, 3] graph6=b'G|mN]C' /tmp/boots-plantri.HxHvH4/plantri58/plantri -g 8 /tmp/tri8.g6 14 triangulations written to /tmp/tri8.g6; cpu=0.00 sec
**Planning loop generation with tty command**
The independent enumeration has already corroborated the paper’s two exceptions: at \(n=7\) the reported non-fan triangulation wins by about \(0.00674\), and at \(n=8\) the non-fan wins by about \(0.01556\). For every triangulation through \(n=13\), the fan-like \(K_2\vee P_{n-2}\) is uniquely first when it should be; the \(n=14\) run is still finishing. This is useful correctness evidence, but I am keeping it explicitly separate from the Lean theorem because plantri’s completeness is not a kernel-checked proof.**Optimizing power iteration convergence**
**Planning script optimization**
$ /bin/bash -lc 'plantri_dir=$(find /tmp -maxdepth 2 -type d -path '"'*/plantri58' | tail -1); for n in 9 10 11 12 13 14; do \""'$plantri_dir/plantri" -g "$n" "/tmp/tri${n}.g6" >/tmp/plantri-current.log 2>&1; python3 tools/check_finite.py "$n" "/tmp/tri${n}.g6"; done'
n=10 count=233 target=5.411801176471
1: radius=5.411801176471 delta=+0.000000000000e+00 degrees=[9, 9, 4, 4, 4, 4, 4, 4, 3, 3] graph6=b'I~e[kePsG'
2: radius=5.367557682459 delta=-4.424349401198e-02 degrees=[9, 8, 5, 5, 4, 4, 4, 3, 3, 3] graph6=b'I|mKKFnoG'
3: radius=5.365177363083 delta=-4.662381338731e-02 degrees=[8, 7, 7, 6, 5, 3, 3, 3, 3, 3] graph6=b'I~f[MN@T?'
n=11 count=1249 target=5.666284480139
1: radius=5.666284480139 delta=+0.000000000000e+00 degrees=[10, 10, 4, 4, 4, 4, 4, 4, 4, 3, 3] graph6=b'J~e[kePcM__'
2: radius=5.613581751369 delta=-5.270272877003e-02 degrees=[10, 9, 5, 5, 4, 4, 4, 4, 3, 3, 3] graph6=b'J|mKKFn_M@_'
3: radius=5.613095110115 delta=-5.318937002420e-02 degrees=[10, 9, 5, 5, 4, 4, 4, 4, 3, 3, 3] graph6=b'J|mKKE@z}?_'
n=12 count=7595 target=5.905046089761
1: radius=5.905046089761 delta=+0.000000000000e+00 degrees=[11, 11, 4, 4, 4, 4, 4, 4, 4, 4, 3, 3] graph6=b'K~e[kePcK_y@'
2: radius=5.846233372824 delta=-5.881271693694e-02 degrees=[11, 10, 5, 5, 4, 4, 4, 4, 4, 3, 3, 3] graph6=b'K|mKKE@z{?wB'
3: radius=5.845787618257 delta=-5.925847150412e-02 degrees=[11, 10, 5, 5, 4, 4, 4, 4, 4, 3, 3, 3] graph6=b'K|mKKE@_N^w@'
n=13 count=49566 target=6.130771829068
1: radius=6.130771829068 delta=+0.000000000000e+00 degrees=[12, 12, 4, 4, 4, 4, 4, 4, 4, 4, 4, 3, 3] graph6=b'L~e[kePcK_q@s@'
2: radius=6.067789450148 delta=-6.298237892022e-02 degrees=[12, 11, 5, 5, 4, 4, 4, 4, 4, 4, 3, 3, 3] graph6=b'L|mKKE@z{?oBoD'
3: radius=6.067738267418 delta=-6.303356164968e-02 degrees=[12, 11, 5, 5, 4, 4, 4, 4, 4, 4, 3, 3, 3] graph6=b'L|mKKE@_N^o@oB'**Planning spectral radius optimization** **Evaluating C implementation for eigen computations** **Confirming eigenvalue gap sufficiency**
**Assessing spectral radius convergence speed**
$ /bin/bash -lc "/usr/bin/time -f '%e seconds' sh -c 'head -1001 /tmp/tri14.g6 > /tmp/tri14-small.g6; python3 tools/check_finite.py 14 /tmp/tri14-small.g6 >/tmp/tri14-small.out' && cat /tmp/tri14-small.out" /bin/bash: line 1: /usr/bin/time: No such file or directory
**Evaluating shell time builtin usage**
$ /bin/bash -lc 'time (head -1001 /tmp/tri14.g6 > /tmp/tri14-small.g6; python3 tools/check_finite.py 14 /tmp/tri14-small.g6 >/tmp/tri14-small.out); cat /tmp/tri14-small.out' real 0m0.539s user 0m0.528s sys 0m0.009s n=14 count=1001 target=6.345446852691 1: radius=6.130887191658 delta=-2.145596610326e-01 degrees=[11, 9, 8, 8, 6, 5, 4, 3, 3, 3, 3, 3, 3, 3] graph6=b'M|mK[VhGHPd@AIAW?' 2: radius=6.102974626386 delta=-2.424722263046e-01 degrees=[10, 9, 9, 8, 6, 4, 4, 4, 3, 3, 3, 3, 3, 3] graph6=b'M~f[KNDoIHI_S@[??' 3: radius=6.099121822076 delta=-2.463250306148e-01 degrees=[10, 10, 8, 8, 5, 5, 4, 4, 3, 3, 3, 3, 3, 3] graph6=b'M|mK[U@y]?kAGCIC_'
**Planning numerical optimization and benchmarking**
$ /bin/bash -lc "python3 -m pip install --quiet --target /tmp/boots-numpy numpy && PYTHONPATH=/tmp/boots-numpy python3 -c 'import numpy; print(numpy.__version__)'" /usr/bin/python3: No module named pip
**Planning adjacency matrix spectral analysis** **Planning numeric target computation and patch application**
The last finite case exposed a tooling bottleneck rather than a mathematical one: the generated \(339{,}722\) order-14 triangulations make the pure-Python eigenvalue loop unnecessarily slow. I’m replacing only that numerical audit loop with a small compiled checker, while leaving all theorem-bearing work in Lean; this should close the enumeration check without weakening the distinction between evidence and proof.$ /bin/bash -lc 'export ZIG_GLOBAL_CACHE_DIR=/tmp/boots-zig-global ZIG_LOCAL_CACHE_DIR=/tmp/boots-zig-local; /tmp/zig-x86_64-linux-0.14.1/zig cc -O3 -o /tmp/check_finite tools/check_finite.c -lm && time /tmp/check_finite 14 /tmp/tri14.g6' n=14 count=339722 target=6.345446852691 1: radius=6.345446852691 delta=-8.881784197001e-16 degrees=[13, 13, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 3, 3] graph6=M~e[kePcK_q@c@s?_ 2: radius=6.279560032939 delta=-6.588681975185e-02 degrees=[13, 12, 5, 5, 4, 4, 4, 4, 4, 4, 4, 3, 3, 3] graph6=M|mKKE@_N^o@_BoA_ 3: radius=6.279513384416 delta=-6.593346827480e-02 degrees=[13, 12, 5, 5, 4, 4, 4, 4, 4, 4, 4, 3, 3, 3] graph6=M|mKKE@_K?|~_@o@_ real 0m2.508s user 0m2.490s sys 0m0.008s
**Comparing C and Python outputs for n7/8**
$ /bin/bash -lc '/tmp/check_finite 7 /tmp/tri7.g6 && /tmp/check_finite 8 /tmp/tri8.g6' n=7 count=5 target=4.504664353588 1: radius=4.511404664227 delta=+6.740310638712e-03 degrees=[6, 5, 5, 5, 3, 3, 3] graph6=F~f]G 2: radius=4.504664353588 delta=+0.000000000000e+00 degrees=[6, 6, 4, 4, 4, 3, 3] graph6=F~e]g 3: radius=4.475122250239 delta=-2.954210334920e-02 degrees=[6, 5, 5, 4, 4, 3, 3] graph6=F|nmG n=8 count=14 target=4.838537617035 1: radius=4.854101966250 delta=+1.556434921504e-02 degrees=[6, 6, 6, 6, 3, 3, 3, 3] graph6=G~f]Ig 2: radius=4.838537617035 delta=+8.881784197001e-16 degrees=[7, 7, 4, 4, 4, 4, 3, 3] graph6=G|}K]S 3: radius=4.821583421593 delta=-1.695419544211e-02 degrees=[7, 6, 5, 5, 4, 3, 3, 3] graph6=G|mN]C
**Planning formal planar graph proof** **Analyzing vertex degree constraints in planar graph** **Confirming nonplanarity of K₂ join cycle**
**Formalizing planar edge bound contradiction** **Planning formal structural lemma implementation**
$ /bin/bash -lc 'rg -n "IsPath|path.*degree|degree.*two|IsCycle|acyclic.*degree|PathGraph|pathGraph" Mathlib/Combinatorics/SimpleGraph | head -100 && rg -n "maxDegree.*2|degree.*≤ 2|degree.*<= 2" Mathlib | head -80'
Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean:105: h.regular.degree_eq, two_mul]
Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean:107: simp [h.regular.degree_eq, two_mul]
Mathlib/Combinatorics/SimpleGraph/CycleGraph.lean:77:theorem cycleGraph_degree_two_le {n : ℕ} {v : Fin (n + 2)} :
Mathlib/Combinatorics/SimpleGraph/CycleGraph.lean:83: rw [cycleGraph_degree_two_le, Finset.card_pair]
Mathlib/Combinatorics/SimpleGraph/CycleGraph.lean:87:theorem pathGraph_le_cycleGraph {n : ℕ} : pathGraph n ≤ cycleGraph n := by
Mathlib/Combinatorics/SimpleGraph/CycleGraph.lean:92: rw [pathGraph_adj] at h
Mathlib/Combinatorics/SimpleGraph/CycleGraph.lean:99: (pathGraph_preconnected n).mono pathGraph_le_cycleGraph
Mathlib/Combinatorics/SimpleGraph/CycleGraph.lean:102: (pathGraph_connected n).mono pathGraph_le_cycleGraph
Mathlib/Combinatorics/SimpleGraph/CycleGraph.lean:158:theorem cycleGraph.isPath_tail_cycle : (cycleGraph.cycle n).tail.IsPath := by
Mathlib/Combinatorics/SimpleGraph/CycleGraph.lean:164:theorem cycleGraph.isCycle_cycle : (cycleGraph.cycle n).IsCycle :=
Mathlib/Combinatorics/SimpleGraph/CycleGraph.lean:174: cycleGraph n ⊑ G ↔ ∃ (v : V) (p : G.Walk v v), p.IsCycle ∧ p.length = n := by
Mathlib/Combinatorics/SimpleGraph/CycleGraph.lean:199: have := IsPath.mk' <| (support_tail_of_not_nil _ hp₁.not_nil) ▸ hp₁.support_nodup
Mathlib/Combinatorics/SimpleGraph/Hasse.lean:24:* `SimpleGraph.pathGraph`: Path graph on `n` vertices.
Mathlib/Combinatorics/SimpleGraph/Hasse.lean:108:def pathGraph (n : ℕ) : SimpleGraph (Fin n) :=
Mathlib/Combinatorics/SimpleGraph/Hasse.lean:111:theorem pathGraph_adj {n : ℕ} {u v : Fin n} :
Mathlib/Combinatorics/SimpleGraph/Hasse.lean:112: (pathGraph n).Adj u v ↔ u.val + 1 = v.val ∨ v.val + 1 = u.val := by simp [pathGraph, hasse]
Mathlib/Combinatorics/SimpleGraph/Hasse.lean:114:theorem pathGraph_preconnected (n : ℕ) : (pathGraph n).Preconnected :=
Mathlib/Combinatorics/SimpleGraph/Hasse.lean:117:theorem pathGraph_con**Verifying graph structure as path**
$ /bin/bash -lc 'rg -n "degree.*[≤<]=? 2|degree.*two|pathGraph.*Iso|iso.*pathGraph|IsTree.*path|Path.*spanning" Mathlib/Combinatorics/SimpleGraph | head -150'
Mathlib/Combinatorics/SimpleGraph/CycleGraph.lean:77:theorem cycleGraph_degree_two_le {n : ℕ} {v : Fin (n + 2)} :
Mathlib/Combinatorics/SimpleGraph/CycleGraph.lean:83: rw [cycleGraph_degree_two_le, Finset.card_pair]
Mathlib/Combinatorics/SimpleGraph/Hasse.lean:141:def IsPath.pathGraphIsoToSubgraph (hw : w.IsPath) :
Mathlib/Combinatorics/SimpleGraph/Hasse.lean:155: w.toSubgraph.coeCopy.comp hw.pathGraphIsoToSubgraph.toCopy
Mathlib/Combinatorics/SimpleGraph/Matching.lean:415:lemma Walk.IsPath.isCycles_spanningCoe_toSubgraph_sup_edge {u v} {p : G.Walk u v} (hp : p.IsPath)
Mathlib/Combinatorics/SimpleGraph/Matching.lean:513: (p : G.Walk v w) (hp : p.IsPath) : (G \ p.toSubgraph.spanningCoe).Reachable w v := by
Mathlib/Combinatorics/SimpleGraph/Tutte.lean:42: (p : G'.Walk a x) (hp : p.IsPath) (hcalt : G'.IsAlternating M.spanningCoe)
Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean:105: h.regular.degree_eq, two_mul]
Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean:107: simp [h.regular.degree_eq, two_mul]
Mathlib/Combinatorics/SimpleGraph/Acyclic.lean:265:lemma IsTree.existsUnique_path (hG : G.IsTree) : ∀ v w, ∃! p : G.Walk v w, p.IsPath :=**Planning formal planarity characterization** **Evaluating planarity definition strategies** **Planning theorem aggregator and build checks**
**Inspecting Audit.lean axioms**
$ /bin/bash -lc "sed -n '1,260p' BootsRoyle/Spectral.lean && sed -n '1,260p' BootsRoyle/Arithmetic.lean && sed -n '1,320p' BootsRoyle/Identities.lean"
import Mathlib.Analysis.InnerProductSpace.Rayleigh
import Mathlib.Analysis.Matrix.Spectrum
import Mathlib.Combinatorics.SimpleGraph.LapMatrix
/-!
# Spectral preliminaries for the Boots--Royle/Cao--Vince problem
This file defines the adjacency spectral radius as the maximum Rayleigh
quotient of the real adjacency operator. This is a convenient definition for
the edge-switching arguments in the paper and is definitionally independent of
any ordering chosen for the eigenvalues.
-/
open scoped InnerProductSpace
namespace BootsRoyle
open Matrix
variable {V : Type*} [Fintype V] [DecidableEq V]
/-- The real adjacency matrix, with its finite decidability instance hidden
behind a noncomputable definition. -/
noncomputable def adjacencyMatrix (G : SimpleGraph V) : Matrix V V ℝ :=
by
classical
exact G.adjMatrix ℝ
/-- The real adjacency operator of a finite simple graph. -/
noncomputable def adjacencyOperator (G : SimpleGraph V) :
EuclideanSpace ℝ V →ₗ[ℝ] EuclideanSpace ℝ V :=
(adjacencyMatrix G).toEuclideanLin
/-- The continuous version of `adjacencyOperator`. -/
noncomputable def adjacencyContinuousOperator (G : SimpleGraph V) :
EuclideanSpace ℝ V →L[ℝ] EuclideanSpace ℝ V :=
(adjacencyOperator G).toContinuousLinearMap
/-- The adjacency spectral radius, expressed as the maximum Rayleigh quotient.
For a real symmetric adjacency matrix this is its largest (algebraic)
eigenvalue. The name follows the graph-theory convention; for a nonnegative
matrix Perron--Frobenius identifies this with the usual matrix spectral radius.
-/
noncomputable def adjacencySpectralRadius (G : SimpleGraph V) : ℝ :=
⨆ x : {x : EuclideanSpace ℝ V // x ≠ 0},
⟪adjacencyOperator G x, x⟫_ℝ / ‖(x : EuclideanSpace ℝ V)‖ ^ 2
lemma adjacencyOperator_isSymmetric (G : SimpleGraph V) :
(adjacencyOperator G).IsSymmetric := by
classical
exact Matrix.isSymmetric_toEuclideanLin_iff.mpr (G.isHermitian_adjMatrix (R := ℝ))
lemma adjacencyOperator_apply (G : SimpleGraph V) **Planning formalizing polynomial lemmas**
$ /bin/bash -lc "sed -n '400,900p' /work/paper.txt"
Lemma 3.4. For any v ∈ S and any face F of G − v, we have
6
P
u∈F xu ≤ λxv .
Proof. Let v be a cubic vertex with support triangle T , and let F be a face of G − v. Draw v
inside the interior of F , and join it to the three vertices of F , and call the resulting triangulation
P
GF . Let S(F ) := u∈F xu . The Rayleigh principle implies that
xT A(GF )x xT A(G)x
−
xT x
xT x
2xv
2xv
= T (S(F ) − S(T )) = T (S(F ) − λxv )
x x
x x
λ(GF ) − λ ≥
Since G is extremal, λ(GF ) ≤ λ. Hence S(F ) ≤ λxv .
Lemma 3.4 allows us to refine our understanding of how the Perron entries are distributed.
With this in mind, for x > 0, let
L0 (x) :=
k
,
2n − k − 4 + 3k/x
c :=
2 1
+ .
3 λ
Lemma 3.5. For every v ∈ S, we have
3
.
λ(λ + 1)
(3.4)
L
L
≤ x∗ ≤
.
k
1 + (k − 1)c
(3.5)
cx∗ ≤ xv ≤
Moreover, the maximum entry x∗ satisfies
Proof. We first show that xv ≥ cx∗ for every v ∈ S. The case k = 1 is trivial. Assume now that
k ≥ 2, and choose distinct cubic vertices u, v with xu = x∗ . Write N (u) = {a, b, c}. By Lemma
3.2, u remains a cubic vertex of G − v, and uab, ubc, uca are faces of G − v. Moving v inside the
interior of the face among these three that maximizes the sum of the Perron entries, Lemma 3.4
yields
λ xv ≥ xu + max{xa + xb , xb + xc , xc + xa }
2λ
2
xu .
≥ xu + (xa + xb + xc ) = 1 +
3
3
Thus xv ≥ cxu = cx∗ . Moreover, since λ > rn > 5, we have c < 1, and therefore xv ≥ cx∗ for all
cubic vertices.
For the upper bound in (3.4), we observe that rw = 1 − (λ + 1)xw ≥ 0 for each w ∈ V (G), so
xw ≤ 1/(λ + 1). Now, using the eigenvalue – eigenvector equation at a cubic vertex v, we get
λxv =
X
xw ≤
w∈N (v)
3
,
λ+1
which proves the desired inequality.
Now we prove (3.5). The inequality x∗ ≥ L/k follows because x∗ is their largest coordinate.
For the upper bound on x∗ , we use the bound xv ≥ cx∗ for v ∈ S, which implies L ≥
x∗ + (k − 1)cx∗ .
Lemma 3.6. L ≥ L0 (λ).
7
Proof. Let T1 , . . . , Tk be the support faces in the core R. If F is an unoccupied face of R, then
F i$ /bin/bash -lc "sed -n '900,1320p' /work/paper.txt"
12
Case 4: k ≥ 7 and n − 6 − kt/(t − 2) < 0. In this case, put θ := k/(2n − 4). Since 0 < θ ≤ 1/3,
the quantity 1 − (1 − 3/t)θ is positive. By the definition of L0 (x),
L0 (t) =
θ
,
1 − (1 − 3/t)θ
γk L0 (t) =
2 θ − 6/(2n − 4)
·
.
3 1 − (1 − 3/t)θ
Substituting into (4.4), and using 2n − 4 = t2 − 3t + 3, gives
(n − 6)s + kz − L0 (t) − (t − 4)
2 θ − 6/(2n − 4)
θ
2n − 12 + (2n − 4)θ
2− ·
−
− (t − 4)
≤
3t − 2
3 1 − (1 − 3/t)θ
1 − (1 − 3/t)θ
−2(2n − 4)(4t − 9)θ2 + (7t3 − 54t2 + 172t − 162)θ − 3t3 + 24t2 − 42t −
=
(3t − 2)(3t − (3t − 9)θ)
96t
2n − 4 .
(4.9)
The numerator in the last fraction is a quadratic in θ with negative leading coefficient. Its
discriminant is
−(47t6 − 516t5 + 988t4 + 5652t3 − 25720t2 + 39744t − 26244) < 0.
Hence the numerator in (4.9) is negative for every real θ. This proves the desired inequality in
the last case.
Proposition 4.1. The extremal graph G has a universal vertex.
Proof. Assume, for a contradiction, that d(v) ≤ n−2 for each v ∈ V (G). Then cv = max{0, d(v)−
P
4} ≤ n − 6 for every v ∈ V (G). By (3.2), we have v cv = 2n − 12 + k. Since xi ≤ z for i ≥ 3, it
follows that
X
E≤z
cv + (x1 − z)cv1 + (x2 − z)cv2
v∈V (G)
≤ z(2n − 12 + k) + (n − 6)(x1 + x2 − 2z)
= (n − 6)s + kz.
(4.10)
Combining (4.10) with Lemma 3.3, we get λ − 4 = E − L ≤ (n − 6)s + kz − L. Since L > L0 (rn ),
this yields λ − 4 < (n − 6)s + kz − L0 (rn ). On the other hand, it follows from Lemma 4.1 that
(n − 6)s + kz − L0 (rn ) < rn − 4. Combining the above two inequalities,
λ − 4 < (n − 6)s + kz − L0 (rn ) < rn − 4,
a contradiction. Hence G has a universal vertex.
5. Forcing a second universal vertex
In Section 4, we proved that G has a universal vertex, say u. The eigenvalue – eigenvector
equation at u implies that xu = 1/(λ + 1). Moreover, this is the largest Perron entry. Hence, we
may assume the universal vertex is v1 . The aim of this section is to prove that G has a second
universal vertex.
13
Since v1 is a universal vertex, the graph G − v1 has 3n − 6$ /bin/bash -lc "sed -n '1320,1400p' /work/paper.txt" The graph G′ contains no cycle. Indeed, if it contained a cycle Cℓ , then the subgraph on that cycle together with v1 , v2 would contain K2 ∨ Cℓ . This graph has 1 + 2ℓ + ℓ = 3ℓ + 1 edges on ℓ + 2 vertices, exceeding the planar bound 3(ℓ + 2) − 6 = 3ℓ. Thus G′ is acyclic. Together with ∆(G′ ) ≤ 2, this shows that G′ is a disjoint union of paths and isolated vertices. Finally, since G is a triangulation, e(G′ ) = e(G) − (1 + 2(n − 2)) = 3n − 6 − (2n − 3) = |V (G′ )| − 1. An acyclic graph on |V (G′ )| vertices with |V (G′ )| − 1 edges is connected. Therefore G′ = Pn−2 , and G = K2 ∨ Pn−2 . This proves the Theorem 1.1. Declaration on the use of AI The authors used ChatGPT to generate code for searching the extremal planar graphs for n ≤ 14, and to assist with several computations and symbolic derivations. ChatGPT was also used for grammar checking, language polishing, and improving the clarity of the exposition. The core ideas and overall strategy of the proof were developed by the authors. The authors take full responsibility for the correctness and originality of the paper. References [1] J. A. Bondy and U. S. R. Murty, Graph Theory, Graduate Texts in Mathematics 244, Springer, New York, 2008. 3 [2] B. N. Boots and G. F. Royle, A conjecture on the maximum value of the principal eigenvalue of a planar graph, Geogr. Anal. 23 (1991), 276–282. 2 [3] D. Cao and A. Vince, The spectral radius of a planar graph, Linear Algebra Appl. 187 (1993), 251–257. 1, 2 [4] D. Cvetković and P. Rowlinson, The largest eigenvalue of a graph: A survey, Linear Multilinear Algebra 28 (1990), 3–33. 1 [5] M. N. Ellingham, L. Lu, and Z. Wang, Maximum spectral radius of outerplanar 3-uniform hypergraphs, J. Graph Theory 100 (2022), 671–685. 3 [6] M. N. Ellingham and X. Zha, The spectral radius of graphs on surfaces, J. Combin. Theory Ser. B 78 (2000), 45–56. 1, 3 [7] B. D. Guiduli, Spectral Extrema for Graphs, Ph.D. thesis, University of Chicago, Chicago, Illinois, 1996. 2 [8] W.H. Haemers, In
**Identifying minor paper inconsistencies** **Planning Lean build and audit setup**
**Verifying exact theorem name**
$ /bin/bash -lc 'rg -n "theorem strict|lemma strict" BootsRoyle/Spectral.lean && lake build BootsRoyle && lake env lean BootsRoyle/Audit.lean'
**Considering alternative name patterns**
$ /bin/bash -lc 'tail -160 BootsRoyle/Spectral.lean'
intro v
refine lt_of_le_of_ne (hx_nonneg v) ?_
intro hv_eq
have hv : x v = 0 := hv_eq.symm
have hall : ∀ w, x w = 0 := by
intro w
obtain ⟨p⟩ := hG v w
have along {a b : V} (q : G.Walk a b) : x a = 0 → x b = 0 := by
induction q with
| nil => exact fun ha ↦ ha
| @cons u z w huz q ih =>
intro hu
exact ih (eigenvector_zero_propagates G hx_nonneg hx_eigen huz hu)
exact along p hv
apply hx_ne
ext i
exact hall i
/-- Connected graphs have a strictly positive Perron vector for the
variational adjacency spectral radius. -/
theorem exists_positive_perronVector (G : SimpleGraph V) (hG : G.Connected) :
∃ x : EuclideanSpace ℝ V,
(∀ i, 0 < x i) ∧
adjacencyOperator G x = adjacencySpectralRadius G • x := by
letI := hG.nonempty
obtain ⟨x, hx_ne, hx_nonneg, hx_eigen⟩ := exists_nonnegative_perronVector G
exact ⟨x, eigenvector_pos_of_connected G hG hx_ne hx_nonneg hx_eigen, hx_eigen⟩
/-- The `ℓ¹`-normalization used throughout the paper. -/
theorem exists_l1_normalized_perronVector (G : SimpleGraph V) (hG : G.Connected) :
∃ x : EuclideanSpace ℝ V,
(∀ i, 0 < x i) ∧
(∑ i, x i) = 1 ∧
adjacencyOperator G x = adjacencySpectralRadius G • x := by
classical
letI := hG.nonempty
obtain ⟨x, hx_pos, hx_eigen⟩ := exists_positive_perronVector G hG
let s : ℝ := ∑ i, x i
have hs_nonneg : 0 ≤ s := Finset.sum_nonneg fun i _ ↦ (hx_pos i).le
have hs_ne : s ≠ 0 := by
intro hs
have hall := (Finset.sum_eq_zero_iff_of_nonneg fun i _ ↦ (hx_pos i).le).mp hs
exact (hx_pos (Classical.choice inferInstance)).ne' (hall _ (Finset.mem_univ _))
have hs_pos : 0 < s := lt_of_le_of_ne hs_nonneg (Ne.symm hs_ne)
let y : EuclideanSpace ℝ V := s⁻¹ • x
refine ⟨y, fun i ↦ ?_, ?_, ?_⟩
· simp only [y, PiLp.smul_apply, smul_eq_mul]
exact mul_pos (inv_pos.mpr hs_pos) (hx_pos i)
· simp only [y, PiLp.smul_apply, smul_eq_mul, ← Finset.mul_sum, s]
exact inv_mul_cancel₀ hs_ne
· simp **Fixing audit name application**
**Running build process**
$ /bin/bash -lc 'lake build BootsRoyle && lake env lean BootsRoyle/Audit.lean' ✖ [2/3] Building BootsRoyle (535ms) trace: .> LEAN_PATH=/work/repro/.lake/packages/Cli/.lake/build/lib/lean:/work/repro/.lake/packages/batteries/.lake/build/lib/lean:/work/repro/.lake/packages/Qq/.lake/build/lib/lean:/work/repro/.lake/packages/aesop/.lake/build/lib/lean:/work/repro/.lake/packages/proofwidgets/.lake/build/lib/lean:/work/repro/.lake/packages/importGraph/.lake/build/lib/lean:/work/repro/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/work/repro/.lake/packages/plausible/.lake/build/lib/lean:/work/repro/.lake/build/lib/lean /opt/elan/toolchains/leanprover--lean4---v4.33.0-rc1/bin/lean /work/repro/BootsRoyle.lean -o /work/repro/.lake/build/lib/lean/BootsRoyle.olean -i /work/repro/.lake/build/lib/lean/BootsRoyle.ilean -c /work/repro/.lake/build/ir/BootsRoyle.c --setup /work/repro/.lake/build/ir/BootsRoyle.setup.json --json error: BootsRoyle.lean:9:0: invalid 'import' command, it must be used in the beginning of the file error: Lean exited with code 1 Some required targets logged failures: - BootsRoyle error: build failed
**Verifying import order rules** **Testing combined import syntax**
$ /bin/bash -lc 'nl -ba BootsRoyle.lean | head -30 && nl -ba lakefile.lean | head -60'
1 /-!
2 # Formal components of the Boots--Royle/Cao--Vince reproduction attempt
3
4 The modules imported here are the parts of the paper's proof that were
5 completed without additional axioms. The exact completion status and the
6 missing planarity layer are documented in `README.md`.
7 -/
8
9 import BootsRoyle.Arithmetic
10 import BootsRoyle.Identities
11 import BootsRoyle.Spectral
1 import Lake
2
3 open Lake DSL
4
5 /-!
6 ## Mathlib dependencies on upstream projects
7 -/
8
9 require "leanprover-community" / "batteries" @ git "main"
10 require "leanprover-community" / "Qq" @ git "master"
11
12 require "leanprover-community" / "aesop" @ git "master"
13 require "leanprover-community" / "proofwidgets" @ git "main"
14 with NameMap.empty.insert `errorOnBuild
15 "ProofWidgets failed to reuse pre-built JS code. \
16 Please report this issue on the Lean Zulip."
17 require "leanprover-community" / "importGraph" @ git "main"
18 require "leanprover-community" / "LeanSearchClient" @ git "main"
19 require "leanprover-community" / "plausible" @ git "main"
20
21
22 /-!
23 ## Options for building mathlib
24 -/
25
26 /-- These options are used as `leanOptions`, prefixed by `` `weak``, so that
27 `lake build` uses them, as well as `Archive` and `Counterexamples`. -/
28 abbrev mathlibOnlyLinters : Array LeanOption := #[
29 ⟨`linter.mathlibStandardSet, true⟩,
30 -- Explicitly enable the header linter, since the standard set is defined in `Mathlib.Init`
31 -- but we want to run this linter in files imported by `Mathlib.Init`.
32 ⟨`linter.style.header, true⟩,
33 ⟨`linter.checkInitImports, true⟩,
34 ⟨`linter.allScriptsDocumented, true⟩,
35 ⟨`linter.pythonStyle, true⟩,
36 ⟨`linter.style.longFile, .ofNat 1500⟩,
37 -- ⟨`linter.nightlyRegressionSet, tr**Reordering imports before module doc and removing duplicates**
$ /bin/bash -lc 'lake build BootsRoyle && lake env lean BootsRoyle/Audit.lean' ⚠ [8676/8681] Replayed BootsRoyle.Spectral warning: BootsRoyle/Spectral.lean:66:8: automatically included section variable(s) unused in theorem `BootsRoyle.vectorAbs_apply`: [Fintype V] [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype V] [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` warning: BootsRoyle/Spectral.lean:69:8: automatically included section variable(s) unused in theorem `BootsRoyle.norm_vectorAbs`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` warning: BootsRoyle/Spectral.lean:284:2: `push_neg` has been deprecated. Prefer using `push Not` instead. If you'd rather continue using `push_neg` in your project, you can implement it as follows: ``` open Lean.Parser.Tactic in macro "push_neg" cfg:optConfig loc:(location)? : tactic => `(tactic| push $cfg:optConfig Not $[$loc]?) ``` ⚠ [8678/8681] Built BootsRoyle.Identities (4.7s) warning: BootsRoyle/Identities.lean:89:4: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` warning: BootsRoyle/Identities.lean:118:0: automatically included section variable(s) unused in theorem `BootsRoyle.PerronData.degreeExcess_cast_eq`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` ⚠ [8679/8681] Built BootsRoyle.Arithmetic (13s) warning: BootsRoyle/Arithmetic.lean:49:34: Variable name `hn` is not explicitly referenced. Hint: The binding can be removed (if unu
**Planning detailed README content**
$ /bin/bash -lc 'plantri_dir=$(find /tmp -maxdepth 2 -type d -path '"'*/plantri58' | tail -1); for n in 4 5 6; do \""'$plantri_dir/plantri" -g "$n" "/tmp/tri${n}.g6" >/dev/null 2>&1; /tmp/check_finite "$n" "/tmp/tri${n}.g6"; done'
n=4 count=1 target=3.000000000000
1: radius=3.000000000000 delta=+0.000000000000e+00 degrees=[3, 3, 3, 3] graph6=C~
2: radius=-inf delta=-inf degrees=[0, 0, 0, 0] graph6=
3: radius=-inf delta=-inf degrees=[0, 0, 0, 0] graph6=
n=5 count=1 target=3.645751311065
1: radius=3.645751311065 delta=+0.000000000000e+00 degrees=[4, 4, 4, 3, 3] graph6=D~s
2: radius=-inf delta=-inf degrees=[0, 0, 0, 0, 0] graph6=
3: radius=-inf delta=-inf degrees=[0, 0, 0, 0, 0] graph6=
n=6 count=2 target=4.119026675526
1: radius=4.119026675526 delta=-8.881784197001e-16 degrees=[5, 5, 4, 4, 3, 3] graph6=E|~G
2: radius=4.000000000000 delta=-1.190266755259e-01 degrees=[4, 4, 4, 4, 4, 4] graph6=E|tw
3: radius=-inf delta=-inf degrees=[0, 0, 0, 0, 0, 0] graph6=**Analyzing planar graph exceptions and gaps** **Assessing planarity formalization challenges** **Planning audit script creation**
**Evaluating polynomial positivity proofs** **Drafting proven results summary**
The order-14 audit is complete: all \(339{,}722\) unlabelled plane triangulations were checked, and \(K_2\vee P_{12}\) is first with a numerical gap of about \(0.06589\) to the runner-up. The remaining obstruction is now sharply isolated: neither mathlib nor the tooling projects I could locate provide a formal notion of planarity with the Euler/face/outerplanar consequences used throughout the argument. Substituting only those consequences would prove a convenient variant, not the paper’s theorem, so I am documenting that boundary explicitly and performing the final axiom/build audit.**Evaluating README link strategy** **Searching GitHub for Lean graph libraries**
**Refining source audit regex** **Improving audit command for source detection**
**Testing deprecated warning replacements**
$ /bin/bash -lc "nl -ba BootsRoyle/Arithmetic.lean | sed -n '42,55p'; nl -ba BootsRoyle/Identities.lean | sed -n '82,94p'; nl -ba BootsRoyle/Spectral.lean | sed -n '278,288p'"
42
43 lemma comparisonRoot_quadratic {n : ℕ} (hn : 3 ≤ n) :
44 comparisonRoot n ^ 2 - 3 * comparisonRoot n = 2 * n - 7 := by
45 have hs := comparisonRoot_sq_sqrt hn
46 rw [comparisonRoot]
47 nlinarith
48
49 lemma comparisonRoot_pos {n : ℕ} (hn : 3 ≤ n) :
50 0 < comparisonRoot n := by
51 rw [comparisonRoot]
52 have := Real.sqrt_nonneg (8 * (n : ℝ) - 19)
53 positivity
54
55 lemma comparisonRoot_gt_thirteen_halves {n : ℕ} (hn : 15 ≤ n) :
82
83 lemma degree_term_eq (hmin : ∀ v, 3 ≤ G.degree v) (v : V) :
84 (G.degree v : ℝ) * P.x v =
85 4 * P.x v + (degreeExcess (G := G) v : ℝ) * P.x v -
86 (if G.degree v = 3 then P.x v else 0) := by
87 by_cases hv : G.degree v = 3
88 · simp [hv, degreeExcess]
89 <;> ring
90 · have hv4 : 4 ≤ G.degree v := by
91 have := hmin v
92 omega
93 rw [degreeExcess, Nat.cast_sub hv4]
94 simp [hv]
278 lemma quadraticForm_strictMono_of_positive {G H : SimpleGraph V} (hGH : G < H)
279 (x : EuclideanSpace ℝ V) (hx : ∀ i, 0 < x i) :
280 ⟪adjacencyOperator G x, x⟫_ℝ < ⟪adjacencyOperator H x, x⟫_ℝ := by
281 classical
282 have hnle : ¬H ≤ G := hGH.2
283 simp only [SimpleGraph.le_iff_adj] at hnle
284 push_neg at hnle
285 obtain ⟨v, w, hH, hG⟩ := hnle
286 simp only [adjacencyOperator_apply, EuclideanSpace.inner_eq_star_dotProduct, star_trivial,
287 dotProduct, mulVec, Finset.mul_sum, adjacencyMatrix, SimpleGraph.adjMatrix_apply]
288 apply Finset.sum_lt_sum**Evaluating renaming or removing _hn variable**
$ /bin/bash -lc "rg -n \"comparisonRoot_pos\" . --glob '*.lean'"
./BootsRoyle/Arithmetic.lean:49:lemma comparisonRoot_pos {n : ℕ} (hn : 3 ≤ n) :**Removing warnings and optimizing type constraints**
**Testing semicolon syntax in linter** **Clarifying semicolon tactic syntax behavior**
$ /bin/bash -lc "lake build BootsRoyle && lake env lean BootsRoyle/Audit.lean && rg -n '\\bsorry\\b|\\badmit\\b' --glob '*.lean' BootsRoyle BootsRoyle.lean || true" ✔ [8677/8681] Built BootsRoyle.Spectral (8.8s) ✔ [8678/8681] Built BootsRoyle.Arithmetic (10s) ⚠ [8679/8681] Built BootsRoyle.Identities (3.2s) warning: BootsRoyle/Identities.lean:89:4: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` warning: BootsRoyle/Identities.lean:132:0: automatically included section variable(s) unused in theorem `BootsRoyle.PerronData.sum_degreeExcess_eq`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` ✔ [8680/8681] Built BootsRoyle (6.5s) Build completed successfully (8681 jobs). 'BootsRoyle.exists_l1_normalized_perronVector' depends on axioms: [propext, Classical.choice, Quot.sound] 'BootsRoyle.adjacencySpectralRadius_strictMono_of_connected' depends on axioms: [propext, Classical.choice, Quot.sound] 'BootsRoyle.PerronData.lambda_eq_four_add_excess_sub_cubicWeight' depends on axioms: [propext, Classical.choice, Quot.sound] 'BootsRoyle.PerronData.sum_degreeExcess_eq' depends on axioms: [propext, Classical.choice, Quot.sound] 'BootsRoyle.selectedFace_averaging' depends on axioms: [propext, Classical.choice, Quot.sound]
**Refining tactic syntax and handling warnings**
$ /bin/bash -lc "git diff --check && git status --short && git diff --stat && sed -n '1,160p' lakefile.lean | tail -25" M README.md M lakefile.lean ?? BootsRoyle.lean ?? BootsRoyle/ ?? tools/ README.md | 338 ++++++++++++++++++++++++++++++++++------------------------ lakefile.lean | 3 + 2 files changed, 204 insertions(+), 137 deletions(-) -- Executables which import `Lake` must set `-lLake`. weakLinkArgs := #["-lLake"] /-- `lake exe check-title-labels` checks if a PR title obeys some basic formatting requirements. Currently, these checks are quite lenient, but could be made stricter in the future. -/ lean_exe «check_title_labels» where srcDir := "scripts" /-- `lake exe nightly-testing-checklist` reports nightly-testing branch status. -/ lean_exe «nightly-testing-checklist» where srcDir := "scripts" lean_exe mathlib_test_executable where root := `MathlibTest.MathlibTestExecutable /-! ## Other configuration -/ /-- When a package depending on Mathlib updates its dependencies, update its toolchain to match Mathlib's and fetch the new cache. -/ post_update pkg do let rootPkg ← getRootPackage
**Confirming authorized README overwrite** **Reviewing Lakefile minimal changes**
$ /bin/bash -lc 'git diff -- lakefile.lean | cat && git diff -- README.md | head -80' diff --git a/lakefile.lean b/lakefile.lean index bcdf13405f..e76353648d 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -72,6 +72,9 @@ lean_lib Mathlib where -- Enforce Mathlib's default linters and style options. leanOptions := mathlibLeanOptions +/-- Self-contained reproduction development for arXiv:2607.19268v1. -/ +lean_lib BootsRoyle + -- NB. When adding further libraries, check if they should be excluded from `getLeanLibs` in -- `scripts/mk_all.lean`. lean_lib Cache where diff --git a/README.md b/README.md index 36cbc2334f..affa4be220 100644 --- a/README.md +++ b/README.md @@ -1,168 +1,232 @@ -# mathlib4 +# Boots--Royle/Cao--Vince reproduction report - -[](https://mathlib-bors-ca18eefec4cb.herokuapp.com/repositories/16) -[](https://leanprover.zulipchat.com) -[](https://gitpod.io/#https://github.com/leanprover-community/mathlib4) +## Verdict -[Mathlib](https://leanprover-community.github.io) is a user maintained library for the [Lean theorem prover](https://leanprover.github.io). -It contains both programming infrastructure and mathematics, -as well as tactics that use the former and allow to develop the latter. +**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**. -## Installation +The paper's central statement is: -You can find detailed instruct
**Updating plan statuses to completed**
**Planning precise JSON formatting** **Evaluating partial status justification** **Confirming partial status and final JSON**
{"status":"partial","claim":"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.","note":"All files build without sorry; the axiom audit reports only propext, Classical.choice, and Quot.sound. An independent plantri audit confirmed every finite case through n=14, including the exceptions at 7 and 8, but it is not kernel-certified. Completion stopped because mathlib and the tooling projects located contain no faithful planarity/outerplanarity theory supporting Euler counts, facial relocation, maximal outerplanar structure, or certified enumeration. Topological embeddings, rotation systems, and excluded-minor encodings were each investigated; every route requires a substantial foundational formalization, while assuming only the paper’s needed consequences would be circular. No counterexample was found; several nonfatal typographical slips are documented in repro/README.md.","significance":"The paper claims that, except at orders 7 and 8, K₂ ∨ Pₙ₋₂ uniquely maximizes adjacency spectral radius among n-vertex planar graphs. This resolves a conjecture dating to 1991 and identifies the exact spectral extremizer at every order."}