A Proof of Graffiti 290:
Second-Smallest Adjacency Eigenvalues and Size over Mean Gravity

Nathan Wilbanks and Annie

AGNT Labs

Research Report · July 23, 2026 · revised October 7, 2026 (§2.5–2.6, uniform argument and Lean 4 proof)

Artifacts & evidence set · SHA256SUMS · Manuscript · Lean proof · Companion: Graffiti 292

Abstract

We prove Graffiti 290: for every connected simple graph $G$ of order $n$ and girth at least five, \[ -\lambda_{n-1}(A)\;\le\;\frac{m}{\overline{\operatorname{Gr}}}, \] where $\lambda_{n-1}$ is the second-smallest adjacency eigenvalue, $m$ is the number of edges, and $\overline{\operatorname{Gr}}$ is the mean of the gravity matrix over all $n^2$ entries. The proof actually gives the stronger statement $\max_i |\lambda_i(A)| \le m/\overline{\operatorname{Gr}}$. The chain is the same three lemmas used for Graffiti 292 — a degree-sum bound on mean gravity, the trace identity $\operatorname{tr}(A^2)=2m$, and Reiman's $C_4$-free edge bound — closed by a quartic $Q(t)$ whose shift $Q(u+5)$ has exclusively positive coefficients. Orders $n\le 7$ are dispatched by exact rational arithmetic. Verification uses four independent batteries — symbolic reduction, exact exhaustive small cases (34 girth-$\ge 5$ graphs), a named-graph battery including Hoffman–Singleton, and a from-scratch independent reimplementation using LCF-constructed cages, random trees, and random girth-pruned graphs. A shorter uniform argument (§2.5) needs no edge cap, polynomial or small-case check: for girth at least five, both readings of the mean gravity are at most $1$, and every eigenvalue satisfies $|\lambda|\le\Delta\le m$. That argument is machine-checked in Lean 4 with Mathlib (§2.6), for both readings of the mean, using only Lean's standard axioms. Novelty is stated provisionally.

Status. All verification batteries pass, and the uniform argument of §2.5 is machine-checked in Lean 4 (§2.6). This is a complete proof, under the gravity matrix of Written on the Wall (p. 52), of a conjecture listed open by Roucairol–Cazenave (arXiv:2409.18626, September 2024). It has not yet received external peer review. A formal proof shows that the argument is correct for the stated definitions; it does not settle the intended reading of the original statement or priority. Historical priority is not claimed; see §6.

1. The conjecture

Let $G$ be a connected simple graph on $n$ vertices with adjacency matrix $A$ and edge set of cardinality $m$. Its gravity matrix (Brewster–Dinneen–Faber convention, reproduced by Roucairol–Cazenave and used verbatim in our companion Graffiti 292 proof) is

$$\operatorname{Gr}_{uv}=\begin{cases}0,&u=v,\\[3pt]\dfrac{d(u)\,d(v)}{(n-1)\,d(u,v)},&u\ne v,\end{cases}$$

