% Generated from the current standalone source; edit that source.
% Only title/contents wrappers and reference namespaces are changed.
\begin{abstract}
We give an exact computer-assisted proof of $R(5,6)\leq84$.
We derive a system of linear inequalities that must be satisfied by any
graph on 84 vertices containing neither a five-vertex clique nor a
six-vertex independent set. We provide explicit nonnegative rational
weights for which adding these inequalities yields a contradiction.
Published small Ramsey bounds and complete catalogues of smaller Ramsey
graphs supply the external inputs. The accompanying verification programs
check the derivation of the inequalities and their weighted sum using
exact arithmetic. Two supplements give a worked local calculation and
a detailed mathematical specification of the complete proof.
\end{abstract}

\section{Graphs, counts, and the statement}
All graphs in this paper are finite, undirected, and simple: there are no
loops or multiple edges. For a graph $X$, write $V(X)$ for its vertex set,
$E(X)$ for its edge set, and $n=|V(X)|$ for its order. For a vertex
$v\in V(X)$, its neighborhood $N_X(v)$ is the set of vertices adjacent to
$v$, and $d_v=d_X(v)=|N_X(v)|$ is its degree. For $S\subseteq V(X)$,
$X[S]$ denotes the induced subgraph: its vertices are $S$ and its edges
are all the edges of $X$ with both ends in $S$. The complement
$\overline X$ has the same vertices and exactly the pairs which are not
edges of $X$.

A clique is a vertex set whose distinct vertices are pairwise adjacent;
an independent set is a vertex set containing no edge. Define
\[
\R(s,r,n)=\{X:|V(X)|=n,\ X\text{ has no clique of size }s
\text{ and no independent set of size }r\}.
\]
We also call a member of this family an $(s,r)$-graph of order $n$.
The Ramsey number $R(s,r)$ is the least $n$ for which $\R(s,r,n)$ is
empty.

We use the following statistics of a graph:
\begin{itemize}
\item $e(X)=|E(X)|$, the number of edges;
\item $t(X)$, the number of unordered three-element vertex sets inducing
  a triangle;
\item $w(X)=\sum_{v\in V(X)}\binom{d_v}{2}$, the number of choices of a
  vertex and an unordered pair of its neighbors;
\item $q(X)=w(X)-t(X)$.
\end{itemize}
The pair of neighbors counted by $w(X)$ may itself be adjacent. Thus a
triangle contributes three to $w(X)$, while an induced three-vertex path
contributes one. Consequently
\[
q(X)=2t(X)+\#\{\text{three-element sets inducing a path in }X\}.
\]
For a triangle, $(e,t,q)=(3,1,2)$; for a three-vertex path,
$(e,t,q)=(2,0,1)$. All these counts are integers. When the graph is
specified, we abbreviate them to $e,t,w,q$.

For every vertex $v$ of the graph under discussion, put
\[
 A_v=X[N_X(v)],\qquad
 B_v=X[V(X)\setminus(N_X(v)\cup\{v\})].
\]
These are the induced subgraphs on the neighbors and on the nonneighbors
of $v$, respectively; neither contains $v$. Their orders are $d_v$ and $n-1-d_v$. 
The same definitions apply when $X$ is a smaller graph considered in an intermediate calculation.

\paragraph{Theorem.}
Subject to the small Ramsey bounds and complete catalogue inputs stated
in Section~\ref{article:sec:inputs}, $\R(5,6,84)$ is empty. Therefore
$R(5,6)\leq84$.

The small Ramsey bounds and catalogue completeness are established in
the cited sources. The verification programs check the inequalities
derived from these inputs and the final contradiction by exact arithmetic.

\subsection*{The route through the proof}
Suppose that a counterexample $X\in\R(5,6,84)$ exists. We first determine
its possible vertex degrees. We then obtain restrictions on the counts
$e,t,q$ in each $A_v$ and $B_v$. The word \emph{local} refers to these
neighborhoods or to smaller specified subsets of $V(X)$.

We write equations that every possible graph $X$ and each of its
neighborhoods would have to satisfy.
We allow additional solutions that may not come from graphs. This
larger system is called a \emph{relaxation}. An inconsistency in the
larger system rules out the existence of graphs as well.

The final system describes the proportions of the different graphs
induced by seven-element subsets of $V(X)$. Its contradiction is a
weighted sum of valid inequalities. The weights are supplied in the
electronic supplement. Understanding why an inequality is valid and
checking the arithmetic of its saved weights are separate tasks; the
reader's instructions in Section~\ref{article:sec:reader} explain both.

\section{Degrees and the first counting identity}\label{article:sec:first}
Let $X\in\R(5,6,84)$. 
For a $v\in V(X)$, a four-clique in $A_v$, together with $v$, would
be a five-clique in $X$. An independent six-set in $A_v$ would already
be one in $X$. Hence $A_v\in\R(4,6,d_v)$. Similarly, an independent
five-set in $B_v$, together with $v$, would be an independent six-set
in $X$, so $B_v\in\R(5,5,83-d_v)$.

The bounds $R(4,6)\leq40$ and $R(5,5)\leq46$ (see 
\cite[Table~Ib, p.~7]{article:survey} and \cite[Theorem~1.1]{article:r55}) now give
$d_v\leq39$ and $83-d_v\leq45$. Thus every vertex has degree 38 or 39.
The four possible local families are precisely
\[
\begin{array}{c|cc}
d_v&A_v&B_v\\ \hline
38&\R(4,6,38)&\R(5,5,45)\\
39&\R(4,6,39)&\R(5,5,44).
\end{array}
\]
If $x$ vertices have degree 39, the sum of the degrees is
$38(84-x)+39x=3192+x=2e(X)$. Therefore $x$ is even and
$e(X)=1596+x/2$.

The first relation between the two kinds of neighborhoods is
\begin{equation}\label{article:eq:tri}
 \sum_{v\in V(X)}\bigl[e(B_v)-e(A_v)-d_v(42-d_v)\bigr]=0.
\end{equation}
We give the double count, since it is also the first example of the
identities used in the proof. In an arbitrary graph of order $n$, each
triangle contributes one edge to each of three neighborhoods. Thus
$\sum_v e(A_v)=3t(X)$. For an edge $uw$, write
$c_{uw}=|N_X(u)\cap N_X(w)|$. The number of vertices adjacent to neither
$u$ nor $w$ is $n-d_u-d_w+c_{uw}$. Counting an edge inside a
nonneighborhood in this way gives
\[
\begin{aligned}
\sum_v e(B_v)
 &=\sum_{uw\in E(X)}(n-d_u-d_w+c_{uw})\\
 &=ne(X)-\sum_v d_v^2+3t(X).
\end{aligned}
\]
Here $d_v$ occurs once for each of the $d_v$ edges at $v$, and every
triangle contributes one common neighbor to each of its three edges.
Subtract $\sum_v e(A_v)$ and use $e(X)=\tfrac12\sum_vd_v$. The result is
\[
 \sum_v\bigl[e(B_v)-e(A_v)-d_v(n/2-d_v)\bigr]=0.
\]
Putting $n=84$ proves~\eqref{article:eq:tri}. This is the simplified form of
\cite[Theorem~2.2, $m=2$]{article:count}, also stated in
\cite[equation~(1.2)]{article:r55}. The last term in~\eqref{article:eq:tri} is 152 for
degree 38 and 117 for degree 39.

