\documentclass[11pt]{article}
\usepackage[margin=1in]{geometry}
\usepackage{amsmath,amssymb,amsthm,microtype,hyperref}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\title{A Proof of Graffiti 292}
\author{Nathan Wilbanks and Annie (AGNT)}
\date{23 July 2026}
\begin{document}
\maketitle

\begin{abstract}
Let $G$ be a connected simple graph of order $n$ and girth at least five. Its gravity matrix is
\[
\operatorname{Gr}_{uv}=\begin{cases}
0,&u=v,\\
\dfrac{d(u)d(v)}{(n-1)d(u,v)},&u\ne v,
\end{cases}
\]
and its mean is taken over all $n^2$ entries. Graffiti 292 states that the least positive adjacency eigenvalue of $G$ is at most $n/\operatorname{mean}(\operatorname{Gr})$. We prove the conjecture by combining a degree-sum upper bound for mean gravity, the trace bound $\lambda^2\le 2m$, and the standard extremal edge bound for graphs of girth at least five. Small orders are verified exactly.
\end{abstract}

\section{Statement}
For a graph $G$, let $\lambda_+(G)$ denote its least positive adjacency eigenvalue. Graffiti 292 is
\[
\lambda_+(G)\le \frac{n}{\overline{\operatorname{Gr}}}
\]
whenever $G$ has girth at least five. The statement is read directly from page 80 of \emph{Written on the Wall}; the gravity definition is the one reproduced by Roucairol and Cazenave from Brewster--Dinneen--Faber.

\begin{lemma}\label{lem:gravity}
If $G$ has $n$ vertices and $m$ edges, then
\[
\frac{n}{\overline{\operatorname{Gr}}}\ge \frac{(n-1)n^3}{4m^2}.
\]
\end{lemma}
\begin{proof}
Since $d(u,v)\ge1$ for $u\ne v$,
\[
\begin{aligned}
\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{1}{n^2(n-1)}\left(\sum_u d(u)\right)^2
=\frac{4m^2}{n^2(n-1)}.
\end{aligned}
\]
Taking reciprocals gives the result.
\end{proof}

\begin{lemma}\label{lem:trace}
Every adjacency eigenvalue $\lambda$ satisfies $|\lambda|\le\sqrt{2m}$.
\end{lemma}
\begin{proof}
If $\lambda_1,\dots,\lambda_n$ are the adjacency eigenvalues, then
$\sum_i\lambda_i^2=\operatorname{tr}(A^2)=2m$.
\end{proof}

\begin{lemma}[standard $C_4$-free edge bound]\label{lem:reiman}
If $G$ contains no four-cycle, then
\[
m\le B(n):=\frac n4\left(1+\sqrt{4n-3}\right).
\]
\end{lemma}

\begin{theorem}
Graffiti 292 is true.
\end{theorem}
\begin{proof}
Suppose first that $n\ge7$. Put $t=\sqrt{4n-3}$, so $n=(t^2+3)/4$ and $t\ge5$. Because the left side below decreases with $m$ and the right side increases with $m$, Lemma~\ref{lem:reiman} reduces the desired comparison to
\[
\frac{(n-1)n^3}{4B(n)^2}\ge\sqrt{2B(n)}.\tag{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(t^4-4t^3-2t^2-12t+1).
\]
Writing $t=u+5$ gives
\[
P(u+5)=2u^6+56u^5+632u^4+3600u^3+10400u^2+12480u+1152>0
\]
for every $u\ge0$. Hence, by Lemmas~\ref{lem:gravity}--\ref{lem:reiman},
\[
\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 graph-atlas cases checked by exact characteristic polynomials and rational root isolation in the accompanying verifier. (The verifier checks all qualifying graphs through order seven.)
\end{proof}

\section*{Reproduction}
Run \texttt{python attack\_graffiti\_292.py}, \texttt{python verify\_symbolic\_292.py}, and \texttt{python verify\_small\_cases\_exact.py}. SHA-256 hashes are supplied in \texttt{SHA256SUMS.txt}.

\begin{thebibliography}{9}
\bibitem{fajtlowicz} S. Fajtlowicz, \emph{Written on the Wall}, July 2004, p.~80.
\bibitem{roucairol} M. Roucairol and T. Cazenave, \emph{Refutation of Spectral Graph Theory Conjectures with Search Algorithms}, arXiv:2409.18626, 2024.
\bibitem{jukna} S. Jukna, \emph{Extremal Combinatorics}, section ``Graphs with no 4-cycles.''
\end{thebibliography}
\end{document}