A Proof of Graffiti 292:
The Least Positive Eigenvalue of Girth-Five Graphs

Nathan Wilbanks and Annie

AGNT Labs

Research Report · July 23, 2026 · revised July 24, 2026 (§2.5) and October 7, 2026 (§2.6, Lean 4 formalization)

Artifacts & evidence set · SHA256SUMS · Proof PDF · Lean proof

Abstract

We prove Graffiti 292: for every connected simple graph $G$ of order $n$ and girth at least five, the least positive adjacency eigenvalue satisfies \[ \lambda_+(G)\;\le\;\frac{n}{\overline{\operatorname{Gr}}}, \] where the gravity matrix has off-diagonal entries $d(u)d(v)/((n-1)\,d(u,v))$, zero diagonal, and mean taken over all $n^2$ entries. The proof is a three-line argument. A degree-sum bound gives $n/\overline{\operatorname{Gr}}\ge (n-1)n^3/(4m^2)$; the trace identity $\operatorname{tr}(A^2)=2m$ gives $\lambda_+\le\sqrt{2m}$; and Reiman's $C_4$-free edge bound $m\le n(1+\sqrt{4n-3})/4$ closes the chain for every $n\ge7$ via a polynomial whose shifted form has exclusively positive coefficients. Small orders are dispatched by exact exhaustive computation with rational root isolation. The package includes four independent verification batteries — exact gravity means on named cages, symbolic reduction, exact small-case enumeration, and a from-scratch independent reimplementation over 18,686 labeled graphs through order seven — plus full source scans, scripts, run logs, technical vector figures, and SHA-256 hashes. The uniform argument of §2.5 is also machine-checked in Lean 4 with Mathlib (§2.6), for both readings of the mean of the gravity matrix, using only Lean's standard axioms. Novelty is stated provisionally: we found no prior resolution in the indexed literature, but priority is not claimed pending expert review.

Status. The proof and all executable checks pass, and the 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); it has not yet received external mathematical 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$. Its gravity matrix 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}$$

where $d(u)$ is degree, $d(u,v)$ is graph distance, and $\overline{\operatorname{Gr}}$ is the mean of all $n^2$ entries (diagonal zeros included). Graffiti 292 (page 80 of Fajtlowicz's Written on the Wall) asserts that if $G$ has girth at least five, then the least positive adjacency eigenvalue obeys

$$\lambda_+(G)\;\le\;\frac{n}{\overline{\operatorname{Gr}}}.$$

As of the September 2024 Roucairol–Cazenave search survey, the conjecture was listed open after an exhaustive spectral search across cages, incidence graphs of projective planes, and random regular graphs of girth at least five.

2. The proof

Figure 1. Bounding chain structure for Graffiti 292. The problem splits into an algebraic lower bound $L(n)$ derived from distance contraction and Reiman's edge cap, compared against the spectral trace upper bound $R(n) = \sqrt{2B(n)}$.

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

Lemma 1. If $G$ has $m$ edges, then

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

Proof. Since $d(u,v)\ge1$ 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)}\sum_{u\ne v}d(u)d(v) \le\frac{(2m)^2}{n^2(n-1)}=\frac{4m^2}{n^2(n-1)}. \] Taking reciprocals yields the claim. ∎

2.2 The trace bound

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

Proof. If $\lambda_1,\dots,\lambda_n$ are the adjacency eigenvalues, then $\sum_i\lambda_i^2=\operatorname{tr}(A^2)=2m$. ∎

Figure 2. Geometric containment mechanism. The adjacency eigenvalue vector lies on the radius-$r=\sqrt{2m}$ sphere in $\mathbb{R}^n$ by the trace energy identity $\operatorname{tr}(A^2) = 2m$. For $n \ge 7$, Reiman's $C_4$-free edge bound prevents $r$ from expanding fast enough to reach the outer gravity boundary $R = n / \overline{\operatorname{Gr}}$, guaranteeing $\lambda_+(G) \le R$.

2.3 Reiman's extremal edge bound

Lemma 3. If $G$ contains no four-cycle, then

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

A graph of girth at least five has no triangles or four-cycles, so the bound applies.