To use this identity we need information about the possible edge and
triangle counts inside $A_v$ and $B_v$. The next sections explain where
that information comes from, before introducing its numerical bounds.

\section{What the small graph catalogues supply}\label{article:sec:inputs}
A \emph{complete catalogue} for $\R(s,r,m)$ lists one representative of
every graph in that family up to isomorphism. 
Two graphs are isomorphic if a bijection of their vertex sets preserves adjacency. 
Counts such as $e,t,q$ are unchanged by such a bijection, so one representative suffices for checking an inequality involving these counts.
The catalogues used here are supplied on Brendan McKay's Ramsey-graph
page~\cite{article:data}. They cover the following families:
\begin{center}
\begin{tabular}{ll}
\toprule
Family&Orders or edge classes used\\\midrule
$\R(3,5,m)$&$1\leq m\leq13$\\
$\R(3,6,m)$&$13\leq m\leq17$\\
$\R(4,4,m)$&$5\leq m\leq17$\\
$\R(4,5,24)$&the complete order-24 family\\
$\R(4,5,m)$, $19\leq m\leq23$&26 specified extreme-edge classes\\
\bottomrule
\end{tabular}
\end{center}
An \emph{edge class} fixes both the order $m$ and the exact edge count.
The last line supplies complete catalogues only for those 26 classes,
not for every $(4,5)$-graph on 19 through 23 vertices. The files from
\path{r45extreme.tar.gz} identify each class by its order and edge count;
the packaged distribution contains the extracted graph6 files. The
other required edge classes are handled by proved outer bounds, described
in Section~\ref{article:sec:recursive}.

For example, \path{r36_13.g6.gz} encodes the complete 13-vertex
$(3,6)$ catalogue in compressed graph6 format. Graph6 encodes graph adjacency. The file \path{r36_13.g6.gz.profiles} records the
distinct tuples $(m,e(Y),t(Y),q(Y))$ extracted from those graphs.
Several nonisomorphic graphs may have the same tuple. Once the profile
has been computed, a linear inequality in these statistics can be
checked on one copy of each distinct profile.

The published small Ramsey bounds used with these data are
\[
R(3,5)=14,\quad R(3,6)=18,\quad R(4,4)=18,\quad R(4,5)=25,
\]
and the two bounds used in Section~\ref{article:sec:first}.
The $R(4,6)\leq40$ result is recorded in the survey~\cite{article:survey}, which
attributes the computations to Angeltveit and McKay through personal
communications from 2020 and 2024. A separate full publication of that
computation is not supplied here. The bound $R(5,5)\leq46$ is
\cite[Theorem~1.1]{article:r55}.

We also use the edge-count intervals recorded in
\cite[Appendix~A, Table~1]{article:r55}:
\[
\begin{array}{c|rrrrrr}
m&19&20&21&22&23&24\\\hline
e_{\min}&57&68&77&88&101&116\\
e_{\max}&92&100&107&114&122&132.
\end{array}
\]
These are bounds on every graph in the corresponding $\R(4,5,m)$ family.
Every integer edge count between the stated endpoints must be covered in
the proof. Absence of a catalogue file is not evidence that an edge class
is empty.

For the smaller common-neighborhood cells used later, we also need the
established minimum-edge formula for $(3,6)$-graphs on at most 12
vertices, a specialization of \cite[Theorem~2]{article:trianglefree}. If $Y$ is
such a graph of order $c$, the lower bounds are $e(Y)\geq0$ for
$0\leq c\leq5$, $e(Y)\geq c-5$ for $6\leq c\leq10$, and
$e(Y)\geq3c-25$ for $11\leq c\leq12$. The specification states the
additional elementary upper bounds and explains how these give outer
profiles when the catalogue range $13\leq c\leq17$ does not apply.

The catalogue files are inputs. Their mathematical completeness is
accepted from the cited work. Our checks count the supplied records and
check their derived profiles. The optional full verification also
recomputes the profiles of every supplied graph. Neither operation
reproves that the catalogue contains every possible graph.

\section{From possible neighborhoods to a counting system}\label{article:sec:local-model}
This section applies to an arbitrary ambient graph $X\in\R(s,r,n)$.
It will be used, separately, for the four local families in
Section~\ref{article:sec:first}. The notation $A_v,B_v,d_v$ continues to refer
to the neighborhoods and degrees in the currently specified graph $X$.

The construction has three steps. We retain a small number of statistics
of each possible neighborhood. We introduce nonnegative variables to
record how these possibilities occur around the vertices of $X$. We
then impose equations that count the same configurations in two ways.

\subsection{Profiles and containing polygons}
For fixed parameters $s',r',m$ and an integer edge count $\eta$, define
\[
\mathcal S_{s',r',m,\eta}
 =\{(t(Y),q(Y)):Y\in\R(s',r',m),\ e(Y)=\eta\}.
\]
This is a finite set of points in the plane. The order $m$ and edge count
$\eta$ are fixed, and the two coordinates record triangles and $q$.
When a complete catalogue for this edge class is available, it determines
$\mathcal S$ exactly.

For each needed edge class we use a bounded rational convex polygon
$\mathcal P_{s',r',m,\eta}$ containing $\mathcal S_{s',r',m,\eta}$.
Here a polygon may be a segment or a single point. A polygon is allowed
to be empty only when the corresponding graph class has independently
been ruled out. There are two ways to obtain it:
\begin{itemize}
\item From a complete catalogue, take the convex hull of its points:
  all their weighted averages with nonnegative weights summing to one.
\item Without a complete catalogue, prove finitely many inequalities
  $L\leq\alpha t(Y)+\beta q(Y)\leq U$ for every graph in the edge class,
  and intersect the corresponding half-planes.
\end{itemize}
A point in either polygon need not be the profile of a graph: even
averaging two catalogue profiles can produce a point with no realizing
graph.
If a linear inequality holds throughout
the polygon, it holds for every actual profile inside it. Moreover, to
check a linear inequality on a bounded convex polygon, it suffices to
check its vertices: every point is a convex combination of the vertices,
and a linear expression preserves that combination.

Write $\mathcal V_{s',r',m,\eta}$ for the finite vertex set of
$\mathcal P_{s',r',m,\eta}$. Denote its coordinates by $(\tau,\kappa)$.
These rational coordinates may lie between integer graph profiles.
Containment of all actual profiles is the property needed below.

\subsection{What the profile variables mean}
Let $D\subseteq\{0,\ldots,n-1\}$ contain every possible degree of a
graph in the ambient family. Define the two finite index sets
\[
\begin{aligned}
\mathcal I_A=\{(d,\eta,\tau,\kappa):{}&d\in D,\quad
 \eta\in\mathbb Z,\quad 0\leq\eta\leq\tbinom d2,\\
 & (\tau,\kappa)\in\mathcal V_{s-1,r,d,\eta}\},\\
\mathcal I_B=\{(h,\eta,\tau,\kappa):{}&h=n-1-d\text{ for some }d\in D,\\
 &\eta\in\mathbb Z,\quad 0\leq\eta\leq\tbinom h2,\quad
 (\tau,\kappa)\in\mathcal V_{s,r-1,h,\eta}\}.
\end{aligned}
\]
The four entries specify the order of a local graph, its exact edge
count, and one vertex of its profile polygon. Introduce a nonnegative
real variable $a_i$ for every $i\in\mathcal I_A$ and $b_j$ for every
$j\in\mathcal I_B$. These are variables of our counting system.
Here is how an actual graph assigns values to them.

