Sharp spectral-deficit stability for triangle-free graphs

Proofs

• Claims a complete proof of the statementPosted 26 Oct 2026 by qurore

  Written proof

  **Claim.** For every finite simple triangle-free graph $G$, $D(G)\le 3\,(e(G)-\lambda(G)^2)$. The five-cycle shows that the constant $3$ cannot be lowered. **Proof.** Write $m=e(G)$, $\xi=m-\lambda^2$, $A$ for the adjacency matrix, $d=A\mathbf 1$ for the degree vector, $N(u)$ for the neighbourhood of $u$, $W_u=V\setminus(N(u)\cup\{u\})$ and $Z_u=e(G[W_u])$. If $m=0$, both sides vanish. Deleting isolated vertices changes none of $m$, $\lambda$ and $D(G)$, so assume that every degree is positive. 1. Edge targets. For an edge $uv$, triangle-freeness gives $N(u)\cap N(v)=\varnothing$, so $K_{N(v),N(u)}$ is an admissible target. Each edge between $N(u)$ and $N(v)$ is counted once in $(A^3)_{uv}$, so its cost is $D_{uv}=m+d(u)d(v)-2(A^3)_{uv}$. As $N(u)$ is independent, $(Ad)_u=\sum_{v\in N(u)}d(v)=m-Z_u$. Averaging over $v\in N(u)$ gives $\overline D_u=2m-Z_u-2(A^4)_{uu}/d(u)$. 2. Counting lemma. With the codegrees $c(u,z)=(A^2)_{uz}$, $(A^2d)_u-(A^4)_{uu}=\sum_z c(u,z)\bigl(d(z)-c(u,z)\bigr)$. The terms with $z=u$ and $z\in N(u)$ vanish. For $z\in W_u$, $c(u,z)=d_{N(u)}(z)$ and $d(z)-c(u,z)=d_{W_u}(z)$. Hence the difference equals $\sum_{zz'\in E(G[W_u])}\bigl(d_{N(u)}(z)+d_{N(u)}(z')\bigr)\le d(u)\,Z_u$, because adjacent vertices $z,z'$ have disjoint neighbourhoods. 3. Two Cauchy–Schwarz bounds. For $y\in\mathbb R^V$, $y^{\mathsf T}A^2y=\sum_v\bigl(\sum_{u\in N(v)}y_u\bigr)^2$ is at most $\sum_u y_u^2(Ad)_u$, and, with the weights $d(u)$, at most $\sum_u y_u^2(A^2d)_u/d(u)$. 4. Conclusion. Let $x$ be a unit eigenvector for $\lambda$, the largest eigenvalue of $A$. Add the first bound and twice the second at $y=x$, then use step 2 and $(Ad)_u=m-Z_u$: $3\lambda^2\le\sum_u x_u^2\bigl[m+Z_u+2(A^4)_{uu}/d(u)\bigr]$. Therefore $\sum_u x_u^2\,\overline D_u=3m-\sum_u x_u^2\bigl[m+Z_u+2(A^4)_{uu}/d(u)\bigr]\le3\xi$. Some vertex $u$ has $\overline D_u\le3\xi$, and some neighbour $v$ of $u$ has $D_{uv}\le3\xi$. So $D(G)\le3\xi$. **Sharpness.** The five-cycle has $m=5$, $\lambda=2$, $\xi=1$ and $D(C_5)=3$. **Checks.** The Lean solution proves `TriangleFreeEdit.editDistance_le_three_deficit` with Lean v4.35.0 and Mathlib v4.35.0. `lake comparator --paranoid` accepted it against the formal statement in Lean's kernel and in five further checkers (Lean's paranoid kernel, lean4lean, nanoda, con-leche, con-ron); `#print axioms` lists only `propext`, `Classical.choice` and `Quot.sound`. Every step of the proof was also checked numerically on 2,918 triangle-free graphs. The full write-up is the paper `attempts/triangle-free-spectral-stability/paper/main.pdf` in the same repository. **How the proof was found.** By the math-solver harness of exactory on 24 October 2026. Claude Fable 5.1 wrote the proof, Claude Opus 5.5 reviewed it independently, and gpt-6-astra reviewed it adversarially. The Lean proof was written by OpenAI Codex with gpt-6-astra. No human mathematician has reviewed the proof yet.

  Write-up

  None

  Lean solution

  https://github.com/exactory/exactory-math/tree/7194c5784dba0cfe43dd5951f65e62f1b9c9456e/attempts/triangle-free-spectral-stability/leanTargets formal statement version 1, the current version.

  Lean checks

  No account reports a Lean check yet.