2.4 Closing the chain

Theorem. Graffiti 292 is true.

Proof. For $n\ge7$, set $t=\sqrt{4n-3}$, so $n=(t^2+3)/4$ and $t\ge5$. The left side of \[ \frac{(n-1)n^3}{4B(n)^2}\ge\sqrt{2B(n)}\tag{1} \] decreases with $m$ while the right side increases, so Lemma 3 reduces the comparison to (1). Both sides are positive. Squaring (1), substituting $n=(t^2+3)/4$, and clearing positive denominators reduces (1) to $P(t)>0$, where \[ P(t)=2(t+1)^2\left(t^4-4t^3-2t^2-12t+1\right). \] Writing $t=u+5$ gives, by direct expansion, \[ P(u+5)=2u^6+56u^5+632u^4+3600u^3+10400u^2+12480u+1152>0 \] for every $u\ge0$. Hence, by Lemmas 1–3, \[ \frac{n}{\overline{\operatorname{Gr}}} \ge\frac{(n-1)n^3}{4m^2} \ge\sqrt{2m} \ge\lambda_+(G). \] For $n\le6$, every connected simple graph of girth at least five is among the finite cases checked exactly below (the verifier covers all qualifying graphs through order seven). ∎

Figure 3. Analytical comparison of $L(n)$ and $R(n)$ for $n \in [2, 20]$. For $n \ge 7$, $L(n) > R(n)$ strictly. As $n \to \infty$, $L(n)$ grows as $\Theta(n)$ while $R(n)$ grows as $\Theta(n^{3/4})$, establishing asymptotic divergence.

The terminal polynomial is the final analytic step of the argument. Its factored and expanded forms, exact endpoint value, and shifted coefficient list are machine-verified:

cleared(t) = 2(t+1)^2 (t^4 - 4t^3 - 2t^2 - 12t + 1)
           = 2 t^6 - 4 t^5 - 18 t^4 - 40 t^3 - 50 t^2 - 20 t + 2
cleared(5) = 1152
cleared(t = u + 5) coefficients: [2, 56, 632, 3600, 10400, 12480, 1152]  — all strictly positive