For each $v\in V(X)$, the pair $(t(A_v),q(A_v))$ lies in the polygon
with order $d_v$ and edge count $e(A_v)$. Express that pair as a convex
combination of the polygon's vertices. Let $\lambda^A_{v,i}$ be the
coefficient assigned to index $i$, with coefficient zero for all indices
having any other order or edge count. Then
\[
\sum_{i\in\mathcal I_A}\lambda^A_{v,i}=1,\qquad
\sum_{i=(d,\eta,\tau,\kappa)\in\mathcal I_A}
 \lambda^A_{v,i}(\tau,\kappa)=(t(A_v),q(A_v)).
\]
Choose coefficients $\lambda^B_{v,j}$ in the same way for $B_v$, and set
\[
 a_i=\sum_{v\in V(X)}\lambda^A_{v,i},\qquad
 b_j=\sum_{v\in V(X)}\lambda^B_{v,j}.
\]
Thus $a_i$ is an aggregate weight assigned to one allowed neighborhood
profile vertex; $b_j$ has the corresponding meaning for nonneighborhoods.
They need not be integers, even when they arise from an actual graph.

For a concrete example, the catalogue profiles with order 13 and 16
edges in \path{r36_13.g6.gz.profiles} have exactly the pairs
$(0,25),(0,26),(0,28)$. The polygon is the segment with endpoints
$(0,25)$ and $(0,28)$, and
\[
 (0,26)=\tfrac23(0,25)+\tfrac13(0,28).
\]
A single vertex whose neighborhood has profile $(13,16,0,26)$ therefore
contributes $2/3$ to $a_{13,16,0,25}$ and $1/3$ to $a_{13,16,0,28}$.
Its total weight is one, and its weighted $q$ coordinate is 26. This
shows how fractional profile weights represent one vertex while
preserving the statistics of its neighborhood.

\subsection{Recovering counts and imposing equations}
Let $m_d$ be the sum of all $a$ variables with first coordinate $d$.
For an assignment obtained from a graph, $m_d$ is the number of vertices
of degree $d$. The sum of the $b$ variables with first coordinate
$n-1-d$ has the same value. The system therefore includes these matching
equations and $\sum_{d\in D}m_d=n$.

Define four linear expressions in the $a$ variables:
\[
\begin{aligned}
\mathcal E(a)&=\frac12\sum_{\mathcal I_A}d\,a_{d,\eta,\tau,\kappa},
&\mathcal T(a)&=\frac13\sum_{\mathcal I_A}\eta\,a_{d,\eta,\tau,\kappa},\\
\mathcal W(a)&=\sum_{\mathcal I_A}\binom d2a_{d,\eta,\tau,\kappa},
&\mathcal Q(a)&=\mathcal W(a)-\mathcal T(a).
\end{aligned}
\]
Each sum runs over the entire index set $\mathcal I_A$. On the assignment
constructed from $X$, these expressions equal $e(X),t(X),w(X),q(X)$.
The first assertion is handshaking; the second uses
$\sum_v e(A_v)=3t(X)$; the third counts pairs of neighbors at their
center. More generally, any expression affine in the local coordinates
$(\tau,\kappa)$ is preserved by the convex combinations at each vertex.
The order and edge count remain fixed within each combination.

We next introduce $z_F\geq0$, one variable for each of the eleven
isomorphism types $F$ of graphs on four vertices. Its value for an actual
$X$ is the number of four-element subsets inducing type $F$. Examples
are $z_{K_4}$ for four-cliques and $z_{4K_1}$ for independent four-sets.
Counting four-sets and the edges, triangles and adjacent-edge pairs
inside them gives
\[
\begin{aligned}
 \sum_F z_F&=\binom n4,&
 \sum_F e(F)z_F&=\binom{n-2}{2}\mathcal E(a),\\
 \sum_F t(F)z_F&=(n-3)\mathcal T(a),&
 \sum_F w(F)z_F&=(n-3)\mathcal W(a).
\end{aligned}
\]
For example, an edge of $X$ is contained in exactly $\binom{n-2}{2}$
four-sets. Counting incidences between an edge and a containing four-set
proves the second equation.

We also match triples counted inside neighborhoods with the same triples
counted inside four-sets. To make this explicit, define
\[
\begin{aligned}
 T_0(m,\eta,\tau,\kappa)&=\binom m3-(m-2)\eta+\kappa,\\
 T_1(m,\eta,\tau,\kappa)&=(m-2)\eta-2\kappa+\tau,\\
 T_2(m,\eta,\tau,\kappa)&=\kappa-2\tau,\qquad
 T_3(m,\eta,\tau,\kappa)=\tau.
\end{aligned}
\]
For a graph profile these are the counts of induced triples with
$0,1,2,3$ edges. They follow by counting all triples, edge incidences
in triples, and adjacent-edge pairs in triples. Let $U_k(F)$ count
vertices of $F$ adjacent to all other three vertices whose deletion
leaves exactly $k$ edges. Let $Z_k(F)$ count isolated vertices of $F$
whose deletion leaves $k$ edges. Then, for $k=0,1,2,3$,
\[
\begin{aligned}
\sum_{\mathcal I_A}T_k(d,\eta,\tau,\kappa)a_{d,\eta,\tau,\kappa}
 &=\sum_F U_k(F)z_F,\\
\sum_{\mathcal I_B}T_k(h,\eta,\tau,\kappa)b_{h,\eta,\tau,\kappa}
 &=\sum_F Z_k(F)z_F.
\end{aligned}
\]
For instance, a triple in $A_v$ together with $v$ is a four-set in which
$v$ is adjacent to the whole triple. Both sides count precisely those
choices. These equations require the neighborhood and nonneighborhood
statistics to fit into the \emph{same} collection of four-sets.

The simplified triple identity is another equation of the system:
\[
\sum_{\mathcal I_B}\eta b_{h,\eta,\tau,\kappa}
-\sum_{\mathcal I_A}\bigl(\eta+d(n/2-d)\bigr)
 a_{d,\eta,\tau,\kappa}=0.
\]
We also record edges by their endpoint degrees. For $d,f\in D$ with $d\leq f$, let $j_{d,f}\geq0$ count such
edges. Each edge within degree class $d$ contributes two ends to that
class; each edge to another class contributes one. Thus
\[
 d m_d=2j_{d,d}+\sum_{f<d}j_{f,d}+\sum_{f>d}j_{d,f}.
\]
The sums here are over $f\in D$. If $p(F)$ denotes the number of
unoriented paths of three edges on four distinct vertices of $F$, with
additional edges allowed, the path equation is
\[
 \sum_F p(F)z_F
 =\sum_{d\leq f}(d-1)(f-1)j_{d,f}-3\mathcal T(a).
\]
To see the correction term, choose the middle edge of a path and then
its two outer endpoints. Coincident outer endpoints correspond to
triangles; there are $3t(X)$ of these choices.