and $\overline{\operatorname{Gr}}$ is the mean of all $n^2$ entries. Order the adjacency eigenvalues $\lambda_1 \ge \lambda_2 \ge \cdots \ge \lambda_n$; the second-smallest is $\lambda_{n-1}$. Graffiti 290 (page 79 of Fajtlowicz's Written on the Wall, statement verified by direct transcription of the scan) asserts:

Conjecture 290. If $G$ has girth at least five, then $-\lambda_{n-1}(A) \le m/\overline{\operatorname{Gr}}$.

As of September 2024 the conjecture was listed open in Roucairol–Cazenave's Table 1 after search algorithms (NMCS, LNMCS, NRPA, UCT, GBFS, BEAM, GRAVE, RAVE) failed to refute it. The paper's erratum notes that the Aouchiche–Hansen gravity convention would make 290 trivially refutable; the Written on the Wall definition (used here) blocks all such counterexamples.

2. The proof

Figure 1. Bounding chain for Graffiti 290. The 292 chain lifts verbatim by rescaling the right-hand side from $n/\overline{\operatorname{Gr}}$ to $m/\overline{\operatorname{Gr}}$; the terminal inequality becomes a quartic in $t=\sqrt{4n-3}$, which after the shift $t=u+5$ has strictly positive coefficients.

2.1 A degree-sum lower bound for $m/\overline{\operatorname{Gr}}$

Lemma 1. $\displaystyle \frac{m}{\overline{\operatorname{Gr}}}\;\ge\;\frac{n^2(n-1)}{4m}$.

Proof. Since $d(u,v)\ge 1$ for $u \ne v$, \[ \overline{\operatorname{Gr}} =\frac{1}{n^2(n-1)}\sum_{u\ne v}\frac{d(u)d(v)}{d(u,v)} \le\frac{1}{n^2(n-1)}\Bigl(\sum_v d(v)\Bigr)^{\!2} = \frac{4m^2}{n^2(n-1)}, \] and division by $m$ followed by reciprocation gives the claim. ∎

2.2 The trace bound

Lemma 2. Every adjacency eigenvalue satisfies $|\lambda|\le\sqrt{2m}$.

Proof. $\sum_i \lambda_i^2 = \operatorname{tr}(A^2) = 2m$. ∎

2.3 Reiman's extremal edge bound

Lemma 3. If $G$ has girth at least five (hence is $C_4$-free), then

$$m \le B(n) := \frac{n}{4}\bigl(1+\sqrt{4n-3}\bigr).$$

2.4 Closing the chain

Theorem. For every connected simple graph $G$ of order $n\ge 2$ and girth at least five, $\max_i |\lambda_i(A)|\;\le\;m/\overline{\operatorname{Gr}}$; a fortiori $-\lambda_{n-1}(A)\;\le\;m/\overline{\operatorname{Gr}}$.

Proof. By Lemma 2 it suffices to prove $\sqrt{2m}\le m/\overline{\operatorname{Gr}}$; by Lemma 1 it suffices that $\sqrt{2m}\le n^2(n-1)/(4m)$, i.e. $n^4(n-1)^2\ge 32 m^3$. The right side is monotone in $m$, so by Lemma 3 it suffices that $n^4(n-1)^2 \ge 32 B(n)^3$, which simplifies to \[ 2n(n-1)^2 \ge \bigl(1+\sqrt{4n-3}\bigr)^3.\tag{1} \] Substituting $t=\sqrt{4n-3}$, $n=(t^2+3)/4$ and clearing 32 gives \[ 32\bigl(2n(n-1)^2-(1+t)^3\bigr) = (t+1)^2\,Q(t),\qquad Q(t)=t^4-2t^3+4t^2-38t-29. \] Writing $t=u+5$ yields \[ Q(u+5) = u^4 + 18u^3 + 124u^2 + 352u + 256, \] whose coefficients are all strictly positive, so $Q(t)>0$ for every $t\ge 5$, i.e. every $n\ge 7$. The endpoints $n=5$ (value $108-20\sqrt{17}\approx 25.54$) and $n=6$ (value $236-24\sqrt{21}\approx 126.02$) are strictly positive by exact arithmetic. For $n\le 7$, all 34 connected girth-$\ge 5$ graphs are verified exactly (Sturm counts of the adjacency characteristic polynomial roots below the rational bound $-m/\overline{\operatorname{Gr}}$). ∎

The terminal quartic is the entire analytic content of the argument:

Q(t) = t^4 - 2 t^3 + 4 t^2 - 38 t - 29
Q(u+5) = u^4 + 18 u^3 + 124 u^2 + 352 u + 256    — all coefficients strictly positive
32(2n(n-1)^2 - (1+t)^3) = (t+1)^2 Q(t)
n=5 endpoint:  108 - 20 sqrt(17)  ≈  25.5379   > 0
n=6 endpoint:  236 - 24 sqrt(21)  ≈  126.0182  > 0

2.5 A uniform argument (added in revision, October 7, 2026)

Theorem (uniform form). For every graph $G$ with $n\ge2$ vertices, $m$ edges and girth at least five, every adjacency eigenvalue satisfies

$$|\lambda|\;\le\;\Delta(G)\;\le\;m\;\le\;\frac{m}{\overline{\operatorname{Gr}}},$$

for the mean over all $n^2$ entries and for the mean over the $n(n-1)$ off-diagonal entries. In particular $-\lambda_{n-1}\le m/\overline{\operatorname{Gr}}$. Connectivity is not used, and there is no edge cap, polynomial or small-case check.

Proof. Girth at least five rules out triangles and four-cycles. As in §2.5 of the Graffiti 292 paper, this gives $\sum_v d(v)^2\le n(n-1)$, and Cauchy–Schwarz gives $(2m)^2\le n\sum_v d(v)^2\le n^2(n-1)$. Since $d(u,v)\ge1$ off the diagonal, \[ \sum_{u\ne v}\operatorname{Gr}_{uv}\;\le\;\frac{1}{n-1}\sum_{u\ne v}d(u)d(v)\;=\;\frac{(2m)^2-\sum_v d(v)^2}{n-1}\;\le\;\frac{(2m)^2-(2m)^2/n}{n-1}\;=\;\frac{(2m)^2}{n}. \] So the mean over all $n^2$ entries is at most $(2m)^2/n^3\le(n-1)/n<1$, and the off-diagonal mean is at most $(2m)^2/(n^2(n-1))\le1$. An eigenvector's largest coordinate gives $|\lambda|\le\Delta(G)$, and $\Delta(G)\le m$. If $m=0$, every eigenvalue is $0$ and both sides are $0$. Otherwise $0<\overline{\operatorname{Gr}}\le1$, so $m\le m/\overline{\operatorname{Gr}}$. ∎

Attribution. The counting bound $\sum_v d(v)^2\le n(n-1)$ and the observation that the mean gravity is at most $1$ come from the uniform argument for Graffiti 292, which that paper credits to Spanky McDoob. New here: subtracting the diagonal, which covers the off-diagonal reading of the mean, and the step $|\lambda|\le\Delta\le m$. The argument of §§2.1–2.4 is retained as an independent companion and is the object of batteries 1–4 of §3.

2.6 A machine-checked proof in Lean 4 (added in revision, October 7, 2026)

We formalized the argument of §2.5 in Lean 4 with Mathlib. Lean's kernel checks every inference. The source is on GitHub at agnt-gg/graffiti-lean (commit cceea87) and in the archive.

Degree, distance, girth and eigenvalues are Mathlib's own definitions: SimpleGraph.degree, SimpleGraph.dist, the extended girth SimpleGraph.egirth, and Matrix.IsHermitian.eigenvalues₀, the eigenvalues of the real adjacency matrix in decreasing order. Mathlib proves that this list is the sorted list of roots of the characteristic polynomial, with multiplicity. The only new definitions are the gravity matrix and its means. The main statement reads:

noncomputable def gravity (G : SimpleGraph α) [DecidableRel G.Adj] (u v : α) : ℝ :=
  if u = v then 0
  else (G.degree u * G.degree v : ℝ) / ((Fintype.card α - 1 : ℝ) * G.dist u v)

noncomputable def meanGravity (G : SimpleGraph α) [DecidableRel G.Adj] : ℝ :=
  (∑ u, ∑ v, G.gravity u v) / (Fintype.card α : ℝ) ^ 2

theorem graffiti_290 {α : Type*} [Fintype α] [DecidableEq α] (G : SimpleGraph α)
    [DecidableRel G.Adj] (hconn : G.Connected) (hgirth : 5 ≤ G.egirth)
    (hn : 2 ≤ Fintype.card α) :
    -(G.isHermitian_adjMatrix ℝ).eigenvalues₀ ⟨Fintype.card α - 2, by omega⟩ ≤
      G.edgeFinset.card / G.meanGravity

**Table 3.** Theorems proved in Lean.
Theorem	Statement
`graffiti_290`	Graffiti 290, with the mean over all $n^2$ entries of the gravity matrix.
`graffiti_290.variants.off_diagonal_mean`	Graffiti 290, with the mean over the $n(n-1)$ off-diagonal entries.
`graffiti_290.variants.abs_le`	Every eigenvalue: $\|\lambda\|\le m/\overline{\operatorname{Gr}}$, without connectivity.

Fidelity to the source.

Statement. Page 79 reads "If girth is ≥ 5 then the − 2nd smallest eigenvalue ≤ size / meangravity." The size of a graph is its number of edges.
Second-smallest eigenvalue. eigenvalues₀ is indexed from $0$ in decreasing order, so $\lambda_{n-1}$ has index $n-2$. The hypothesis $n\ge2$ makes it exist.
Gravity. On p. 52 an entry is $0$ when no path joins $u$ and $v$. Mathlib's dist is $0$ for such a pair and Lean defines $x/0=0$, so the Lean entry is also $0$.
Eigenvalues and connectivity. Eigenvalues are those of the adjacency matrix unless stated otherwise (p. 1), and conjectures that involve distance are only for connected graphs (p. 2). Hence the hypothesis G.Connected.
Girth. An acyclic graph has egirth = ⊤, so it satisfies the girth hypothesis, as trees do in the source.
Mean. The source does not define the mean of a matrix, so both readings are proved.

What was checked.

The project builds with lake build on Lean v4.33.1 with Mathlib v4.33.1 (commit 0df444a), with warnings treated as errors.
For all three theorems, #print axioms reports only propext, Classical.choice and Quot.sound, Lean's standard axioms. There is no sorry, no custom axiom and no native_decide.
Negative controls: with the girth hypothesis weakened from 5 to 4, the proof fails; with the gravity bound tightened from $(2m)^2/n$ to $(2m)^2/n^2$, which $K_2$ violates, the proof fails.
Battery 5 checks every inequality of §2.5 in exact rational arithmetic on 345 graphs of girth at least five, including all 34 connected ones with $n\le7$. The bound $\sum\operatorname{Gr}\le(2m)^2/n$ holds with equality for $K_2$.

As with any Mathlib proof, this check trusts the Lean kernel and the Mathlib definitions above. Mathlib's prebuilt library files were loaded, not rebuilt from source.

3. Verification architecture

Six verification batteries. Batteries 1–4 check the argument of §§2.1–2.4, with no shared code between the primary certifiers and the independent reimplementation. Battery 5 checks the uniform argument of §2.5, and battery 6 is the Lean kernel (§2.6). A failure at any battery would block publication.

**Table 1.** Verification batteries and outcomes.
Battery	Method	Coverage	Status
1. Named-graph battery	exact gravity means (rational) + numeric spectra	C₅, C₆, C₇, Petersen, Heawood, Pappus, Desargues, Möbius–Kantor, dodecahedron, Hoffman–Singleton, path P₁₀, star K₁,₉, spider (3,3,3), McGee 7-cage, Tutte–Coxeter 8-cage	PASS
2. Symbolic reduction	SymPy exact factorization	factorization $(t+1)^2 Q(t)$, shifted coefficients [1, 18, 124, 352, 256], exact endpoints n=5, 6	PASS
3. Exhaustive exact small cases	exact rational gravity + Sturm root counts of adjacency characteristic polynomial	all 34 connected girth ≥ 5 graphs with 2 ≤ n ≤ 7 from the graph atlas	PASS
4. Independent reimplementation	from-scratch: LCF cages, hand-rolled Hoffman–Singleton (pentagon/pentagram), separate gravity accumulator	HS, Petersen, Heawood, C₅, K₂, K₁,₂₀, McGee, Tutte–Coxeter, 60 random trees (2 ≤ n ≤ 60), 40 random girth-pruned graphs	PASS
5. Uniform bound	exact rational gravity sums, numeric spectra	345 girth ≥ 5 graphs: 11 named, all 34 connected ones with n ≤ 7, 300 random; every inequality of §2.5	PASS
6. Formal proof	Lean 4 kernel with Mathlib	the uniform argument of §2.5 for every graph of girth at least five, both readings of the mean; standard axioms only	PASS

4. Exact certificates

4.1 Named-graph margins

Every entry is derived from an exact rational gravity mean; the last column reports the certified inequality margin $m/\overline{\operatorname{Gr}} - (-\lambda_{n-1})$. Positive means the bound holds; the strong pattern is that the margin grows quickly with $n$.

**Table 2.** Exact gravity means, second-smallest adjacency eigenvalue, and inequality margin.
Graph	n	m	−λₙ₋₁	m / Gr	margin
C₅	5	5	1.6180	8.333	+6.715
C₆	6	6	1.0000	13.500	+12.500
C₇	7	7	1.8019	20.045	+18.244
Petersen	10	15	2.0000	25.000	+23.000
Heawood (6-cage)	14	21	1.4142	57.909	+56.495
Möbius–Kantor	16	24	1.7321	80.842	+79.110
Pappus	18	27	1.7321	108.000	+106.268
Desargues	20	30	2.0000	141.527	+139.527
McGee (7-cage)	24	36	2.3429	210.286	+207.943
Tutte–Coxeter (8-cage)	30	45	2.0000	362.500	+360.500
Hoffman–Singleton	50	175	3.0000	312.500	+309.500

4.2 The exhaustive small-order check

All 34 connected simple graphs of order $2\le n\le 7$ with girth at least five (path graphs, trees of every shape, C₅, C₆, C₇, and the small trees on 7 vertices) are enumerated from NetworkX's graph atlas. For each graph, the gravity mean is computed as an exact rational number $m/\overline{\operatorname{Gr}}\in\mathbb{Q}$, and the adjacency characteristic polynomial is passed to SymPy's Sturm-based root counter to count roots strictly below $-m/\overline{\operatorname{Gr}}$. The inequality $-\lambda_{n-1}\le m/\overline{\operatorname{Gr}}$ holds exactly when at most one root lies strictly below $-m/\overline{\operatorname{Gr}}$. In all 34 graphs, no root lies there.

4.3 Independent reimplementation highlights

The Battery 4 script constructs the Hoffman–Singleton graph by the classical pentagon/pentagram recipe — five pentagons $P_h$, five pentagrams $Q_h$, with joins $P_{h,i} \sim Q_{k,\,hk+i\bmod 5}$ — and separately verifies via A² and A³ that the graph is 7-regular, triangle-free, C₄-free, and contains a 5-cycle (hence girth 5). It uses its own gravity accumulator (no reuse of Battery 1's code) and its own path/cage constructions via LCF notation. Every check for 290 passes, including on 60 random trees generated by networkx.random_labeled_tree and 40 random girth-pruned graphs.

5. Companion result and mechanism sharing

Graffiti 290 falls out of the exact chain that settles Graffiti 292 (companion whitepaper, a-proof-of-graffiti-292.html). Because the 292 terminal already proves $n/\overline{\operatorname{Gr}} \ge \sqrt{2m}$ for $n\ge 7$, whenever $m \ge n$ the 290 target $m/\overline{\operatorname{Gr}}$ exceeds $n/\overline{\operatorname{Gr}}\ge\sqrt{2m}\ge |\lambda|$ automatically. The quartic $Q(t)$ above absorbs the remaining sparse cases (trees, forests, unicyclic girth-$\ge 5$ graphs where \(m

6. Novelty status — stated provisionally

Priority. A targeted search across arXiv (including the September 2024 Roucairol–Cazenave paper and its citation graph), the Aouchiche–Hansen distance-spectra survey (LAA 458, 2014, which discusses adjacent conjectures but not 290), MathOverflow, GitHub, Zenodo, and the Brewster–Dinneen–Faber corpus locates no prior resolution. Self-echo (our own indexed artifacts and the CE10 tokiwa transcript, which was pursuing counterexamples not proofs) was excluded from the priority search. A recheck on October 7, 2026 found no resolution of 290 in Google DeepMind's formal-conjectures repository (issues and pull requests), in a GitHub repository search, in the agent-driven catalog jzone3/solving-math-problems, or on arXiv. We therefore report a complete, machine-checked proof that appears to be the first publicly documented one under the Written on the Wall gravity matrix; we do not claim historical priority. Expert review of statement fidelity, the exact convention, and prior art is invited.

7. Reproduction protocol

python -m pip install sympy networkx numpy
python verify_290_symbolic.py         # factorization, shift positivity, endpoints
python verify_290_small_cases.py      # exhaustive n≤7, exact rational gravity, Sturm counts
python independent_check_284_290.py   # independent reimplementation, 60 trees + 40 pruned
python battery_290.py                 # uniform bound (§2.5): 345 graphs, exact rational sums

# Lean (§2.6): in the lean/ folder of the archive, or a clone of agnt-gg/graffiti-lean
lake exe cache get                    # prebuilt Mathlib
lake build                            # checks the proofs and prints their axioms

Dependencies: Python 3.13, SymPy 1.14, NetworkX 3.5, NumPy 2.3; for §2.6, Lean v4.33.1 and Mathlib v4.33.1, both pinned in the Lean files. Exact arithmetic on the decisive rung; floating point is only used for numeric spectra in the named-graph table.

8. Artifact ledger

Artifact	Purpose
manuscript-graffiti-290.md	Markdown proof with full derivations
verify_290_symbolic.py · output	Symbolic reduction: (t+1)²Q(t), shift positivity, endpoints
verify_290_small_cases.py · output	Exhaustive small-case + named-graph batteries (exact rational gravity, Sturm root count)
independent_check_284_290.py · output	Independent reimplementation (shared with the 284 refutation package)
battery_290.py · output	Uniform bound (§2.5): exact checks on 345 graphs
agnt-gg/graffiti-lean · archived copy	Lean 4 proof (§2.6), with the shared gravity definitions and lemmas
claim-ledger.json	Claim-by-claim evidence map (covers 290 proof + 284 refutation verification + 295 attack state)
wow-p79-bot.png	Primary source scan of the page-79 conjecture statement
SHA256SUMS.txt	Integrity ledger

References

S. Fajtlowicz, "Written on the Wall," July 2004, p. 79 (conjecture 290); p. 52 (gravity matrix definition).
M. Roucairol and T. Cazenave, "Refutation of Spectral Graph Theory Conjectures with Search Algorithms," arXiv:2409.18626, 2024 (open-status table; erratum §5.2 on gravity conventions).
T. L. Brewster, M. J. Dinneen, and V. Faber, "A computational attack on the conjectures of Graffiti: new counterexamples and proofs," Discrete Mathematics 147 (1995), 35–55.
M. Aouchiche and P. Hansen, "Distance spectra of graphs: a survey," Linear Algebra and its Applications 458 (2014), 301–386.
I. Reiman, "Über ein Problem von K. Zarankiewicz," Acta Math. Acad. Sci. Hungar. 9 (1958), 269–273.
O. Favaron, M. Mahéo, and J.-F. Saclé, "Some eigenvalue properties in graphs (conjectures of Graffiti — II)," Discrete Mathematics 111 (1993), 197–220.
AGNT Labs, "A Proof of Graffiti 292," July 23, 2026, companion whitepaper.
N. Wilbanks and Annie, "graffiti-lean: Lean 4 proofs of Graffiti conjectures 290 and 292," GitHub, 2026, agnt-gg/graffiti-lean, commit cceea87.
L. de Moura and S. Ullrich, "The Lean 4 Theorem Prover and Programming Language," Automated Deduction – CADE 28, LNCS 12699 (2021), 625–635.
The mathlib Community, "The Lean Mathematical Library," Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), 367–381.

Bottom line. Graffiti 290 is proved for every connected simple graph of girth at least five, in the stronger form $\max_i |\lambda_i(A)| \le m/\overline{\operatorname{Gr}}$. The proof is a three-lemma chain lifted verbatim from the Graffiti 292 argument; the terminal inequality reduces to a quartic with strictly positive shifted coefficients. A shorter uniform argument (§2.5) gives the same result for both readings of the mean, and it is machine-checked in Lean 4 (§2.6). Six verification batteries pass. Novelty is reported provisionally; priority is not claimed.

This is what the product is for

AGNT Labs publishes its working out. The same discipline runs through the product: every agent run produces a receipt showing what it did, what it read, and why — so a result can be checked rather than trusted. AGNT runs on your own machine and is free to use.

Download AGNT free Read the other papers

A Proof of Graffiti 290:
Second-Smallest Adjacency Eigenvalues and Size over Mean Gravity

1. The conjecture

2. The proof

2.1 A degree-sum lower bound for \(m/\overline{\operatorname{Gr}}\)

2.2 The trace bound

2.3 Reiman's extremal edge bound

2.4 Closing the chain

2.5 A uniform argument (added in revision, October 7, 2026)

2.6 A machine-checked proof in Lean 4 (added in revision, October 7, 2026)

3. Verification architecture

4. Exact certificates

4.1 Named-graph margins

4.2 The exhaustive small-order check

4.3 Independent reimplementation highlights

5. Companion result and mechanism sharing

6. Novelty status — stated provisionally

7. Reproduction protocol

8. Artifact ledger

References

This is what the product is for

Stay in the loop.

Theorem	Statement
`graffiti_290`	Graffiti 290, with the mean over all \(n^2\) entries of the gravity matrix.
`graffiti_290.variants.off_diagonal_mean`	Graffiti 290, with the mean over the \(n(n-1)\) off-diagonal entries.
`graffiti_290.variants.abs_le`	Every eigenvalue: \(\|\lambda\|\le m/\overline{\operatorname{Gr}}\), without connectivity.

A Proof of Graffiti 290:Second-Smallest Adjacency Eigenvalues and Size over Mean Gravity

1. The conjecture

2. The proof

2.1 A degree-sum lower bound for \(m/\overline{\operatorname{Gr}}\)

2.2 The trace bound

2.3 Reiman's extremal edge bound

2.4 Closing the chain

2.5 A uniform argument (added in revision, October 7, 2026)

2.6 A machine-checked proof in Lean 4 (added in revision, October 7, 2026)

3. Verification architecture

4. Exact certificates

4.1 Named-graph margins

4.2 The exhaustive small-order check

4.3 Independent reimplementation highlights

5. Companion result and mechanism sharing

6. Novelty status — stated provisionally

7. Reproduction protocol

8. Artifact ledger

References

This is what the product is for

Stay in the loop.

A Proof of Graffiti 290:
Second-Smallest Adjacency Eigenvalues and Size over Mean Gravity