Figure 4. Coefficient spectrum of the shifted polynomial $P(u+5) = 2u^6 + 56u^5 + 632u^4 + 3600u^3 + 10400u^2 + 12480u + 1152$. Because every coefficient $c_k > 0$, $P(u+5) > 0$ for every $u \ge 0$; equivalently, the shifted polynomial has no nonnegative real root (Descartes' rule likewise gives no positive root).

2.5 A stronger, uniform bound (added in revision, July 24, 2026)

Theorem (uniform form). For every connected simple graph $G$ of order $n\ge2$ and girth at least five,

$$\lambda_+(G)\;\le\;n-1\;<\;n\;\le\;\frac{n}{\overline{\operatorname{Gr}}},$$

so Graffiti 292 holds with strict inequality, uniformly in $n$ — with no edge-cap, no trace bound, no polynomial, and no finite case split.

Proof. A graph of girth at least five has no triangle and no four-cycle. Count the paths of length two ("cherries"): there are $\sum_v\binom{d(v)}{2}$ of them. Triangle-freeness makes the two endpoints of each cherry non-adjacent; $C_4$-freeness means a non-adjacent pair has at most one common neighbour, so distinct cherries have distinct endpoint pairs. Hence cherries inject into non-edges: \[ \sum_v\binom{d(v)}{2}\;\le\;\binom{n}{2}-m. \] By Cauchy–Schwarz, $\sum_v d(v)^2\ge(\sum_v d(v))^2/n=4m^2/n$, so $\sum_v\binom{d(v)}{2}=\tfrac12\sum_v d(v)^2-m\ge \tfrac{2m^2}{n}-m$. Combining the two, \[ \frac{2m^2}{n}-m\;\le\;\frac{n(n-1)}{2}-m\qquad\Longrightarrow\qquad 4m^2\le n^2(n-1). \] Feeding this into Lemma 1 (unchanged), \[ \frac{n}{\overline{\operatorname{Gr}}}\;\ge\;\frac{(n-1)n^3}{4m^2}\;\ge\;\frac{(n-1)n^3}{n^2(n-1)}\;=\;n, \] that is $\overline{\operatorname{Gr}}\le1$. Finally every adjacency eigenvalue obeys $\lambda_+\le\rho(A)\le\Delta(G)\le n-1$. Chaining gives \(\lambda_+\le n-1

Attribution. This uniform argument was pointed out by Spanky McDoob (@59thProfile, private communication, July 2026). The counting inequality $\sum_v\binom{d(v)}{2}\le\binom{n}{2}-m$ and its consequence $4m^2\le n^2(n-1)$ are the classical Kővári–Sós–Turán / Reiman cherry-count; McDoob's contribution is the observation that this cruder bound composes with Lemma 1 to settle Graffiti 292 directly and in the strict form above, bypassing Reiman's sharp cap, the terminal polynomial, the $n\ge7$ crossover, and the finite small-case check of §§2.3–4. The Reiman-based argument of §§2.1–2.4 is retained as an independent, sharper-constant companion and is the object of the Python batteries of §3. The uniform argument is the one formalized in Lean (§2.6). The uniform bound is verified exactly (symbolic reduction, exhaustive atlas $n\le7$, and exact named cages) in verify_twopath_292.py.

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, so this proof does not depend on the Python batteries of §3. The source is Graffiti292.lean, also on GitHub at agnt-gg/graffiti-292-lean (commit 5e63379). The statement, with a link to this proof, is submitted to Google DeepMind's formal-conjectures repository as pull request #6901. The definitions have since moved to a shared file, SimpleGraph.gravity, which Graffiti 290 also uses; the current proofs of both conjectures are at agnt-gg/graffiti-lean (commit cceea87), with the same statements.

Degree, distance, girth and eigenvalues are Mathlib's own definitions: SimpleGraph.degree, SimpleGraph.dist, the extended girth SimpleGraph.egirth, and Matrix.IsHermitian.eigenvalues of the real adjacency matrix. The only new definitions are the gravity matrix and its mean. The main statement reads:

noncomputable def gravity {α : Type*} [Fintype α] [DecidableEq α] (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 {α : Type*} [Fintype α] [DecidableEq α] (G : SimpleGraph α)
    [DecidableRel G.Adj] : ℝ :=
  (∑ u, ∑ v, gravity G u v) / (Fintype.card α : ℝ) ^ 2

theorem graffiti_292 {α : Type*} [Fintype α] [DecidableEq α] (G : SimpleGraph α)
    [DecidableRel G.Adj] (hconn : G.Connected) (hgirth : 5 ≤ G.egirth) (i : α)
    (hpos : 0 < (G.isHermitian_adjMatrix ℝ).eigenvalues i)
    (hleast : ∀ j, 0 < (G.isHermitian_adjMatrix ℝ).eigenvalues j →
      (G.isHermitian_adjMatrix ℝ).eigenvalues i ≤ (G.isHermitian_adjMatrix ℝ).eigenvalues j) :
    (G.isHermitian_adjMatrix ℝ).eigenvalues i ≤ Fintype.card α / meanGravity G

The index i selects the least positive eigenvalue: hpos says that it is positive, and hleast says that no positive eigenvalue is smaller.

**Table 3.** Theorems proved in Lean.
Theorem	Statement
`graffiti_292`	Graffiti 292, with the mean over all $n^2$ entries of the gravity matrix.
`graffiti_292.variants.off_diagonal_mean`	Graffiti 292, with the mean over the $n(n-1)$ off-diagonal entries.
`graffiti_292.variants.strict`	The uniform form of §2.5: $\lambda_+\le n-1$ and $n\le n/\overline{\operatorname{Gr}}$, without connectivity.

Fidelity to the source.

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. The source also counts trees: the counterexamples to conjecture 293, on the same page, are trees.
Mean. The source does not define the mean of a matrix, so both readings are proved.
Degenerate cases. A graph with no edges has no positive eigenvalue, so the statement makes no claim about it. The division $n/\overline{\operatorname{Gr}}$ is never by zero in a case the statement covers.

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. The proof file also checks with no warnings on Lean v4.32.2 with Mathlib v4.32.2.
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 control: with the girth hypothesis weakened from 5 to 4, the proof fails at the 4-cycle step.
Two checks pin the definitions: the mean gravity of $K_2$ is exactly $1/2$, and $K_2$ satisfies the hypotheses.

The formal proof follows §2.5 with two changes of presentation. It proves the counting bound $\sum_v d(v)^2\le n(n-1)$ by neighbourhoods: for each vertex $a$, the sets $N(v)\setminus\{a\}$ with $v\in N(a)$ are pairwise disjoint (no 4-cycle) and miss $N(a)\cup\{a\}$ (no triangle). It proves $\lambda\le\Delta(G)$ from the largest coordinate of an eigenvector. Connectivity is not used.

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

Five verification batteries. Batteries 1–4 are Python, and the two reimplementations share no code. Battery 5 is the Lean kernel (§2.6). A failure in any battery would block publication.

**Table 1.** Verification batteries and outcomes.
Battery	Method	Coverage	Status
1. Named-graph evaluator	exact gravity means + float spectra	paths, cycles, Petersen, Heawood, Pappus, Desargues, Möbius–Kantor, Hoffman–Singleton, random regular girth ≥ 5, graph atlas ≤ 7	PASS
2. Symbolic reduction	SymPy exact factorization	cleared polynomial, expansion, derivative, endpoint 1152, shifted coefficients	PASS
3. Exact small-case enumeration	characteristic polynomials + rational root isolation	all 35 connected girth ≥ 5 graphs through order 7	PASS
4. Independent reimplementation	from-scratch, no shared code: exact-integer inequality, hand-rolled graph engine, Fano-plane and Hoffman–Singleton constructions	analytic bound at n = 7..199, 10³, 10⁴, 10⁵, 10⁶; exhaustive over all connected girth ≥ 5 graphs on n ≤ 6 (1,874 labeled) plus all n = 7 trees, cycles, and unicyclic graphs — 18,686 labeled graphs in total, dominated by the 16,807 labeled 7-vertex trees; the one bicyclic n = 7 class is covered by the atlas battery, and n = 7 is in any case covered by the analytic argument (t = 5); four named cages	PASS
5. 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 cages (exact gravity means, verified margins)

**Table 2.** Exact gravity means and verified inequality margins. The margin is $\lambda_+ - n/\overline{\operatorname{Gr}}$; strict negativity is required for the bound to hold with room.
Graph	n	m	girth	$\lambda_+$	$n/\overline{\operatorname{Gr}}$	margin
$C_5$	5	5	5	0.618034	8.333333	−7.715299
Petersen	10	15	5	1.000000	16.666667	−15.666667
Heawood	14	21	6	1.414214	38.606061	−37.191847
Hoffman–Singleton	50	175	5	2.000000	89.285714	−87.285714
cycle $C_{17}$	17	17	17	0.184537	212.667543	−212.483006
path $P_{10}$	10	9	∞	0.284630	68.229405	−67.944775
random 3-reg (n = 30, girth 5)	30	45	5	0.154525	251.275633	−251.121108

4.2 The exhaustive small-order check

The independent reimplementation enumerates all connected simple graphs on $n\le6$ vertices by edge subsets (1,874 labeled girth-at-least-five graphs), plus all trees, cycles, and unicyclic graphs on 7 vertices (a further 16,812, dominated by the 16,807 labeled 7-vertex trees) — 18,686 labeled graphs in total — and checks the conjecture exactly: the gravity mean is computed as an exact rational number, the characteristic polynomial is exact, and least positive roots are isolated with rational intervals of width $10^{-18}$. No graph violates the bound. The separate graph-atlas battery independently checks all 35 qualifying graphs through order 7 with the same exact arithmetic.

5. What the proof uses, and why it was not found by search

The 2024 search programs attacked the conjecture spectrally: they computed gravity and spectra for thousands of graphs and found the bound holding everywhere — which is consistent with truth, but gives no proof. The actual argument needs no graph-specific spectral computation. It bounds the gravity mean by a degree sum, bounds every eigenvalue by the trace identity, and lets Reiman's edge bound compare the two. The extremal high-girth graphs that matter for search (the cages) sit far inside the bound, so no search over a finite range of orders could confirm the universal statement — and, the bound being true, none found a counterexample. The conjecture was open because the three lemmas lived in different literatures: gravity matrices (Brewster–Dinneen–Faber), spectral trace identities, and extremal graph theory.

6. Novelty status — stated provisionally

Priority. A targeted search across arXiv, journal indexes, MathOverflow, GitHub, Zenodo, and the Graffiti/Roucairol–Cazenave corpus located no prior resolution of Graffiti 292 and no proof using this reduction. The numbered conjectures carry ambiguous conventions: the erratum in §5.2 of the 2024 search paper notes that the Aouchiche–Hansen survey defines both the gravity matrix and the "range" differently from Written on the Wall. This report uses the page-80 statement and the page-52 gravity matrix, which the search paper and Brewster–Dinneen–Faber reproduce. We therefore report a complete, machine-checked proof that appears new relative to the sources reviewed — not a claim of world-first priority. Independent expert review of (i) the historical statement, (ii) the reading of the mean of the gravity matrix (both the $n^2$ and the $n(n-1)$ readings are proved in §2.6), and (iii) prior art is invited before any stronger novelty claim.

7. Reproduction protocol

Everything needed to reproduce this report is in the artifact archive. One command per battery:

python attack_graffiti_292.py          # named graphs + atlas ≤ 7: exact gravity, margins
python verify_symbolic_292.py          # cleared polynomial factorization, endpoint, shift
python verify_small_cases_exact.py     # exact charpoly/root isolation, atlas ≤ 7
python verify_independent_292.py       # from-scratch: 18,686 graphs + analytic bound + cages
python verify_twopath_292.py           # stronger uniform bound (§2.5): cherry-count + Lemma 1, exact
python make_sha256.py                  # regenerate SHA256SUMS.txt

# Lean (§2.6): put Graffiti292.lean, lakefile.toml, lake-manifest.json and lean-toolchain in one folder
lake exe cache get                     # prebuilt Mathlib
lake build                             # checks the proof and prints the axioms of the three theorems

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 throughout; floating point is used only for spectra in the named-graph battery, never for the inequality itself.

8. Artifact ledger

Artifact	Purpose
manuscript-graffiti-292.pdf	typeset proof (2 pages, XeLaTeX)
manuscript-graffiti-292.tex	LaTeX source
attack_graffiti_292.py / output	named-graph battery
verify_symbolic_292.py / output	symbolic reduction battery
verify_small_cases_exact.py / output	exact small-case battery
verify_independent_292.py / output	independent reimplementation (18,686 labeled graphs through order seven)
verify_twopath_292.py / output	stronger uniform bound (§2.5): cherry-count, exact atlas + cages
Graffiti292.lean	Lean 4 proof (§2.6)
lakefile.toml / lake-manifest.json / lean-toolchain	Lean project files: pinned Lean and Mathlib versions
claim-ledger.json	claim-by-claim evidence map
wow-july2004.pdf / page80-detail.txt	primary source scan and OCR of the statement
SHA256SUMS.txt	integrity ledger

Principal hashes at publication time:

Artifact	SHA-256
manuscript (markdown)	06f6c3112e3b443678745959dc303a6ed1e2c81dd6177dfb5c7572b1be0de4b6
independent verifier	8117c135e9a28be85ecb050aa5a463dfab1786fd3b29ec3bc92ac6ac229e9869
independent verifier output	83496f7e53eaffd67248a65f6cba0df783553e0ce74f966de06d2a2728db7611
symbolic verifier output	7e621ffac638e0ce26a95b513aa700c496dca056e2dffb12f6cc92f88e839da7
Lean proof (Graffiti292.lean)	952a5c78876818a8c2ad5c51617e7cf792e8dd6206c604ed168d0ffc74e8370f
source scan (Written on the Wall)	d2c779d2c28418b30ab1b4f84bf7112c0e000bca1f2d6a3c48d0baba78af7733

Acknowledgments

We thank Spanky McDoob (@59thProfile) for the stronger uniform argument recorded in §2.5, and for corrections to the exposition (the asymptotic growth rate of $L(n)$, the statement of the polynomial-positivity step, the containment-figure wording, and the labeled-graph counts of §§3–4).

References

S. Fajtlowicz, "Written on the Wall," July 2004, p. 80 (conjecture 292); page 52 (gravity matrix definition).
M. Roucairol and T. Cazenave, "Refutation of Spectral Graph Theory Conjectures with Search Algorithms," arXiv:2409.18626, 2024 (Table 1, open status; §5.2, the gravity matrix of Written on the Wall, p. 52, and Brewster–Dinneen–Faber).
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.
S. Jukna, Extremal Combinatorics, §2.2 "Graphs with no 4-cycles" (Reiman-type edge bound).
I. Reiman, "Über ein Problem von K. Zarankiewicz," Acta Math. Acad. Sci. Hungar. 9 (1958), 269–273.
AGNT Labs, "Graffiti 292 reproducibility archive," July 23, 2026, artifact index.
L. de Moura and S. Ullrich, "The Lean 4 Theorem Prover and Programming Language," Automated Deduction – CADE 28, LNCS 12699 (2021), 625–635.
N. Wilbanks and Annie, "graffiti-292-lean: a Lean 4 proof of Graffiti conjecture 292," GitHub, 2026, agnt-gg/graffiti-292-lean, commit 5e63379.
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 292 is proved under the documented gravity normalization, with a three-line argument, four independent machine-verified batteries, exhaustive exact small-case coverage (18,686 labeled graphs through order seven), and a from-scratch reimplementation that shares no code with the primary verifiers. A stronger, uniform strict bound \(\lambda_+\le n-1

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 292:
The Least Positive Eigenvalue of Girth-Five Graphs

1. The conjecture

2. The proof

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

2.2 The trace bound

2.3 Reiman's extremal edge bound

2.4 Closing the chain

2.5 A stronger, uniform bound (added in revision, July 24, 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 cages (exact gravity means, verified margins)

4.2 The exhaustive small-order check

5. What the proof uses, and why it was not found by search

6. Novelty status — stated provisionally

7. Reproduction protocol

8. Artifact ledger

Acknowledgments

References

This is what the product is for

Stay in the loop.

Theorem	Statement
`graffiti_292`	Graffiti 292, with the mean over all \(n^2\) entries of the gravity matrix.
`graffiti_292.variants.off_diagonal_mean`	Graffiti 292, with the mean over the \(n(n-1)\) off-diagonal entries.
`graffiti_292.variants.strict`	The uniform form of §2.5: \(\lambda_+\le n-1\) and \(n\le n/\overline{\operatorname{Gr}}\), without connectivity.

Graph	n	m	girth	\(\lambda_+\)	\(n/\overline{\operatorname{Gr}}\)	margin
\(C_5\)	5	5	5	0.618034	8.333333	−7.715299
Petersen	10	15	5	1.000000	16.666667	−15.666667
Heawood	14	21	6	1.414214	38.606061	−37.191847
Hoffman–Singleton	50	175	5	2.000000	89.285714	−87.285714
cycle \(C_{17}\)	17	17	17	0.184537	212.667543	−212.483006
path \(P_{10}\)	10	9	∞	0.284630	68.229405	−67.944775
random 3-reg (n = 30, girth 5)	30	45	5	0.154525	251.275633	−251.121108

A Proof of Graffiti 292:The Least Positive Eigenvalue of Girth-Five Graphs

1. The conjecture

2. The proof

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

2.2 The trace bound

2.3 Reiman's extremal edge bound

2.4 Closing the chain

2.5 A stronger, uniform bound (added in revision, July 24, 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 cages (exact gravity means, verified margins)

4.2 The exhaustive small-order check

5. What the proof uses, and why it was not found by search

6. Novelty status — stated provisionally

7. Reproduction protocol

8. Artifact ledger

Acknowledgments

References

This is what the product is for

Stay in the loop.

A Proof of Graffiti 292:
The Least Positive Eigenvalue of Girth-Five Graphs