To restrict the model to a fixed edge count $e(X)=e_0$, we impose the
linear equation $\mathcal E(a)=e_0$. Only in this fixed-edge model do
we also include the equation counting pairs of disjoint edges:
\[
 \mathcal W(a)+\sum_F\left(\binom{e(F)}2-w(F)\right)z_F
 =\binom{e_0}{2}.
\]
The first term counts pairs sharing a vertex. Each remaining pair has
four distinct endpoints and is counted by exactly one four-set. Fixing
$e_0$ makes the right side a constant, so this is a linear equation.

These equations are necessary conditions on every graph in the chosen
family. We allow the variables to be arbitrary nonnegative real numbers
satisfying them. We do not claim that every solution comes from a graph.
Bounds valid for every solution therefore apply to every graph in the
family.
The accompanying specification gives the full row list, its order in the
files, and the distinction between versions 3 and 4.

\section{How a certificate proves a bound}\label{article:sec:certificate}
A certificate in this paper is a finite list of rational multipliers
for already justified equations or inequalities. Checking a certificate
means checking what their weighted sum says. The optimization algorithm
which found the multipliers is not part of that check.

Consider this elementary example, unrelated to the Ramsey data. Suppose
$u_1,u_2,u_3\geq0$ and
\[
 u_1+u_2=5,\qquad u_2+u_3=4.
\]
Twice the first equation plus the second gives
$2u_1+3u_2+u_3=14$. Therefore
\[
 3u_1+3u_2+u_3=14+u_1\geq14.
\]
The multipliers $(2,1)$ and the nonnegative remainder $u_1$ are a
complete proof of this lower bound for every feasible triple
$(u_1,u_2,u_3)$.

The actual certificates do the same thing with many more variables.
First remove any variable already known to be zero. For example,
$z_{K_4}=0$ in a $(4,6)$-graph because it contains no four-clique.
Similarly $z_{4K_1}=0$ when the forbidden independent-set size is four.
Removing these coordinates means substituting their known value zero
in every equation.

Let $\mathbf u=(u_1,\ldots,u_N)^{\mathsf T}$ be the remaining profile,
four-set, and endpoint-degree variables, in the order used by the
certificate. Let there be $m$ counting equations. Put their coefficients
in the $m$ by $N$ rational matrix $M$, and their right-hand sides in
$\mathbf b\in\mathbb Q^m$. Thus the $k$th equation is
$\sum_{j=1}^N M_{kj}u_j=b_k$, and the whole system is
\[
 M\mathbf u=\mathbf b,\qquad \mathbf u\geq0.
\]
A coefficient vector $\mathbf c\in\mathbb Q^N$ specifies the quantity
we wish to bound: $\mathbf c^{\mathsf T}\mathbf u=\sum_jc_ju_j$.
For example, $\mathbf c$ can be the coefficients of $\mathcal E(a)$
for a lower edge bound, or of $-\mathcal E(a)$ for an upper edge bound.

Choose a rational multiplier $y_k$ for the $k$th equation, and collect
these into $\mathbf y\in\mathbb Q^m$. Their weighted sum has coefficient
$\sum_k y_kM_{kj}$ on $u_j$. Subtract this sum from the objective and
use the equations:
\begin{equation}\label{article:eq:certificate}
 \mathbf c^{\mathsf T}\mathbf u
 =\mathbf y^{\mathsf T}\mathbf b+
   \sum_{j=1}^N\left(c_j-\sum_{k=1}^m y_kM_{kj}\right)u_j.
\end{equation}
If every coefficient in parentheses is nonnegative, every term in the
last sum is nonnegative. The objective is then at least
$\mathbf y^{\mathsf T}\mathbf b$. In matrix notation the coefficient
test is $M^{\mathsf T}\mathbf y\leq\mathbf c$, coordinate by coordinate.
The multipliers $y_k$ may have either sign because they multiply
\emph{equalities}. Only the remainders multiplying the nonnegative
variables must have the stated sign.

The saved vectors $\mathbf y$ are called \emph{dual certificates}.
For each one, the verifier reconstructs $M,\mathbf b,\mathbf c$ from
the mathematical model, checks all the remainder coefficients, and
computes $\mathbf y^{\mathsf T}\mathbf b$ exactly. The files store the family
and optional fixed-edge parameters in \texttt{model}, the objective
vector in \texttt{objective}, the multiplier vector in \texttt{dual},
and the resulting rational bound in \texttt{exact\_lower\_bound}.
The matrix and right-hand side are reconstructed from the model
parameters and the counting definitions. In the file format, the fields
\texttt{s}, \texttt{t}, and \texttt{n} encode the parameters $s,r,n$
of $\R(s,r,n)$, respectively.

The stored triple-identity row is twice the equation displayed
above, so that its coefficients are integral. Multiplying an equation
by two and dividing its multiplier by two leaves the weighted sum
unchanged. This correspondence allows the displayed equation and the
stored certificate row to be checked against each other.

\section{Obtaining all required local profile bounds}\label{article:sec:recursive}
We can now explain the passage from the small catalogues to the
38--45-vertex local graphs. For example, let $X\in\R(4,6,38)$.
Its neighborhoods are in $\R(3,6,d_v)$ and its nonneighborhoods in
$\R(4,5,37-d_v)$. The bounds $R(3,6)=18$ and $R(4,5)=25$ give
$13\leq d_v\leq17$. The neighborhood profiles are therefore supplied
by complete catalogues on 13 through 17 vertices. The nonneighborhoods
have orders 20 through 24. At order 24 the catalogue is complete;
at orders 20 through 23, complete extreme-edge catalogues are combined
with the outer polygons described next.

For the other three local families the degree restrictions are obtained
in the same way. The complete list of orders needed on the two sides is
\[
\begin{array}{c|cc}
\text{ambient family}&\text{order of }A_v&\text{order of }B_v\\\hline
\R(4,6,38)&13\text{--}17&20\text{--}24\\
\R(4,6,39)&14\text{--}17&21\text{--}24\\
\R(5,5,44)&19\text{--}24&19\text{--}24\\
\R(5,5,45)&20\text{--}24&20\text{--}24.
\end{array}
\]
In the last two lines, $A_v$ is a $(4,5)$-graph and $B_v$ is a
$(5,4)$-graph. Complementing $B_v$ makes it a $(4,5)$-graph, so the
same catalogue and polygon inputs suffice. For any graph $Y$ of order
$m$, the exact profile transformation is
\[
\begin{aligned}
e(\overline Y)&=\binom m2-e(Y),\\
t(\overline Y)&=\binom m3-(m-2)e(Y)+q(Y),\\
q(\overline Y)&=2\binom m3-(m-2)e(Y)+t(Y).
\end{aligned}
\]
These formulas follow by interchanging edges and nonedges in the four
possible induced triple types. They are affine, so they also transform
containing polygons and convex combinations correctly.

