Bollobás–Nikiforov conjecture

The work claims a complete proof of the original Bollobás–Nikiforov conjecture for every finite non-complete simple graph. More precisely, the Lean theorem `BN.lambda1_sq_add_lambda2_sq_le` proves $$\lambda_1(G)^2+\lambda_2(G)^2 \le 2\left(1-\frac{1}{\omega(G)}\right)|E(G)|.$$ The development proves a stronger weighted spectral inequality. If $B$ is a real symmetric entrywise nonnegative matrix with zero diagonal, supported on the edges of $G$, and $F(B)$ is the sum of the squares of its two largest positive eigenvalues, then $$F(B) \le \left(1-\frac{1}{\omega(G)}\right)\|B\|_F^2.$$ The human-readable manuscript is still preliminary and is being rewritten and polished.

The work claims a complete proof of the original Bollobás–Nikiforov conjecture for every finite non-complete simple graph. More precisely, the Lean theorem `BN.lambda1_sq_add_lambda2_sq_le` proves $$\lambda_1(G)^2+\lambda_2(G)^2 \le 2\left(1-\frac{1}{\omega(G)}\right)|E(G)|.$$ The development proves a stronger weighted spectral inequality. If $B$ is a real symmetric entrywise nonnegative matrix with zero diagonal, supported on the edges of $G$, and $F(B)$ is the sum of the squares of its two largest positive eigenvalues, then $$F(B) \le \left(1-\frac{1}{\omega(G)}\right)\|B\|_F^2.$$ The human-readable manuscript is still preliminary and is being rewritten and polished.