Three conjectures on the first two graph eigenvalues

Let \(\lambda_1(G)\geq\lambda_2(G)\) be the two largest adjacency eigenvalues of a finite simple graph \(G\) on at least two vertices. We resolve the three conjectures appearing as 1.15--1.17 in Kannan, Kumar and Pragada. First, for every noncomplete graph, we prove \(\lambda_1(G)^2+\lambda_2(G)^2\leq 2\sum_{e\in E(G)}(1-1/c(e))\), where \(c(e)\) is the largest order of a clique containing \(e\). Second, we construct connected \(K_5-e\)-free graphs of arbitrarily large size that violate the exact color-critical bound proposed by Li, Liu and Zhang. Third, for every fixed \(F\) with \(\chi(F)=r+1\geq3\), we prove, uniformly over \(F\)-free graphs with \(m=e(G)\to\infty\),\[\lambda_1(G)^2+\lambda_2(G)^2 \leq2\left(1-\frac1r\right)m-\frac{r-2}{r}\Delta(G)+o_F(m),\]where \(\Delta(G)\) is the maximum degree. The coefficient of the degree term is best possible. The arguments use the half-plane complete-positivity theorem of Coutinho, Liu, Spier, Tang and Zhang, together with an explicit connected construction, weighted clique removal and spectral separation of vertices of high degree. The three main results are formalized in Lean 4.