For each order $19\leq m\leq23$ and every edge count in the interval
of Section~\ref{article:sec:inputs}, we need a polygon containing all profiles
of $\R(4,5,m)$ at that edge count. There are 149 such edge classes.
For 26 of them the complete extreme-edge catalogues give the exact
convex hull. For each of the other 123 classes, a smaller counting
system is built using neighborhoods in $(3,5)$-graphs and
nonneighborhoods in $(4,4)$-graphs. Both kinds have complete catalogue
inputs of smaller order. Certificates of the form~\eqref{article:eq:certificate}
then give upper and lower bounds on each of
\[
 t,\ q,\ t+q,\ t-q,\ t+2q,\ 2t+q,\ t-2q,\ 2t-q.
\]
Their values on a graph are integers, so the exact rational bounds can
be rounded in the justified direction. Intersecting these half-planes
gives the required polygon. The $123\cdot8\cdot2=1968$ bound
certificates are included. Each uses the smaller catalogue inputs just
listed, so its premises are available before the resulting polygon is
used in a larger counting system.

The polygons are recorded in \path{computed_v3_45_19.json} through
\path{computed_v3_45_23.json}. A polygon audit checks that the stored
vertices describe the stated intersection. A separate certificate audit
proves that every bounding half-plane contains the required graph
profiles. Together these checks establish that the stored polygon
contains every profile in its edge class.

\subsection{The four edge bounds}\label{article:sec:local-edge}
Applying these counting systems gives the four statements
\begin{equation}\label{article:eq:four-local-bounds}
\begin{aligned}
Y\in\R(4,6,38)&\ \Longrightarrow\ e(Y)\leq314,\\
Y\in\R(4,6,39)&\ \Longrightarrow\ e(Y)\leq324,\\
Y\in\R(5,5,44)&\ \Longrightarrow\ e(Y)\geq432,\\
Y\in\R(5,5,45)&\ \Longrightarrow\ e(Y)\geq460.
\end{aligned}
\end{equation}
Each statement follows from the counting system of
Section~\ref{article:sec:local-model} using the smaller catalogue and polygon
inputs above. The certificates are as follows.
\begin{enumerate}
\item \path{edge_46_38_max.json} gives $-e(Y)\geq-26125/83$.
Since $26125/83<315$ and $e(Y)$ is an integer, $e(Y)\leq314$.
\item \path{edge_46_39_max.json} first gives $e(Y)\leq325$.
For the remaining case $e(Y)=325$, the files
\path{exclude_4639e325_t_gt537.json} and
\path{exclude_4639e325_t_lt538.json} give
$t(Y)\geq1612/3$ and $t(Y)\leq1612/3$. A triangle count cannot
be $1612/3$, so this edge count is excluded and $e(Y)\leq324$.
\item \path{edge_55_44_min.json} gives $e(Y)\geq95414/221>431$,
hence $e(Y)\geq432$.
\item \path{edge_55_45_min.json} gives
$e(Y)\geq12137627230191/26402663302>459$, hence $e(Y)\geq460$.
\end{enumerate}
For a nonempty family, the standard notation $e(s,r,n)$ and $E(s,r,n)$
denotes its minimum and maximum edge count. The universal statements
above also make sense if a family is empty.

Return now to the hypothetical $X\in\R(5,6,84)$. The following table
summarizes the bounds just proved, using the local family corresponding
to each possible degree:
\[
\begin{array}{c|cc}
d_v&\text{upper bound on }e(A_v)&\text{lower bound on }e(B_v)\\\hline
38&314&460\\
39&324&432.
\end{array}
\]
Because these are the only two degrees, the table can also be written
\begin{equation}\label{article:eq:local-affine-bounds}
 e(A_v)\leq10d_v-66,\qquad e(B_v)\geq1524-28d_v.
\end{equation}
These affine formulas simply interpolate the two entries in each column.
They alone do not contradict~\eqref{article:eq:tri}. The lower bounds for its
summands are $460-314-152=-6$ and $432-324-117=-9$.
To obtain more information we must retain $t$ and $q$, not just edges.

\subsection{Five inequalities retaining triangles and adjacent edges}
For every vertex of $X\in\R(5,6,84)$ we prove the following additional
inequalities, labelled A and B$_1$ through B$_4$:
\begin{align*}
\mathrm{A}:\quad&770d_v-269e(A_v)-6t(A_v)+12q(A_v)+5940\leq0,\\
\mathrm{B}_1:\quad&-732d_v-76e(B_v)-t(B_v)+2q(B_v)+49239\leq0,\\
\mathrm{B}_2:\quad&-701d_v-75e(B_v)-t(B_v)+2q(B_v)+47596\leq0,\\
\mathrm{B}_3:\quad&-483d_v-35e(B_v)-2t(B_v)+q(B_v)+29877\leq0,\\
\mathrm{B}_4:\quad&-403d_v-37e(B_v)-t(B_v)+q(B_v)+26296\leq0.
\end{align*}
In every line $d_v$ is the degree of the original vertex in the
84-vertex graph; the order of $B_v$ is $83-d_v$.

The correspondence with the electronic files is
\[
\begin{array}{c|ccccc}
\text{statement}&\mathrm A&\mathrm B_1&\mathrm B_2&\mathrm B_3&\mathrm B_4\\\hline
\text{file identifier}&203&595&603&658&681.
\end{array}
\]
These integers locate the five inequalities in
\path{local_profile_facets.json}. The file
\path{exact_candidate_used_facets.json} lists their coefficients and
keys. The final certificate uses these five entries from the stored
collection of local inequalities.

To prove a line, fix the local family and its integer edge count, build
the counting system of Section~\ref{article:sec:local-model}, and use a dual
certificate as in Section~\ref{article:sec:certificate}. The complete ranges
which must be covered are
\[
\begin{array}{c|rrrr}
\text{local family}&\R(4,6,38)&\R(4,6,39)&\R(5,5,44)&\R(5,5,45)\\\hline
e_{\min}&267&288&432&460\\
e_{\max}&314&324&514&530.
\end{array}
\]
The endpoints are themselves certified. The file
\path{edge_certification_summary.json} indexes the eight endpoint
bounds and the two triangle-count exclusions used above; the full
specification gives their exact values and filenames.

There are $48+37=85$ edge cases for statement A and $83+71=154$
for each statement B. Thus $85+4\cdot154=701$ certificates prove the
five lines. For example, statement A at $d_v=38$ and $e(A_v)=314$
requires
\[
 -6t(A_v)+12q(A_v)\leq49266.
\]
The file \path{facet203_46_n38_e314.json} proves
$6t-12q\geq-541956/11$, hence $-6t+12q<49272$.
The expression $-6t+12q$ is a multiple of six, so it is at most 49266.
The counting equations hold for every graph in the fixed edge class,
so the resulting inequality holds throughout that class.

For a general line with coefficients
$\gamma_d,\gamma_e,\gamma_t,\gamma_q,\gamma_0$, the same argument
bounds $\gamma_t t+\gamma_q q$ at each fixed edge count. The $\gamma$'s denote the fixed coefficients in the chosen line.
The entire required local chain consists of the 1968 prerequisite
polygon bounds, 10 endpoint/exclusion certificates, and 701 final
edge cases: 2679 certificates. The checker
\path{replay_required_local_certificates.py} verifies both their
arithmetic and their coverage. It also checks that their objectives
and integer rounding thresholds match the claimed inequalities.

\section{A distribution on seven-vertex graphs}\label{article:sec:seven}
From now on $X$ again denotes the hypothetical 84-vertex counterexample.
Let $\mathcal H$ contain one representative of each isomorphism type
of seven-vertex graph having no five-clique and no independent six-set.
There are 979 such types. For each $H\in\mathcal H$, define
\[
 p_H=\frac{\#\{W\subseteq V(X):|W|=7,\ X[W]\cong H\}}{\binom{84}{7}}.
\]
This is the probability of seeing type $H$ when a seven-element vertex
set is chosen uniformly. Therefore $p_H\geq0$ and
$\sum_{H\in\mathcal H}p_H=1$. Every seven-set in $X$ is represented
because forbidden configurations in a subset would also be forbidden
configurations in $X$.

The supplied code checks this set of types exhaustively. A labelled
seven-vertex graph is determined by its 21 possible edges. The checker
tests all $2^{21}$ adjacency choices and compares the allowed labelled
counts with the orbit sizes of the 979 representatives, separately by
edge count. Here an orbit consists of the distinct labelled graphs
obtained by permuting a representative's seven vertices.

Our aim is now to express valid facts about $X$ as linear equations
and inequalities in the numbers $p_H$. A \emph{coefficient row} is a
function $U:\mathcal H\to\mathbb Q$: its entry $U(H)$ is the coefficient
of $p_H$. Saying that this row is valid means
$\sum_Hp_HU(H)\leq0$ for every possible $X$. This interpretation
will be used for every row in the final certificate.

\subsection{How a local fact becomes a coefficient row}\label{article:sec:sampling}
A \emph{rooted graph} has specified distinguished vertices, called
roots. A \emph{flag} is a small induced graph together with the roles
of its roots. For example, one root may represent the vertex whose
degree is being measured, or two roots may specify an edge. Isomorphisms
must preserve these roles. A \emph{placement} is a choice of actual
vertices inducing the specified flag. Root labels and any explicitly
unordered groups are counted consistently; the specification states
the conventions of each row family.

Here is the simplest sampling calculation. Fix a placement of a
six-vertex flag with root $v$, and let $r_0$ be the number of neighbors
of $v$ among the other five vertices. There are 78 vertices outside
the flag. Choose one of them uniformly and let $\chi$ be 1 if it is
adjacent to $v$, and 0 otherwise. Then
\[
 \mathbb E(\chi)=\frac{d_v-r_0}{78},\qquad
 \mathbb E(r_0+78\chi)=d_v.
\]
The expectation here is over that one uniformly sampled exterior
vertex, with the flag placement fixed. Thus $r_0+78\chi-39$ is an
estimate of $d_v-39$ with exactly the right average. Its value can be
computed using only the resulting seven-vertex graph. Since $d_v\leq39$,
summing this estimate over all placements of the flag and averaging
over seven-sets gives a valid nonpositive coefficient row.

The general rule is equally finite. A fixed $f$-vertex flag leaves
$84-f$ exterior vertices; a seven-set containing it selects $7-f$
of them. A specified configuration using $m$ distinct exterior vertices
is included with probability
\[
 \frac{\binom{7-f}{m}}{\binom{84-f}{m}},\qquad 0\leq m\leq7-f.
\]
Multiply its observed count by the reciprocal to obtain an estimate
whose average equals the full count. Products of counts require care:
when two factors use the same exterior vertex, that contribution has
$m=1$, not $m=2$. All these coincidences are included.

For precision, let $I(X,\phi)\leq0$ be the original inequality for a
placement $\phi$ of a specified $f$-vertex flag. Let
$\widehat I(H,\phi)$ be its estimate on a seven-vertex graph, and put
$U(H)=\sum_\phi\widehat I(H,\phi)$, summing over placements in $H$.
Interchanging the sums over seven-sets and placements gives
\[
 \sum_Hp_HU(H)
 =\frac{\binom{84-f}{7-f}}{\binom{84}{7}}
    \sum_{\phi\text{ in }X} I(X,\phi)\leq0.
\]
The factor is positive and is the same for every placement. This
establishes the row's validity after averaging over all placements.
Equalities are treated in the same way. This passage
is called \emph{lifting} the local relation; it has no asymptotic error.

\subsection{The local relations used in these rows}
The inputs include the degree bounds, the degree identity
$(d_v-38)(d_v-39)=0$, the local edge bounds~\eqref{article:eq:local-affine-bounds},
and the five local inequalities. Further rows describe small common
neighborhoods. To define them, take disjoint vertex sets $C,D$, with
$C$ a clique and $D$ independent, and put
\[
\mathcal C(C,D)=\{x\in V(X)\setminus(C\cup D):
 x\sim c\text{ for all }c\in C,\quad
 x\not\sim d\text{ for all }d\in D\}.
\]
Here $x\sim y$ means that $x,y$ are adjacent. This \emph{cell} is a
vertex set; counts of edges and triangles in it refer to the induced
graph $X[\mathcal C(C,D)]$. Its size is an integer. A clique in the
cell extends by $C$, and an independent set in it extends by $D$.
This gives a smaller Ramsey family and therefore bounds on the cell.

For example, the common neighborhood of the endpoints of an edge is
a $(3,6)$-graph, so it has at most 17 vertices. It has at least 13:
the neighbors of one endpoint, apart from the other endpoint and their
common neighbors, form a $(4,5)$-graph and have at most 24 vertices.
Since the endpoint has degree at least 38, the common neighborhood
has size at least $38-1-24=13$. The complete $(3,6)$ catalogues on
orders 13 through 17 therefore cover this cell exactly.

The rows use upper capacities, edge/profile inequalities for these
cells, and elementary integer inequalities. For instance, if $c$ is
an integer cell size and $k$ is an integer, then
$(c-k)(c-k-1)\geq0$: no integer lies strictly between $k$ and $k+1$.
The quantities $d_v-38$ and $39-d_v$ are either zero or one, so their
products also give nonnegative expressions. Each is expanded into
counts to which the sampling rule applies.

One further input uses the seven graphs in the complete
$\R(3,6,17)$ catalogue. Their degrees are all 4 or 5. For a triangle
with vertices $u,v,w$, let
\[
 c=|N_X(u)\cap N_X(v)|,\qquad
 \tau=|N_X(u)\cap N_X(v)\cap N_X(w)|.
\]
The vertex $w$ belongs to that common-neighborhood graph. If $c=17$,
its degree there is $\tau\in\{4,5\}$. If $c=16$, its nonneighbors
there form a $(3,5)$-graph of order at most 13, giving $\tau\geq2$.
For $c\leq15$, $\tau\geq0$ suffices. Consequently
\[
 \tau\geq2c-30,\qquad (16-c)(\tau-4)(\tau-5)\geq0.
\]
For the second inequality, at $c=17$ the last two factors have product
zero; for $c\leq16$ they are consecutive integer factors with
nonnegative product. These facts produce additional valid rows by the
same exact sampling procedure. The specification lists all row families
and their formulas; the source audits check that the stored arrays
implement those formulas.

\section{Why sums of squares give further inequalities}\label{article:sec:gram}
We need one additional kind of valid row. Its underlying fact is simply
that a sum of squares is nonnegative. We describe how to express that
fact using seven-vertex graphs, including overlaps exactly.

Fix a labelled root graph $\sigma$ with $\ell$ vertices, and an
extension size $k\geq0$ such that $\ell+2k\leq7$. A root placement
$\rho$ is an injection of those $\ell$ labelled vertices into $V(X)$
which induces $\sigma$. Write $R_\rho$ for its image. Let
$\mathcal F_{\sigma,k}$ be the finite collection of possible rooted
isomorphism types on $\ell+k$ vertices, excluding a five-clique and
an independent six-set. The roots are fixed by isomorphisms; the
$k$ other vertices may be permuted.

For each type $i\in\mathcal F_{\sigma,k}$ define
\[
 f_i(\rho)=\#\{S\subseteq V(X)\setminus R_\rho:
 |S|=k,\ (X[R_\rho\cup S],\rho)\text{ has type }i\}.
\]
This is an integer count of extensions of a fixed root placement.
Collect these counts into a column vector $f(\rho)$. For any real
coefficient vector $z=(z_i)_{i\in\mathcal F_{\sigma,k}}$,
\[
 \sum_\rho\left(\sum_i z_if_i(\rho)\right)^2\geq0.
\]
Equivalently, the matrix $\sum_\rho f(\rho)f(\rho)^{\mathsf T}$ is
\emph{positive semidefinite}: a symmetric matrix $M$ has that property
when $z^{\mathsf T}Mz\geq0$ for every real vector $z$. This explains
both the matrix terminology and the inequality it encodes.

To expand an entry of this matrix, choose a root placement and an
ordered pair $(S,T)$ of $k$-element extension sets. The sets may
intersect, and $S=T$ is allowed. Their union with the roots has
$\ell+|S\cup T|\leq7$ vertices, and is contained in exactly
\[
 D(S,T)=\binom{84-\ell-|S\cup T|}{7-\ell-|S\cup T|}
\]
seven-sets of $X$. This positive integer tells us how often the same
pair would otherwise be counted.

For a seven-vertex graph $H$, form a matrix $M_H$ with rows and columns
indexed by $\mathcal F_{\sigma,k}$. Enumerate root placements in $H$
and all ordered extension pairs $(S,T)$ outside the roots. If $S$ has
type $i$ and $T$ has type $j$, add $1/D(S,T)$ to entry $(i,j)$.
The denominator uses the target order 84, even though this small
calculation takes place in $H$. Summing over all seven-sets of $X$
counts each extension pair with total weight exactly one. Hence
\[
 \sum_{\substack{W\subseteq V(X)\\|W|=7}} M_{X[W]}
 =\sum_\rho f(\rho)f(\rho)^{\mathsf T}.
\]
Dividing by $\binom{84}{7}$ shows that $\sum_Hp_HM_H$ is positive
semidefinite. In particular, for any chosen $z$,
\[
 \sum_Hp_H\bigl(-z^{\mathsf T}M_Hz\bigr)\leq0.
\]
This has exactly the coefficient-row form needed in
Section~\ref{article:sec:seven}.

We use the pairs $(\ell,k)=(0,3),(1,3),(2,2),(3,2)$.
There are respectively one, one, two and four root graph types,
so eight matrices of this kind. For each root type choose one positive
integer $L$ clearing every denominator in its matrices, and set
$I_H=LM_H$. The data supply 448 integer vectors $z$ distributed among
these eight types. Each supplies the valid row
$H\mapsto-z^{\mathsf T}I_Hz$. The enumeration includes all intersections of the extension sets,
as required by the displayed matrix identity.

\section{The final rational sum and its contradiction}\label{article:sec:final}
All the rows now have a defined mathematical meaning. There are 4876
rows from local counting relations and 448 from the square construction.
Index their normalized coefficient functions by
$U_i:\mathcal H\to\mathbb Q$, $0\leq i<5324$. There are also 89
homogeneous equality rows $E_j:\mathcal H\to\mathbb Q$,
$0\leq j<89$. Thus a hypothetical counterexample would give
\[
 \sum_Hp_HU_i(H)\leq0,\qquad \sum_Hp_HE_j(H)=0.
\]
A homogeneous equality has right-hand side zero. The equation
$\sum_Hp_H=1$ is kept separate; it is not one of the $E_j$ rows.

For an integer coefficient row $(a_H)_H$, normalization divides it by
$\max\{1,\max_H|a_H|\}$. This is a positive number, so validity and
sign are unchanged. The saved multipliers refer to these normalized
rows, and the verifier uses that same normalization.

The file \path{exact_separation_certificate.json} supplies rational
weights $\lambda_i\geq0$ for the inequalities and rational weights
$\mu_j$ of either sign for the equalities. They have common denominator
$10^{12}$. For every $H\in\mathcal H$, form the number
\[
 C(H)=\sum_i\lambda_i U_i(H)+\sum_j\mu_j E_j(H).
\]
This is just a weighted sum of coefficients in one column of the
stored arrays. The exact arithmetic check proves
\[
 C(H)\geq\delta\quad\text{for every }H\in\mathcal H,
 \qquad \delta=\frac{3146981978575629437}{10^{24}}>0.
\]
The check obtains a conservative lower bound by rounding each scaled
summand down using integer division, including negative summands.
It therefore proves the displayed inequality without a floating-point
tolerance. The actual coefficients $C(H)$ may exceed this common lower
bound.

Only 903 multipliers are nonzero: 816 for inequalities, of which 194
are square rows, and 87 for homogeneous equalities. These weights give
two incompatible conclusions. First, because the inequality weights
are nonnegative and all the rows are valid,
\[
 \sum_Hp_HC(H)
 =\sum_i\lambda_i\sum_Hp_HU_i(H)
   +\sum_j\mu_j\sum_Hp_HE_j(H)\leq0.
\]
Second, because the $p_H$ are nonnegative and sum to one,
\[
 \sum_Hp_HC(H)\geq\delta\sum_Hp_H=\delta>0.
\]
This contradiction excludes $X$ and proves the theorem.

The complete square calculations have been recomputed with
arbitrary-precision integers. A second implementation uses integer
contractions with a separately checked overflow bound. Both reproduce
the separating calculation.

\section{What an independent reader should check}\label{article:sec:reader}
There are two complementary parts to checking this proof. The
mathematical part establishes why an arbitrary counterexample would
satisfy the equations and inequalities. The computational part checks
that the supplied rational numbers actually combine those relations
as claimed. Neither part replaces the other.

\subsection{Reading the mathematics}
The chain to be checked is as follows.
\begin{enumerate}
\item Confirm the cited external bounds and the precise scope of each
catalogue in Section~\ref{article:sec:inputs}.
\item Check the graph-to-variable construction in
Section~\ref{article:sec:local-model}. Every actual neighborhood profile must
lie in its designated polygon; its convex representation must preserve
the local counts. Verify the displayed double counts.
\item Check the weighted-equation principle~\eqref{article:eq:certificate} and
the exact integer-rounding steps. The worked explanation develops the
314-edge bound in detail, reducing its certificate to ten local
inequalities and one identity that can be followed on paper.
\item Check that each local fact used globally becomes a valid row by
the finite sampling rule, and that the square rows include every
possible overlap. The detailed specification gives all row formulas
and their index conventions for comparison with the programs.
\item Check the two final averaging inequalities in
Section~\ref{article:sec:final}. Once their premises have been established,
this last step is an ordinary finite contradiction.
\end{enumerate}
The two companion documents are titled \emph{Reading the exact
certificate: the method and a worked local example} and
\emph{Detailed mathematical specification}. The first is for following
a concrete calculation; the second is for checking all definitions
and reconstructing the computations. The certificate files supply
the numerical coefficients used in those computations.

\subsection{Replaying the supplied calculations}
The complete electronic distribution is \path{verification.tar.xz}.
Extracting it creates a directory named \path{verification}. In that
directory, \path{README.txt} gives installation instructions and
\path{FILE_INDEX.tsv} locates each basename cited in this paper.
Keep the extracted directory structure intact so that the programs can
locate their inputs.

For the worked local example, run the following command with the
terminal's current directory set to the extracted \path{verification}
directory:
\begin{verbatim}
python3 check_local_example.py --root .
\end{verbatim}
This requires only the Python standard library. A successful run reports
\begin{verbatim}
"worked_example_passed": true
"edge_upper_bound": 314
\end{verbatim}
It checks the explicit
local inequalities on the supplied profiles and polygon vertices and
checks their relation to the saved certificate. It does not by itself
prove the prerequisite polygon bounds or catalogue completeness.

For the main certificate and its computational dependencies, install
the packages specified in \path{requirements.txt}, following the
README, and run from that same directory:
\begin{verbatim}
python3 verify_package.py
\end{verbatim}
The launcher first checks file integrity, then runs the
18 core checks, the source-to-matrix audit, and the worked-example check.
Every stage must exit successfully and the final report must contain
\texttt{"all\_passed": true}. A success message from only one
intermediate stage is insufficient.

For the additional exhaustive profile-extraction replay, install a
C++11 compiler and zlib as specified in the README, and run
\begin{verbatim}
python3 verify_package.py --full
\end{verbatim}
This also runs the supplementary sampling checks and the separate
consequence below. The extraction replay processes all 58 supplied
raw catalogue files using the original C++ extractor. Independent
NetworkX profile checks cover selected records. Catalogue completeness
is the external input stated in Section~\ref{article:sec:inputs}.

The local audit \path{replay_required_local_certificates.py} checks
all 2679 required certificates and their dependencies. The polygon and
coverage audits check that no needed degree or edge class has been
omitted. The package audit \path{audit_packaged_model.py} checks the
link between stored global rows and their source arrays, including the
five selected local inequalities. The final arithmetic is replayed by
\path{replay_global_certificate.py} and
\path{audit_global_exact_certificate.py}. Together these checks connect
the mathematical definitions, the stored coefficients, and the final
weighted sum.

A compact distribution omits the 58 raw catalogues and supplies
\path{restore_catalogues.py} to restore their exact recorded bytes.
Its \path{START_HERE.txt} gives the required extra step. The full
distribution requires no such restoration. Missing inputs, hash
mismatches, a nonzero exit status, or failed assertions mean that the
reproduction has not succeeded. Do not run optimized Python
(\texttt{-O} or \texttt{-OO}), since the checks use assertions.
No optimization solver is required for any of these replay commands.

\section*{A separate consequence, not used above}
A further audited consequence of the 2018 $R(5,5)\leq48$ computation
\cite[Sections~2 and~6]{article:r48} is $e(5,5,45)\geq462$. The proof above
uses only the bound 460; this additional result is not one of its
premises. Its separate derivation is summarized below.

Let $Y$ be a $(5,5)$-graph of order 44 or 45, and let $D_{24}$ be the
set of its vertices of degree 24. The cited gluing result and the
complete $(4,5,24)$ catalogue imply that $Y[D_{24}]$ has maximum
degree at most eight. Here gluing means combining two neighborhoods
along their common induced graph. In the cited computation, cores
smaller than 12 common neighbors either yield no graph or cannot be
extended by even one vertex. The subsequent catalogue calculation,
using the degree profiles, $e(4,5,23)=101$, and the three 22-vertex
$(4,5)$-graphs with 88 edges, proves $|D_{24}|\leq21$.
The full case argument is in \path{degree24_reduction.txt}; the
independent census code is \path{audit_degree24.py}.

To see why this gives the edge bound, take $X\in\R(5,5,45)$.
Both $X$ and its complement have maximum degree at most 24 because
$R(4,5)=25$. Hence every degree in $X$ is at least $44-24=20$.
A degree-20 vertex in $X$ has degree 24 in its complement, so there
are at most 21 such vertices. Every other vertex has degree at least
21. Therefore
\[
 2e(X)\geq21\cdot20+24\cdot21=924,
 \qquad e(X)\geq462.
\]
The nontrivial census statement $|D_{24}|\leq21$ belongs to the
separate argument just cited, not to this last handshaking calculation.

\section*{Acknowledgment}
The author was supported by the NRDI grant KKP~138270. 


\begin{thebibliography}{III.99}
\small
\bibitem[I.1]{article:survey}
S.~P.~Radziszowski, \emph{Small Ramsey Numbers},
Electronic Journal of Combinatorics, Dynamic Survey DS1,
revision~18, 24 April 2026, especially Table~Ib, p.~7.
\url{https://doi.org/10.37236/21};
\url{https://www.cs.rit.edu/~spr/ElJC/ejcram18.pdf}
\bibitem[I.2]{article:r55}
V.~Angeltveit and B.~D.~McKay, \emph{$R(5,5)\leq46$},
Journal of Graph Theory \textbf{112} (2026), 198--208.
Theorem~1.1; Appendix~A, Table~1.
\url{https://doi.org/10.1002/jgt.70029};
\url{https://arxiv.org/html/2409.15709v2}
\bibitem[I.3]{article:count}
B.~D.~McKay and S.~P.~Radziszowski,
\emph{Subgraph counting identities and Ramsey numbers},
J. Combinatorial Theory, Ser.~B \textbf{69} (1997), 193--209.
\url{https://users.cecs.anu.edu.au/~bdm/papers/r55.pdf}
\bibitem[I.4]{article:data}
B.~D.~McKay, \emph{Ramsey Graphs}, complete graph catalogues.
\url{https://users.cecs.anu.edu.au/~bdm/data/ramsey.html}
\bibitem[I.5]{article:r48}
V.~Angeltveit and B.~D.~McKay, \emph{$R(5,5)\leq48$}.
Journal of Graph Theory \textbf{89} (2018), 5--13.
\url{https://arxiv.org/abs/1703.08768}
\bibitem[I.6]{article:trianglefree}
J.~Goedgebeur and S.~P.~Radziszowski,
\emph{New Computational Upper Bounds for Ramsey Numbers $R(3,k)$},
Electronic Journal of Combinatorics \textbf{20}(1) (2013), P30.
Theorem~2. \url{https://doi.org/10.37236/2824}.
\bibitem[I.7]{article:localcert}
\emph{Electronic supplement to the present paper: exact local
Ramsey-profile certificates} (2026).
Mathematical description and provenance:
\path{LOCAL_CERTIFICATES.txt}.
Counting model: \path{recursive_profiles_v4.py}.
Certificate index: \path{edge_certification_summary.json}.
Independent verifier:
\path{replay_required_local_certificates.py}.
\end{thebibliography}