% Generated from the current standalone source; edit that source.
% Only title/contents wrappers and reference namespaces are changed.
\begin{abstract}
This supplement develops a worked example from the computer-assisted proof
of $R(5,6)\leq84$. We prove that a graph on 38 vertices containing neither
a clique of size four nor an independent set of size six has at most
314 edges. The proof starts with ten inequalities for edge and triangle
counts and pairs of incident edges in neighborhoods and nonneighborhoods.
Summing these inequalities and applying counting identities cancels
all quantities except the total number of edges. We give the complete
calculation, identify the finite checks that justify the ten inequalities, and show how the same calculation is
recorded by rational equation multipliers in the verification files.
We then explain how further valid counting inequalities are combined
with rational weights to rule out a counterexample on 84 vertices.
The final sections give commands for checking the worked example and
replaying the complete certificate.
\end{abstract}

\clearpage


\clearpage
\section{Notation and the information retained from a graph}
Write $\R(s,r,n)$ for the graphs on $n$ vertices containing neither a
clique of size $s$ nor an independent set of size $r$.
All graphs are finite and simple: edges are unordered pairs of distinct
vertices. A clique is a set of pairwise adjacent vertices; an independent
set is a set with no edges between its vertices. Two graphs have the same
isomorphism type if a bijection of their vertex sets preserves edges and
nonedges. The symbol $K_m$ denotes the complete graph on $m$ vertices.
For a graph $X$, write $V(X)$ and $E(X)$
for its vertex and edge sets and put $n=|V(X)|$ and $e(X)=|E(X)|$.
The number $t(X)$ is the number of unordered three-subsets inducing a
triangle. Write $N_X(v)$ for the neighbor set of $v$,
$d_v=d_X(v)=|N_X(v)|$, and $X[S]$ for the subgraph induced by
$S\subseteq V(X)$. Unqualified vertex sums run over $V(X)$.
Put
\[
 e=e(X),\qquad t=t(X),\qquad
 w=w(X)=\sum_{v\in V(X)}\bin{d_v}{2},\qquad q=q(X)=w-t.
\]
Here $w$ counts unordered pairs of distinct incident edges. An induced
three-vertex path contributes one to $w$, whereas a triangle contributes
three. Consequently
\begin{equation}\label{method:eq:q}
 q=\#\{\text{induced three-vertex paths}\}+2t.
\end{equation}
For example, $K_3$ has $(e,t,q)=(3,1,2)$, a three-vertex path has
$(2,0,1)$, and a matching of two edges has $(2,0,0)$.

For $0\leq k\leq3$, let $T_k(X)$ count the three-subsets of $V(X)$
inducing exactly $k$ edges. These four counts can be recovered
from the profile $(e,t,q)$:
\begin{equation}\label{method:eq:triples}
\begin{aligned}
 T_0(X)&=\bin n3-(n-2)e+q,\\
 T_1(X)&=(n-2)e-2q+t,\\
 T_2(X)&=q-2t,\\
 T_3(X)&=t.
\end{aligned}
\end{equation}
Indeed, $T_3=t$ and $T_2=q-2t$ follow from \eqref{method:eq:q}. Counting
incidences between edges and triples gives
$T_1+2T_2+3T_3=(n-2)e$, and the four counts sum to $\bin n3$.

For each vertex $v$, let
\[
 A_v=X[N_X(v)],\qquad
 B_v=X[V(X)\setminus(N_X(v)\cup\{v\})].
\]
If $X\in\R(s,r,n)$ and $d_v=d$, then
\begin{equation}\label{method:eq:families}
 A_v\in\R(s-1,r,d),\qquad B_v\in\R(s,r-1,n-1-d).
\end{equation}
The forbidden clique in the first assertion would extend by $v$;
the forbidden independent set in the second would extend by $v$.

A \emph{profile} of a graph is the tuple $(n,e,t,q)$. Many
nonisomorphic graphs can have the same profile. A profile file lists the
distinct tuples obtained from a graph catalogue. Its header records both
the number of graphs processed and the number of distinct profiles.
An inequality depending only on these four statistics can therefore be
checked once for each distinct profile.


\section{What the worked example establishes}
We first prove that every $X\in\R(4,6,38)$ has at most 314 edges.
In the proof of $R(5,6)\leq84$, such a graph occurs as the
neighborhood of a degree-38 vertex in a hypothetical graph on 84
vertices. After deriving the 314-edge bound, we explain how it enters
the counting argument for that hypothetical graph.

The proof of the 314 bound has two tasks. First, prove ten inequalities
for the smaller graphs $A_v$ and $B_v$. Second, add those inequalities
and use counting identities to cancel all unknown quantities except
$e(X)$. The cancellation is written out in Section~\ref{method:sec:worked}.
The input checks for the ten inequalities are described in
Sections~\ref{method:sec:inputs} and~\ref{method:sec:tables}.

A \emph{certificate} in this discussion is a recorded choice of rational
coefficients for such an addition of equations and inequalities.
The certificate specifies a weighted sum of valid counting statements.
Its verification consists of proving those statements and checking that
the specified sum has the claimed coefficients and sign.

The counting proofs below establish that every graph in the relevant
family satisfies the equations. The weighted sum for the worked example
can be checked on paper. The remaining finite calculation substitutes
profiles into the ten local inequalities; Section~\ref{method:sec:verify}
gives the command that performs these substitutions, followed by the
command for the complete 84-vertex proof.

Only the smaller graph families used as local inputs are enumerated.
The families $\R(4,6,38)$ and $\R(5,6,84)$ are treated through
necessary equations and inequalities for their subgraph counts. These
conditions give the edge bound in the first family and a contradiction
in the second.
\section{The first triangle double count}
We begin with a counting identity used at both the local and global
levels. Each triangle is an edge in the neighborhood of each of its three
vertices, so
\begin{equation}\label{method:eq:neighborhood-triangles}
 \sum_v e(A_v)=3t(X).
\end{equation}
For the nonneighborhoods, fix an edge $ab$. It appears in $B_v$ precisely
when $v$ is distinct from and nonadjacent to both $a$ and $b$. The number
of such vertices is
\[
 n-d_a-d_b+|N_X(a)\cap N_X(b)|.
\]
Summing over edges gives
\begin{equation}\label{method:eq:nonneighborhood-edges}
 \sum_v e(B_v)=ne(X)-\sum_v d_v^2+3t(X).
\end{equation}
In the last term, each triangle is counted once at each of its three
edges. Subtracting \eqref{method:eq:neighborhood-triangles} and using
$\sum_vd_v=2e(X)$ yields
\begin{equation}\label{method:eq:goodman}
 \sum_v\left(e(B_v)-e(A_v)-d_v\left(\frac n2-d_v\right)\right)=0.
\end{equation}
This is the three-vertex counting identity used in the certificate model;
see McKay and Radziszowski~\cite{method:count} and the formulation in
Angeltveit and McKay~\cite{method:r55}.

For a hypothetical $X\in\R(5,6,84)$, the external bounds
$R(4,6)\leq40$ and $R(5,5)\leq46$ imply
\[
 d_v\leq39,\qquad 83-d_v\leq45,
 \qquad\text{hence }d_v\in\{38,39\}.
\]
At order 84, \eqref{method:eq:goodman} is
\[
 \sum_v\left(e(B_v)-e(A_v)-d_v(42-d_v)\right)=0.
\]
The subtracted quantity is 152 at degree 38 and 117 at degree 39.
The following table summarizes four computational bounds used in the
main proof. Each entry bounds the number of edges of every graph in its
corresponding local family:
\[
\begin{array}{c|cc}
d_v&e(A_v)\text{ at most}&e(B_v)\text{ at least}\\\hline
38&314&460\\
39&324&432.
\end{array}
\]
They alone do not give a contradiction: they make the corresponding
summands at least $-6$ and $-9$. The full proof therefore retains further
local profile information and uses it in a larger counting model.
The next sections explain the first entry, 314, completely at the level
of its counting argument and its specified finite inputs.

\section{The worked example: its claim and local inputs}\label{method:sec:inputs}
\begin{proposition}\label{method:prop:314}
Subject to the catalogue and certified profile inputs stated below,
every $X\in\R(4,6,38)$ satisfies $e(X)\leq314$.
\end{proposition}
The inputs have two sources. Catalogue completeness is supplied by the
cited mathematical results. Containment in the outer profile polygons
is established by rational certificates in the verification package.
Both kinds of input provide inequalities for the smaller graphs that
can occur around a vertex of $X$.

A complete catalogue of $\R(s,r,m)$ lists a representative of every
isomorphism type in that family. Thus every graph with the specified
order and forbidden subgraphs is isomorphic to a listed graph. The
catalogues used here are supplied by McKay~\cite{method:data}; their precise
families are given below. A statement verified on every listed graph
applies to the entire family by this completeness property.

Fix such a graph $X$. Since $R(3,6)=18$ and $R(4,5)=25$, equation
\eqref{method:eq:families} gives
\[
 13\leq d_v\leq17,\qquad
 A_v\in\R(3,6,d_v),\qquad
 B_v\in\R(4,5,37-d_v).
\]
Thus $A_v$ is triangle-free, while the order of $B_v$ is between 20 and
24. Put
\begin{equation}\label{method:eq:constants}
\begin{array}{c|rrrrr}
d&13&14&15&16&17\\\hline
\alpha_d&346&280&179&80&-48\\
\beta_d=3d-38&1&4&7&10&13\\
K_d&184&143&131&111&114.
\end{array}
\end{equation}
The ten local assertions needed for the proof are
\begin{align}
 \alpha_d+(3d-38)e(A_v)-3q(A_v)&\geq0,\label{method:eq:A-local}\\
 K_d-3e(B_v)+3t(B_v)&\geq0.\label{method:eq:B-local}
\end{align}
The subscript $d$ specifies which of the five rows of constants is used.
For example, the $d=13$ assertions concern all possible neighborhoods of
order 13 and all possible nonneighborhoods of order 24 in $X$.
There are five assertions on triangle-free graphs and five on
$(4,5)$-graphs. Proving each assertion for every graph in its family
allows it to be applied at every vertex of $X$, whatever $X$ may be.

For \eqref{method:eq:A-local}, the input consists of the complete $\R(3,6,d)$
catalogues for $13\leq d\leq17$, supplied by McKay~\cite{method:data}.
Their extracted distinct profiles occur in the files with basenames
\path{r36_13.g6.gz.profiles} through \path{r36_16.g6.gz.profiles}, and
\path{r36_17.g6.profiles}. The degree 13 case, for instance, is the
concrete inequality
\[
 3q(Y)\leq346+e(Y)\qquad(Y\in\R(3,6,13)).
\]
Checking it amounts to substituting every distinct catalogue profile.

For \eqref{method:eq:B-local}, order 24 uses the complete catalogue represented
by \path{r45_24.g6.profiles}. Orders 20--23 use the outer profile
polygons stored in \path{computed_v3_45_20.json} through
\path{computed_v3_45_23.json}. These polygons contain all possible
$(t,q)$ pairs at their specified edge counts. A polygon may also contain
points that are not profiles of any graph. An inequality valid throughout the
polygon still applies to every graph profile contained in it.


Precisely, for any order $m$, clique parameter $s$, independent-set
parameter $r$, and integer $0\leq\eta\leq\binom m2$, define
\[
 \mathcal S_{s,r,m,\eta}
 =\{(t(Y),q(Y)):Y\in\R(s,r,m),\ e(Y)=\eta\}.
\]
A profile polygon $P_{s,r,m,\eta}\subseteq\mathbb R^2$ is a bounded
convex region containing this set, with coordinates denoted
$(\tau,\kappa)$. In this plane, an inequality such as
$\alpha\tau+\beta\kappa\leq c$ defines a half-plane, and finitely many
such inequalities bound the region. All coefficients and vertices used
here are rational. A segment or point is allowed.
An empty polygon is allowed only if the corresponding graph family
with edge count $\eta$ has been excluded. For a complete catalogue we
can take the convex hull of its actual $(t,q)$ pairs at edge count
$\eta$. Otherwise the certified inequalities define an outer polygon.
Write $V_{s,r,m,\eta}=\operatorname{vert}P_{s,r,m,\eta}$ for its finite
vertex set. In this example the neighborhood inputs are
$P_{3,6,d,\eta}$ and the nonneighborhood inputs are
$P_{4,5,37-d,\eta}$, for $13\leq d\leq17$.
A polygon vertex may have noninteger coordinates and need not be the
profile of any graph. Every actual profile is a convex combination of
these vertices at its own, unchanged, integer edge count. This is why
linear inequalities checked on the polygon's vertices hold for all
actual profiles it contains.

Explicitly, a convex combination of points $p_1,\ldots,p_k$ is
$\lambda_1p_1+\cdots+\lambda_kp_k$, with every $\lambda_i\geq0$ and
$\lambda_1+\cdots+\lambda_k=1$. For an affine function $L$, its value
at this combination is $\sum_i\lambda_iL(p_i)$. If all $L(p_i)$ are
nonnegative, so is the value at the actual profile. Thus checking the
polygon vertices proves the inequality for every graph whose profile lies
in the polygon. The edge count $\eta$ remains fixed during the combination; there is a separate polygon for each allowed edge count.

\section{A second identity, counted around triangles}\label{method:sec:second}
A second counting identity eliminates the profile terms that remain
after applying \eqref{method:eq:goodman}.

\begin{lemma}\label{method:lem:four}
For every graph $X$ on $n$ vertices,
\begin{equation}\label{method:eq:four-identity}
 \sum_v\bigl(d_v e(A_v)-q(A_v)+t(B_v)\bigr)=(n+3)t(X).
\end{equation}
\end{lemma}
\begin{proof}
For $0\leq i\leq3$, let $b_i$ count pairs $(T,z)$ in which $T$ is a
triangle, $z\notin T$, and $z$ has exactly $i$ neighbors in $T$.
Every triangle has $n-3$ possible external vertices, so
\begin{equation}\label{method:eq:b-total}
 b_0+b_1+b_2+b_3=(n-3)t(X).
\end{equation}
First,
\begin{equation}\label{method:eq:b-zero}
 \sum_v t(B_v)=b_0.
\end{equation}
Indeed, a triangle in $B_v$ is precisely a triangle with an external
vertex $v$ having no neighbors in it.

Next, each triangle $abc$ contributes $d_a+d_b+d_c$ to
$\sum_vd_ve(A_v)$. Its three internal edges contribute six to this
degree sum; its external vertices contribute their numbers of neighbors
in the triangle. Hence
\begin{equation}\label{method:eq:b-degree}
 \sum_vd_ve(A_v)=6t(X)+b_1+2b_2+3b_3.
\end{equation}
Finally,
\begin{equation}\label{method:eq:b-q}
 \sum_vq(A_v)=b_2+2b_3.
\end{equation}
One way to see this last equality is to inspect its possible four-vertex
configurations. An induced $K_4$ minus an edge has two universal
vertices, meaning vertices adjacent to all three others. In either
universal vertex's neighborhood the other three
vertices form an induced path; it therefore contributes two to the
left side. It also contains two choices of triangle with an external
vertex adjacent to exactly two triangle vertices, and contributes two
to $b_2$. A $K_4$ contributes $q(K_3)=2$ at each of its four vertices,
giving eight; it contributes four to $b_3$, also giving eight on the
right. No other induced four-vertex type contributes to either side.

Combining \eqref{method:eq:b-zero}--\eqref{method:eq:b-q}, the left side of
\eqref{method:eq:four-identity} becomes
$6t+b_0+b_1+b_2+b_3$. Equation \eqref{method:eq:b-total} completes the proof.
\end{proof}
For the worked example $n=38$, the right side is $41t(X)$. Although
$X$ is $K_4$-free in that application, the identity itself is universal.

\clearpage
\section{The complete weighted counting argument}\label{method:sec:worked}
Define the local nonnegative expressions
\[
 L_A(v)=\alpha_{d_v}+(3d_v-38)e(A_v)-3q(A_v),
 \qquad
 L_B(v)=K_{d_v}-3e(B_v)+3t(B_v).
\]
Their nonnegativity is exactly \eqref{method:eq:A-local} and
\eqref{method:eq:B-local}. The constants in \eqref{method:eq:constants} satisfy
\begin{equation}\label{method:eq:constant-polynomial}
 \alpha_d+K_d=1375-26d-3d^2\qquad(13\leq d\leq17).
\end{equation}
Checking the five rows of the table verifies this polynomial expression
for the combined constant term. It allows the sum of local inequalities
to be evaluated using the vertex degrees:

\begin{align*}
\sum_v\bigl(L_A(v)+L_B(v)\bigr)
&=\sum_v\bigl(1375-26d_v-3d_v^2\bigr)\\
&\quad+3\sum_v\bigl(d_ve(A_v)-q(A_v)+t(B_v)\bigr)\\
&\quad-38\sum_ve(A_v)-3\sum_ve(B_v)\\[2mm]
&=38\cdot1375-52e-3\sum_vd_v^2\\
&\quad+3\cdot41t-38\cdot3t
     -3\left(38e-\sum_vd_v^2+3t\right)\\[2mm]
&=52250-166e.
\end{align*}
The second equality uses, in order, the handshaking identity,
Lemma~\ref{method:lem:four}, \eqref{method:eq:neighborhood-triangles}, and
\eqref{method:eq:nonneighborhood-edges}. Both the degree-square terms and the
triangle terms cancel.

The resulting identity is the certificate for the edge bound:
\begin{equation}\label{method:eq:worked-certificate}
 \boxed{\quad52250-166e(X)
 =\sum_v\bigl(L_A(v)+L_B(v)\bigr)\geq0.\quad}
\end{equation}
It follows that
\[
 e(X)\leq\frac{52250}{166}=\frac{26125}{83}
      =314+\frac{63}{83}<315.
\]
Since $e(X)$ is an integer, $e(X)\leq314$, proving
Proposition~\ref{method:prop:314}.

This calculation reduces the edge bound to the ten local inequalities
\eqref{method:eq:A-local} and \eqref{method:eq:B-local}. The next section lists the
finite profile sets on which they are checked and the exact extremal
values obtained by the checker.

\clearpage
\section{Checking the ten local inequalities}\label{method:sec:tables}
For the $A$ side, the following table records the complete profile lists
used, the number of graphs from which they were extracted, and the
minimum of $L_A=\alpha_d+(3d-38)e-3q$ on those lists.
\begin{center}
\begin{tabular}{rrrrl}
\toprule
$d$&Graphs&Distinct profiles&$\min L_A$&One minimizing $(e,t,q)$\\
\midrule
13&275086&138&0&$(32,0,126)$\\
14&263520&118&0&$(35,0,140)$\\
15&64732&68&0&$(37,0,146)$\\
16&2576&31&0&$(40,0,160)$\\
17&7&3&0&$(42,0,166)$\\
\bottomrule
\end{tabular}
\end{center}
The degree 13 minimizing example gives $346+32-3\cdot126=0$.
The degree 17 example gives $-48+13\cdot42-3\cdot166=0$.
These substitutions illustrate the arithmetic, but the universal
statement requires checking every profile in the relevant list.

For the $B$ side, $L_B$ depends only on $e-t$, not on $q$. Thus it
is enough to maximize $e-t$ on the appropriate profile set. At order
24 the set is the catalogue's distinct profiles; at orders 20--23 it
is the union of the vertices of the certified polygons at each edge
count. The results are
\begin{center}
\begin{tabular}{rrrrrl}
\toprule
$d$&$|B_v|$&Profile points&$\max(e-t)$&$\min L_B$&Minimizing $(e,t,q)$\\
\midrule
13&24&1488&$-2$&190&$(118,120,924)$\\
14&23&184&21&80&$(105,84,771)$\\
15&22&235&31&38&$(94,63,649)$\\
16&21&268&37&0&$(83,46,528)$\\
17&20&299&38&0&$(75,37,453)$\\
\bottomrule
\end{tabular}
\end{center}
For example, at $d=15$ the largest possible $e-t$ in the outer
profile set is 31, giving $L_B\geq131-3\cdot31=38$.
At $d=16$, the corresponding calculation is $111-3\cdot37=0$.

An affine function on a polygon achieves its minimum at a vertex.
Consequently, checking polygon vertices is sufficient even if the
polygon contains many additional integer points or unrealizable
profiles. When actual profiles are used directly, completeness of the
underlying catalogue establishes that every graph profile has been checked.

The program \path{check_local_example.py} performs these substitutions
using exact rational arithmetic. It also checks the polynomial
identity \eqref{method:eq:constant-polynomial} and the agreement with the saved
equation multipliers. The program computes the minima from the supplied
profile sets.

\clearpage
\section{Where the profile restrictions come from}\label{method:sec:profiles}
The complete triangle-free catalogues and the complete order 24
$(4,5)$ catalogue are external inputs~\cite{method:data}. The supplied graph6
files encode the graphs. The extractor \path{catalogue_profiles.cpp}
computes their exact profiles. The distinct-profile sets can be
regenerated exhaustively with \path{regenerate_catalogue_profiles.py}
and compared with the supplied sets. The independent catalogue audit
additionally checks graph counts and sampled profile computations by a
different graph decoder. Sampling is not an exhaustive independent
recomputation, and none of these checks re-proves catalogue completeness.

The order 20--23 $(4,5)$ profile polygons are derived from still smaller
graphs. For a fixed order $m$ and edge count $\eta$, the unknown graph has
neighborhoods in $\R(3,5,d)$ and nonneighborhoods in
$\R(4,4,m-1-d)$. Their complete smaller catalogues supply admissible
profiles: the $(3,5)$ catalogues have order at most 13 and the $(4,4)$
catalogues have order at most 17. Counting triples and four-vertex
configurations imposes equations on how many local profiles can occur.
We retain these equations and nonnegativity, but allow real weights
and do not require them to arise from a graph. This enlarged system
is called a \emph{linear relaxation}. Every graph gives a solution of
the system, although some solutions may have no corresponding graph.
A bound valid for every solution therefore holds for every graph.
Section~\ref{method:sec:dual} constructs this assignment explicitly.

To obtain a polygon, we prove lower and upper bounds on eight
linear combinations of $t$ and $q$. The coefficient pairs are
\[
 (1,0),\ (0,1),\ (1,1),\ (1,-1),\
 (1,2),\ (2,1),\ (1,-2),\ (2,-1).
\]
For a direction $(a,b)$, the quantity $at+bq$ is integral. If an exact
rational certificate shows $at+bq>k-1$, where $k$ is an integer, then
$at+bq\geq k$. Upper bounds are treated by changing the sign.
Intersecting these integer half-planes produces an outer polygon.
For example, $(a,b)=(1,0)$ bounds the number of triangles, whereas
$(a,b)=(1,-1)$ bounds $t-q$. Every graph profile satisfies all these
bounds and therefore lies in their half-plane intersection.

Each defining half-plane is justified by an exact rational certificate.
The polygon audit then reconstructs their intersection over the rational
numbers and compares its vertices with the stored vertex list. These
checks establish both that every graph satisfies the defining
inequalities and that the stored vertices describe their full
intersection. The files also contain \texttt{raw} numerical estimates
used to select the integer cutoffs; verification uses the exact
certificates at those cutoffs.

Across orders 19--23, the full dependency chain uses 1968 exact
certificates for the defining half-planes. Twenty-six additional edge
classes use complete extreme-edge catalogues. These certificates form the shared set of
prerequisites for the local bounds used in the complete proof. Their
reconstruction and verification are specified in the companion mathematical specification.

The verified minimum and maximum edge counts for $(4,5)$ graphs of
orders 19--24 are, respectively,
\[
 [57,92],\ [68,100],\ [77,107],\ [88,114],\ [101,122],\ [116,132].
\]
Their published source is Table 1 in Appendix A of~\cite{method:r55}.
They delimit the edge classes that must be covered. The coverage audit
checks that each edge count in these intervals has either a complete
catalogue or a certified containing polygon.

\clearpage
\section{Profile variables and the saved equation multipliers}\label{method:sec:dual}
The file \path{edge_46_38_max.json} stores the same numerical bound
as \eqref{method:eq:worked-certificate}, but in coordinates adapted to a general
counting model. This section identifies those coordinates and all
nonzero multipliers, making the relation explicit.

For $X\in\R(4,6,38)$, the numbers of vertices with each possible
neighborhood profile sum to 38, and their degree-weighted sum is
$2e(X)$. To express these counts using the available containing polygons,
write each actual profile as a convex combination of polygon vertices.
Aggregating those coefficients over the vertices of $X$ gives
nonnegative profile weights. They preserve the two sums just described
and all other statistics that are affine in a local profile.

Put $D=\{13,14,15,16,17\}$. The polygon vertices in
Section~\ref{method:sec:inputs} determine finite index sets
\[
\begin{split}
 \mathcal I_A={}&\{(d,\eta,\tau,\kappa):d\in D,\quad
 \eta\in\{0,\ldots,\tbinom d2\},\quad
 (\tau,\kappa)\in V_{3,6,d,\eta}\},\\
 \mathcal I_B={}&\{(h,\eta,\tau,\kappa):h=37-d,\ d\in D,\quad
 \eta\in\{0,\ldots,\tbinom h2\},\quad
 (\tau,\kappa)\in V_{4,5,h,\eta}\}.
\end{split}
\]
There is one nonnegative real variable $a_{d,\eta,\tau,\kappa}$ per
index in $\mathcal I_A$ and one $b_{h,\eta,\tau,\kappa}$ per index in
$\mathcal I_B$. For brevity put $p=(\eta,\tau,\kappa)$ and write
$a_{d,p}$ and $b_{h,p}$ for these same variables. Thus the first index
always denotes the order of the local graph: $d$ for a neighborhood
and $h=37-d$ for a nonneighborhood. Each sum over $p$ below is restricted
to the indices belonging to its indicated order and side.

Here is the assignment supplied by an actual $X\in\R(4,6,38)$.
For each $v$ of degree $d$, choose nonnegative coefficients
$\lambda^A_{v,p}$ with sum one, supported only on
$p=(e(A_v),\tau,\kappa)$ with
$(\tau,\kappa)\in V_{3,6,d,e(A_v)}$, such that
\[
 (t(A_v),q(A_v))=\sum_p\lambda^A_{v,p}(\tau,\kappa).
\]
They exist because the actual pair lies in that polygon. Similarly
choose nonnegative coefficients $\lambda^B_{v,p}$ with sum one,
supported on $p=(e(B_v),\tau,\kappa)$ with
$(\tau,\kappa)\in V_{4,5,37-d,e(B_v)}$, whose convex combination
of $(\tau,\kappa)$ equals $(t(B_v),q(B_v))$.
Define
\[
 a_{d,p}=\sum_{v:d_v=d}\lambda^A_{v,p},\qquad
 b_{h,p}=\sum_{v:d_v=37-h}\lambda^B_{v,p},
\]
where missing coefficients are zero. These variables are aggregate
convex-combination weights; they do not count vertices whose local graph
has the polygon-vertex profile $p$. They can be fractional and their
representation can be nonunique, even for one fixed graph.
Nevertheless,
\[
 m_d:=\sum_p a_{d,p}=\sum_p b_{37-d,p}=\#\{v:d_v=d\},
 \qquad \sum_{d,p}a_{d,p}=38.
\]
The symbol $m_d$ denotes this common degree-class weight; only for an
assignment supplied by a graph must it be an integer.

For a concrete example, the catalogue
\path{r36_13.g6.gz.profiles} has exactly three profiles with 16 edges,
whose $(t,q)$ coordinates are
\[
(0,25),\qquad(0,26),\qquad(0,28).
\]
Their convex hull is the segment with endpoints $(0,25)$ and $(0,28)$.
If a vertex of $X$ has neighborhood profile $(13,16,0,26)$, then
\[
(0,26)=\frac23(0,25)+\frac13(0,28)
\]
assigns weight $2/3$ to $a_{13,16,0,25}$ and weight $1/3$ to
$a_{13,16,0,28}$. These contributions total one vertex, preserve its
16 local edges and zero local triangles, and give weighted $q$ value
$(2/3)25+(1/3)28=26$. The example uses a profile in the smaller
catalogue and shows how any occurrence of that profile would be
represented. The aggregated variables are consequently allowed to
be fractional, even when they arise from a graph.

The linear functions of the profile weights representing ambient
statistics are
\[
 \mathcal E=\frac12\sum_{d,p}d\,a_{d,p},\qquad
 \mathcal T=\frac13\sum_{d,p}\eta\,a_{d,p},\qquad
 \mathcal W=\sum_{d,p}\binom d2 a_{d,p},\qquad
 \mathcal Q=\mathcal W-\mathcal T.
\]
On the graph assignment these equal $e(X),t(X),w(X),q(X)$.
Likewise a local expression affine in $(\eta,\tau,\kappa)$ at fixed
order is evaluated by its weighted sum. For example,
$\sum_vT_k(A_v)$ means $\sum_{d,p}T_k(d,p)a_{d,p}$, where
$T_k(d,p)$ is obtained from \eqref{method:eq:triples} by substituting
$(n,e,t,q)=(d,\eta,\tau,\kappa)$; the analogous expression for $B$
uses $(h,p)$ and $b_{h,p}$. Convex combinations preserve these affine
expressions, so these weighted sums equal the graph counts whenever
the variables come from a graph.

Add a variable $z_F\geq0$ for each of the eleven unlabelled four-vertex
graph types $F$, and $j_{d,f}\geq0$ for each $d,f\in D$ with $d\leq f$.
For a graph assignment, $z_F$ counts four-subsets inducing $F$ and
$j_{d,f}$ counts unordered edges with endpoint degrees $d,f$.
The relaxation permits real values but imposes the counting equations.
One coordinate is known to be zero: $z_{K_4}=0$, because the ambient
graph $X\in\R(4,6,38)$ contains no complete four-vertex subgraph.
Counting the ends of edges incident with degree-$d$ vertices gives
one equation for each degree class:
\[
 2j_{d,d}+\sum_{f<d}j_{f,d}+\sum_{f>d}j_{d,f}=d\,m_d\qquad(d\in D).
\]
Counting unordered paths on four distinct vertices by their central
edge gives another equation; the paths are not required to be induced:
\[
 \sum_{d\leq f}(d-1)(f-1)j_{d,f}-3\mathcal T
 =\sum_F \operatorname{path}_4(F)z_F,
\]
where $\operatorname{path}_4(F)$ is the number of such paths in $F$.
All other rows appear in Section~\ref{method:sec:multipliers}.

The following elementary example illustrates how a weighted sum of
equations proves a bound. Let $u_1,u_2,u_3$ be nonnegative numbers satisfying
\[
u_1+u_2=5,\qquad u_2+u_3=4.
\]
Multiply the first equation by 2 and the second by 1, then add:
\[
2u_1+3u_2+u_3=14.
\]
To bound the slightly different expression $3u_1+3u_2+u_3$, write
\[
3u_1+3u_2+u_3=14+u_1\geq14.
\]
The equation multipliers $(2,1)$ supply a certificate for the lower
bound 14: subtracting the weighted equations from the desired
expression leaves the nonnegative quantity $u_1$. The same calculation
applies to every nonnegative solution of the two equations. The local
graph certificate uses this operation with its profile weights and
counting equations.

There are 107 neighborhood profile variables, 1084 nonneighborhood
profile variables, 15 degree-pair variables, and 11 four-vertex
variables. Let $\mathbf u=(u_0,\ldots,u_{1216})^T$ list them in the
order used by the supplied program. There are 25 counting equations.
Write the $i$th equation as
\[
\sum_{j=0}^{1216}m_{ij}u_j=b_i\qquad(0\leq i<25).
\]
The matrix $M=(m_{ij})$ is the rectangular table of their
coefficients, and $\mathbf b=(b_0,\ldots,b_{24})^T$ is the vector
of right-hand sides. Thus $M\mathbf u=\mathbf b$ abbreviates these
25 equations; $\mathbf u\geq0$ abbreviates the 1217 nonnegativity
conditions. The additional condition $z_{K_4}=0$ is retained.

We seek an upper bound on $e(X)$, so we seek a lower bound on its
negative, $-\mathcal E$. Define $c_j$ to be the coefficient of $u_j$
in this linear expression; then $-\mathcal E=\sum_jc_ju_j$.
Choose rational multipliers $y_0,\ldots,y_{24}$ for the counting
equations. Their weighted sum is
\[
\sum_j\left(\sum_i y_i m_{ij}\right)u_j=\sum_i y_i b_i.
\]
Subtracting this from $\sum_jc_ju_j$ leaves coefficient
$c_j-\sum_i y_i m_{ij}$ on $u_j$. If each such coefficient is
nonnegative, the target is at least the constant $\sum_i y_i b_i$.
The sign of the coefficient on $z_{K_4}$ is immaterial because that
coordinate is zero. It is therefore sufficient to check the signs on
all remaining coordinates.

With $\mathbf c=(c_j)^T$, $\mathbf y=(y_i)^T$, and superscript $T$
denoting transpose, the preceding calculation can be abbreviated as
\begin{equation}\label{method:eq:dual-principle}
 \mathbf c^T\mathbf u=\mathbf y^T\mathbf b+
                 (\mathbf c-M^T\mathbf y)^T\mathbf u.
\end{equation}
The vector $\mathbf c-M^T\mathbf y$ is called the \emph{residual}.
The checker verifies its coordinate signs and the exact value of
$\mathbf y^T\mathbf b$. It also reconstructs the equations and the
objective so that the calculation is tied to the stated graph problem.
The list of equation multipliers $\mathbf y$ is stored in the JSON
field \texttt{dual}.
In the following row table, $e,t,w$ abbreviate
$\mathcal E,\mathcal T,\mathcal W$; graph-style sums of local counts
abbreviate the affine weighted sums just defined.

The certificate contains 25 equation multipliers, 17 of them nonzero.
The degree-pair equations and
the path equation have zero multiplier in this example. Thus they
contribute nothing to this particular weighted sum, although they
are useful for other certificates.

After the weighted sum is expanded, the coefficient of $a_{d,p}$ is
\[
 \frac{\alpha_d+(3d-38)\eta-3\kappa}{166}
       -\frac{4101}{220780}\,\tau.
\]
All the neighborhood polygon vertices come from triangle-free catalogues,
so $\tau=0$. The coefficient of $b_{37-d,p}$ is
$(K_d-3\eta+3\tau)/166$. Every degree-pair coefficient is
zero. The four-vertex coefficients are zero except that of $K_4$,
which is $4101/55195$ and multiplies a zero variable. Equation
\eqref{method:eq:dual-principle} is therefore precisely
\eqref{method:eq:worked-certificate} divided by 166.

\clearpage
\section{The multipliers and their normalization}\label{method:sec:multipliers}
For completeness, the entire multiplier vector is tabulated below in
the exact row order used by \path{recursive_profiles_v4.py}. Here
$U_k(F)$ is the number of universal vertices of $F$ whose deletion
leaves a triple with $k$ edges; $Z_k(F)$ is the corresponding number
of isolated vertices (vertices of degree zero). Quantities such as
$e,t,w$ in the equations
are linear functions of the profile weights.

The rows arise from the following incidence counts. Each
four-subset has one induced type, giving row 7. Each edge belongs
to $\binom{36}{2}$ four-subsets, and each triangle or pair of
incident edges belongs to 35 four-subsets, giving rows 8--10.
For row 11, a triple in $A_v$ together with $v$ is a four-set in
which $v$ is universal. Counting these pairs first by $v$ gives
the left sum, and first by the induced four-vertex type gives
the right sum. The same argument applies to each triple edge
count and, for $B_v$, to an isolated fourth vertex. Each row therefore
holds for every graph in the ambient family.
\begin{center}\small
\begin{tabular}{r p{91mm} r}
\toprule
Row&Equation, written with the displayed left side&Multiplier\\
\midrule
0&$\sum a=38$&$-6902/1577$\\
1&$\sum_p a_{13,p}-\sum_p b_{24,p}=0$&$5014/55195$\\
2&Matching weights at degree 14&$-11/380$\\
3&Matching weights at degree 15&$47/3154$\\
4&Matching weights at degree 16&$0$\\
5&Matching weights at degree 17&$66/581$\\
6&Twice the left side of \eqref{method:eq:goodman}, with $n=38$&$3/332$\\
7&$\sum_F z_F=\bin{38}{4}$&$-111/55195$\\
8&$2\sum_F e(F)z_F-2\bin{36}{2}e=0$&$111/220780$\\
9&$3\sum_F t(F)z_F-3\cdot35t=0$&$-1/166$\\
10&$\sum_F w(F)z_F-35w=0$&$-111/220780$\\
11&$\sum_vT_0(A_v)-\sum_FU_0(F)z_F=0$&$-111/220780$\\
12&Same equation with $T_1,U_1$&$-4101/220780$\\
13&Same equation with $T_2,U_2$&$-4101/220780$\\
14&Same equation with $T_3,U_3$&$0$\\
15&$\sum_vT_0(B_v)-\sum_FZ_0(F)z_F=0$&$-111/220780$\\
16&Same equation with $T_1,Z_1$&$-111/220780$\\
17&Same equation with $T_2,Z_2$&$-111/220780$\\
18&Same equation with $T_3,Z_3$&$-4101/220780$\\
19--23&Degree-stub equations for $d=13,\ldots,17$&$0$\\
24&Four-vertex path identity&$0$\\
\bottomrule
\end{tabular}\end{center}
Row 6 uses the program's normalization: twice the left side of
equation \eqref{method:eq:goodman}; its multiplier $3/332$ therefore has the
same effect as multiplying the simplified equation by $3/166$.
Rows 8 and 9 similarly retain the program's factors 2 and 3, so that
the multipliers in this table can be compared directly with the JSON.
Only rows 0 and 7 have nonzero right sides. Their contribution is
\[
 -\frac{6902}{1577}\,38
 -\frac{111}{55195}\bin{38}{4}
 =-\frac{26125}{83}.
\]
This is the field \texttt{exact\_lower\_bound} in the JSON file.
Because the objective is $-e$, a lower bound on the objective is an
upper bound on $e$. The field \texttt{threshold} is $-315$:
the certified objective is strictly greater than that threshold,
which gives the integral conclusion $e\leq314$.

The multiplier signs are unrestricted because the multiplied rows
are equalities. The signs of the resulting residual coefficients,
not the signs of these equality multipliers, justify the inequality.
This distinction is useful when inspecting a certificate with many
negative entries.

\clearpage
\section{What the remaining local computations add}
The same mechanism proves the other endpoint bounds used in the main
paper. For a $(4,6)$-graph, the smaller inputs are again $(3,6)$
neighborhoods and $(4,5)$ nonneighborhoods. For a $(5,5)$-graph,
they are $(4,5)$ neighborhoods and $(5,4)$ nonneighborhoods.
Complementation exchanges edges and nonedges and turns a $(5,4)$-graph
into a $(4,5)$-graph of the same order. Thus the same $(4,5)$ input
catalogues and polygons provide bounds for both sides.

To see how the counts are obtained, write $\overline Y$ for the
complement of a graph $Y$ on $m$ vertices. From the triple counts
in \eqref{method:eq:triples},
\[
\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}
\]
The second line is $T_0(Y)$, and the third is $T_1(Y)+2T_0(Y)$.
These are affine transformations of the profiles, so they also
preserve the validity of containing polygons under complementation.

Some endpoint bounds have an immediate integrality step. For example,
\[
 e(Y)\geq\frac{95414}{221}>431
 \quad\Longrightarrow\quad e(Y)\geq432
 \qquad(Y\in\R(5,5,44)).
\]
The corresponding file is \path{edge_55_44_min.json}. For order 45,
\path{edge_55_45_min.json} gives
\[
 e(Y)\geq\frac{12137627230191}{26402663302}>459,
 \qquad\text{hence }e(Y)\geq460.
\]
These bounds are obtained by checking the rational equation
multipliers in the two files using exact arithmetic.

The order 39 $(4,6)$ bound has a useful extra step. The initial
certificate proves $e(Y)\leq325$. Fixing $e(Y)=325$, two further
certificates give
\[
 t(Y)\geq\frac{1612}{3},\qquad
 -t(Y)\geq-\frac{1612}{3}.
\]
Thus $t(Y)=1612/3$, impossible for an integer triangle count. This
excludes the endpoint and yields $e(Y)\leq324$. The files
\path{exclude_4639e325_t_gt537.json} and
\path{exclude_4639e325_t_lt538.json} encode the two sides. Their
filenames refer to the neighboring integer thresholds; the exact
certified value is the rational number displayed above.

To describe the five remaining local inequalities, return to a
hypothetical $X\in\R(5,6,84)$ and take $A_v,B_v$ to be its
neighborhood and nonneighborhood graphs. The inequalities have the form
\[
 \gamma_d d+\gamma_e e(Y)+\gamma_t t(Y)+\gamma_q q(Y)+\gamma_0\leq0,
\]
for $Y=A_v$ or $B_v$ in the 84-vertex graph, where $d=d_X(v)$
and $(\gamma_d,\gamma_e,\gamma_t,\gamma_q,\gamma_0)$ is the fixed
coefficient vector of the chosen inequality. The five vectors are
recorded in \path{exact_candidate_used_facets.json}. The identifiers
203, 595, 603, 658 and 681 are lookup keys for these five stored
inequalities; they identify entries in that file. Each inequality is
proved in every possible edge class of its local family by a weighted
sum of counting equations. The inputs are the smaller profile sets
already described. In particular, the proof requires no catalogue of
all 38-, 39-, 44- or 45-vertex graphs. For example, identifier 203 means
\[
770d-269e(Y)-6t(Y)+12q(Y)+5940\leq0
\qquad(Y=A_v).
\]
At $d=38$ and $e(Y)=314$, the statement becomes
$-6t(Y)+12q(Y)\leq49266$.
The file \path{facet203_46_n38_e314.json} supplies equation
multipliers proving
\[
6t(Y)-12q(Y)\geq-\frac{541956}{11}>-49272.
\]
Since $-6t(Y)+12q(Y)$ is a multiple of 6, this proves the required
bound 49266. It proves it for every graph in the edge class, by the
same graph-to-equations implication as in the worked example.

For identifier 203, the edge classes are $267,\ldots,314$ at order
38 and $288,\ldots,324$ at order 39: 85 cases. Each of the other
four inequalities concerns nonneighborhoods, with edge classes
$432,\ldots,514$ at order 44 and $460,\ldots,530$ at order 45:
154 cases per inequality. Thus there are $85+4\cdot154=701$
checks of rational equation multipliers. The endpoint bounds justify
excluding all other edge counts. The verifier reconstructs this
entire case list so that an absent case cannot silently disappear
from the proof.

The complete local dependency chain consists of 1968 prerequisite
half-plane certificates, ten endpoint and exclusion certificates, and
701 certificates for these five further inequalities: 2679 in total.
The verifier \path{replay_required_local_certificates.py} checks that
entire chain, including the list of required cases and the arithmetic
of each certificate.

\clearpage
\section{Why the global proof uses seven-vertex graphs}
Suppose again that $X\in\R(5,6,84)$ exists. Every seven-vertex induced
subgraph belongs to one of 979 allowed isomorphism types: those with
neither a $K_5$ nor an independent six-set. Let $\mathcal H$ be this
finite set and put
\[
 p_H=\frac{\#\{W\subseteq V(X):|W|=7,\ X[W]\cong H\}}
                {\bin{84}{7}}.
\]
Then $p_H\geq0$ and $\sum_Hp_H=1$. Equivalently, $p_H$ is the
probability that a uniformly chosen seven-subset induces type $H$.

A rooted graph has specified distinguished vertices, called roots;
an isomorphism of rooted graphs must fix each specified root label.
A flag specifies the induced rooted isomorphism type on a chosen set
containing the roots. Its indicator is 1 if the chosen vertices have
that type and 0 otherwise. Thus multiplying an inequality by a flag
indicator restricts the count to those root configurations.

Many local counting expressions can be expanded as linear functions
of the $p_H$. For instance, one can multiply a valid inequality by
the indicator of a prescribed rooted graph and average over roots.
The multiplier is nonnegative, so the averaged inequality is valid.
Lifting the five local inequalities in this way retains information
about how neighborhoods sit inside the ambient graph.

For example, fix a six-vertex flag with a distinguished root $v$,
and let $r_0$ be the number of its other five vertices adjacent to $v$.
There are 78 vertices outside this flag. Choose one uniformly, and
let $\chi$ be 1 if it is adjacent to $v$, and 0 otherwise. The
average of $r_0+78\chi$ is exactly $d_v$, because the chance that
$\chi=1$ is $(d_v-r_0)/78$. The quantity $r_0+78\chi$ can be
read from the induced seven-vertex graph, although $d_v$ cannot.
Thus the universally valid bound $d_v\leq39$ produces an inequality
on averages of seven-vertex statistics. This replacement by a statistic
with the same average is what the general count conversion does.

The normalization follows by comparing counts in a seven-set with
counts in the full graph. If an expression uses $m$
vertices outside a fixed flag on $f$ vertices, where $0\leq m\leq7-f$, a seven-set contains
only $7-f$ available positions while the full graph has $84-f$.
The corresponding count conversion includes the exact factor
\[
 \frac{\bin{84-f}{m}}{\bin{7-f}{m}}.
\]
When two extension sets are counted together, the conversion is
performed separately for each possible size of their intersection.
Including these overlap cases makes the conversion an exact identity
for a graph on 84 vertices.

The linear rows include the degree restriction $d_v\in\{38,39\}$,
capacities of common neighborhoods, local edge and profile bounds,
and elementary constraints on integer cell sizes. Here a mixed cell is
\[
 \mathcal C(C,D)=\{x\in V(X)\setminus(C\cup D):
 C\subseteq N_X(x),\quad D\cap N_X(x)=\varnothing\},
\]
where the specified root sets $C,D$ are disjoint, $C$ is a clique, and
$D$ is independent. The cell size is $c=|\mathcal C(C,D)|$. For any integer
$c$ and integer $k$,
\[
 (c-k)(c-k-1)\geq0.
\]
This inequality holds for each choice of roots and hence also after
averaging over root configurations. Other rows use the fact that
$d_v-38$ and $39-d_v$ take only the values zero and one.
For example, when $C$ is the two endpoints of an edge and $D$ is
empty, the cell is their common neighborhood. A triangle in that
cell would form a $K_5$ with the two roots; an independent six-set
there would also be forbidden in $X$. It is therefore a $(3,6)$-graph,
so its size is at most 17. The general definition treats mixed
adjacency and nonadjacency requirements in the same explicit way.

The 979-type list is itself audited: all $2^{21}$ labelled graphs on
seven vertices are enumerated, forbidden patterns are excluded, and
counts are compared with the orbit sizes of the representatives.
This verifies a finite enumeration used internally by the proof.
It is logically separate from the completeness of the external
Ramsey graph catalogues.

\section{The positive-semidefinite inequalities are sums of squares}
The final certificate contains inequalities that are most compactly
expressed with positive-semidefinite matrices. Their validity comes
from an elementary square-counting observation.

Fix a labelled root graph $\sigma$ on $\{1,\ldots,\ell\}$ and
an integer $k\geq0$ with $\ell+2k\leq7$. A root tuple is an injection
$\rho:\{1,\ldots,\ell\}\to V(X)$ inducing $\sigma$.
Let $\mathcal F_{\sigma,k}$ be the finite set of rooted isomorphism
types on $\ell+k$ vertices whose labelled roots induce $\sigma$ and
which contain neither a $K_5$ nor an independent six-set. Isomorphisms
fix the root labels and may permute the $k$ nonroot vertices.
For each $i\in\mathcal F_{\sigma,k}$ define
\[
 f_i(\rho)=\#\{S\subseteq V(X)\setminus\operatorname{im}\rho:
 |S|=k,\ (X[\operatorname{im}\rho\cup S],\rho)\text{ has type }i\}.
\]
Write $f(\rho)$ for the column vector with these coordinates. For any
real vector $z=(z_i)_{i\in\mathcal F_{\sigma,k}}$,
\[
 \sum_{\rho}\bigl(z^Tf(\rho)\bigr)^2\geq0.
\]
The sum runs over all root injections of type $\sigma$, including the
unique empty injection when $\ell=0$. Thus
$\sum_\rho f(\rho)f(\rho)^T$ is positive semidefinite. Expanding a
square counts ordered pairs of extension sets, including equal or
overlapping sets.
For instance, choosing coefficients 1 and $-2$ on two extension
types gives $(f_1(\rho)-2f_2(\rho))^2\geq0$. Its cross term
$-4f_1(\rho)f_2(\rho)$ counts choices of one extension of each
type with the indicated coefficient. The full matrix records
all such products at once. Positive semidefinite means that every
choice of real coefficients yields a nonnegative quadratic
expression; here that property is proved by the displayed squares.

For each $H\in\mathcal H$, define a matrix $M_H$ with rows and
columns indexed by $\mathcal F_{\sigma,k}$. Its $(i,j)$ entry is a sum
over root injections $\rho$ into $H$ and ordered pairs of $k$-subsets
$S,T\subseteq V(H)\setminus\operatorname{im}\rho$ having types $i,j$.
Give each such configuration weight
\[
 \frac{1}{\bin{84-\ell-|S\cup T|}{7-\ell-|S\cup T|}}.
\]
Its denominator is the number of seven-subsets of $V(X)$ containing
that configuration's roots and extension vertices. Thus summing over
seven-sets counts each full-graph configuration exactly once:
\[
 \sum_{\substack{W\subseteq V(X)\\|W|=7}}M_{X[W]}
   =\sum_\rho f(\rho)f(\rho)^T,
 \qquad \sum_{H\in\mathcal H}p_HM_H\succeq0.
\]
The latter matrix is the former divided by $\binom{84}{7}$.
All pairs $(S,T)$, including $S=T$, enter the definition of $M_H$.

For each fixed pair $(\sigma,k)$, choose a positive common denominator
$L$ and put $I_H=LM_H$ for every $H\in\mathcal H$. The same positive
factor throughout the block makes every $I_H$ integral and preserves
the sign. Every supplied integer vector $z$ gives the valid row
\[
 \sum_{H\in\mathcal H}p_H\bigl(-z^TI_Hz\bigr)\leq0.
\]
The final sum uses 194 such rows, drawn from eight blocks with
$(\ell,k)=(0,3),(1,3),(2,2),(3,2)$: respectively one, one, two,
and four root isomorphism types. Each root type has a fixed labelling;
all injections of that labelled type are counted. The entries can be
recomputed by integer arithmetic, and the displayed sum of squares
proves the sign.

The accompanying files \path{rational_psd_vectors.json} and
\path{moment_integer_verified.npz} specify the vectors and integer
matrices. The array \path{rational_psd_numerators.npy} records their
contractions. The independent verifiers recompute these contractions
and compare them with the saved array.

\section{The final exact separation}
For $0\leq i<5324$, let $U_i:\mathcal H\to\mathbb Q$ be an
inequality row: 4876 linear counting rows and 448 square rows. For
$0\leq j<89$, let $E_j:\mathcal H\to\mathbb Q$ be a homogeneous
equality row. An integer row $(a_H)_{H\in\mathcal H}$ is normalized
by division by $d=\max\{1,\max_H|a_H|\}$. The normalization equation
$\sum_Hp_H=1$ is separate and is not homogeneous. Validity means
\[
 \sum_Hp_HU_i(H)\leq0,
 \qquad\sum_Hp_HE_j(H)=0.
\]
An inequality row is therefore a list of 979 rational coefficients,
one per seven-vertex type. Its validity concerns the weighted average of
those coefficients with the frequencies supplied by an actual 84-vertex graph; individual
coefficients can have either sign. The equality rows have zero
right-hand side, which is the meaning of ``homogeneous'' here.
The final file \path{exact_separation_certificate.json} supplies
nonnegative rational weights $\lambda_i$ and arbitrary rational
weights $\mu_j$. It uses 816 inequality rows, of which 194 are
the square rows just discussed, and 87 equality rows. Thus there
are 903 nonzero weights.

For every allowed seven-vertex type, define
\[
 C(H)=\sum_i\lambda_iU_i(H)+\sum_j\mu_jE_j(H).
\]
The exact computation establishes
\begin{equation}\label{method:eq:delta}
 C(H)\geq\delta
 :=\frac{3146981978575629437}{10^{24}}>0
 \qquad(H\in\mathcal H).
\end{equation}
Once validity of the rows and \eqref{method:eq:delta} are established, the
contradiction itself is short:
\[
 0\geq\sum_Hp_HC(H)
   \geq\delta\sum_Hp_H
   =\delta>0.
\]
There can therefore be no graph $X\in\R(5,6,84)$.

The stored weights have denominator $10^{12}$. Each row also has
its own exact normalization denominator. To avoid a potentially
large least common multiple, the verifier bounds each summand
downward on a common grid of denominator $10^{24}$. If a summand
is $wa/(10^{12}d)$, where $w$ is the signed integer numerator of
its multiplier, $a$ is the integer row coefficient at the chosen $H$,
and $d>0$ is that row's normalization denominator, it contributes the lower bound
\[
 \frac{1}{10^{24}}
 \left\lfloor\frac{wa\,10^{12}}d\right\rfloor.
\]
This formula is valid for negative summands as well as positive
ones. Integer floor division must be used, rather than truncation
toward zero. Summing the floors gives a lower bound, so a strictly
positive resulting numerator proves \eqref{method:eq:delta} without any
floating-point tolerance.

Taking the minimum of these computed lower bounds over the 979 types
gives the reported numerator. Thus $\delta$ is a common strictly
positive lower bound for all coefficients $C(H)$. The use of integer
arithmetic establishes its positivity exactly.

\clearpage
\section{A practical verification route}\label{method:sec:verify}
A reader can check the local argument and then replay the complete
computation. The two tasks have different conclusions. This section
gives the commands in their execution order; the names of internal
programs below explain what those commands invoke.

\subsection*{Prepare one verification directory}
The accompanying file \path{verification.tar.xz} contains a directory
named \path{verification}. In a terminal whose current directory
contains that archive, run
\begin{verbatim}
tar -xJf verification.tar.xz
cd verification
\end{verbatim}
The commands below are run from this extracted directory. It contains
\path{verify_package.py}, \path{check_local_example.py},
\path{README.txt} and the subdirectories holding the data. If those
files have already been extracted, open a terminal in their
\path{verification} directory instead of extracting another copy.
The complete archive includes all raw catalogue inputs. In the
explicitly labelled compact archive, \path{START_HERE.txt} explains
how to restore the 58 omitted catalogue files with their required
hashes; that restoration must precede the complete replay.

\subsection*{Check the local example}
First read the definitions of $e,t,q,A_v,B_v$, the ten inequalities
in Section~\ref{method:sec:inputs}, and the cancellation in
Section~\ref{method:sec:worked}. The exact paper calculation to check is
\[
\sum_v(L_A(v)+L_B(v))=52250-166e(X).
\]
To check its finite profile substitutions, run
\begin{verbatim}
python3 check_local_example.py --root .
\end{verbatim}
Here the dot denotes the extracted \path{verification} directory,
which is the terminal's current directory. This command uses only
the Python standard library. Its output must contain
\begin{verbatim}
"worked_example_passed": true
"edge_upper_bound": 314
\end{verbatim}
It also prints the exact minima
listed in Section~\ref{method:sec:tables}. A successful run checks those
substitutions, the constant identity, and the correspondence with the
saved equation multipliers. It does not yet verify the proofs of all
input polygon bounds or the final 84-vertex contradiction.
The arithmetic uses exact fractions. Decimal polygon coordinates
in the stored files are recovered as small rationals, with reduced
denominators 1, 2 or 3, and checked against their decimal encodings.
The separate exact polygon audit reconstructs the vertices from
their defining half-planes.

\subsection*{Replay the whole computation}
The tested interpreter is Python 3.13.9. The package pins NumPy,
SciPy and NetworkX versions in its requirements file. With Python
3.13 installed, create an isolated environment and install them:
\begin{verbatim}
python3.13 -m venv .venv
. .venv/bin/activate
python -m pip install -r proof_84/requirements.txt
\end{verbatim}
These are terminal commands for macOS or Linux. The package README
also gives Windows instructions. Installation requires access to a
package index or previously downloaded packages. The verification
commands themselves run without network access. The full extraction
check additionally needs a C++11 compiler and zlib headers and library;
the README gives the platform-specific installation commands.

Once these dependencies are installed, run
\begin{verbatim}
python verify_package.py --full
\end{verbatim}
Run Python normally, without \texttt{-O}, \texttt{-OO}, or
\texttt{PYTHONOPTIMIZE}: some proof checks are assertions. Every
invoked stage must finish successfully, and the final summary must
contain \texttt{all\_passed: true}. If a stage fails or the command
stops before the final summary, the full replay has not succeeded.
The launcher writes reports and identifies the stage that failed.

This command invokes the 18-check suite and all supplementary
checks. Together they verify the following parts of the argument:
\begin{enumerate}
\item The 58 supplied catalogue files produce the claimed distinct
profiles. The supplied C++ extractor is rerun exhaustively; independent
sampled calculations also check profile extraction. Neither operation
proves the external catalogue completeness theorem anew.
\item The recursive polygons contain the intended profile possibilities,
and all required degrees and edge classes are covered. The 2679 local
certificates have the stated exact multiplier sums and residual signs.
\item The 979 allowed seven-vertex types form a complete list, the used
coefficient rows agree with their counting definitions, and the square
rows come from the finite square-counting construction.
\item The saved final multipliers produce a strictly positive
coefficient on every allowed seven-vertex type, with the lower bound
in \eqref{method:eq:delta}.
\end{enumerate}
The principal internal local checker is
\path{replay_required_local_certificates.py}; the two final replay
implementations are \path{replay_global_certificate.py} and
\path{audit_global_exact_certificate.py}. The supplied file index
locates these basenames within the preserved archive structure.

\subsection*{What remains mathematical input and review}
The initial Ramsey bounds and completeness of the cited catalogues
remain external mathematical inputs. In particular, $R(4,6)\leq40$
is recorded in the survey~\cite{method:survey} as a result of Angeltveit and
McKay, attributed there to personal communications. The package does
not supply a new proof of that bound. A reader should also check that
the displayed counting identities apply to the stated families and
that convex weights preserve the expressions used. The companion
specification provides the complete definitions for reconstructing
all remaining row families. Software success confirms the specified
finite arithmetic; the preceding explanations identify why that
arithmetic is relevant to the theorem.

\clearpage
\section{Mathematical review and finite verification}
The proof has a mathematical part and a finite arithmetic part. The
mathematical part establishes that every graph in the specified Ramsey
family yields variables satisfying the stated conditions. This requires
the catalogue completeness results, the graph-to-weight construction,
the counting identities, the treatment of root vertices, and the finite
sampling factors. The arithmetic part checks the required profile cases
and the supplied weighted sums using exact rational or integer
operations. Both parts are needed to infer the theorem from a successful
verification run.

For the worked example, the identities in Sections~\ref{method:sec:second}
and~\ref{method:sec:worked} can be checked on paper. The ten local inequalities
have their coefficients printed explicitly; their validity is checked
on the finite profile sets in Section~\ref{method:sec:tables}. The same method
extends to the complete proof, whose 2679 local certificates and 903
nonzero final weights are supplied in machine-readable files. The
companion mathematical specification defines every row family and gives
the procedures for reconstructing and checking those files.

The file hashes identify the precise inputs used in a verification run.
The mathematical meaning of those inputs comes from the constructions
above, while the exact checkers establish their claimed arithmetic
properties. A reproducible verification therefore records both the input
hashes and the successful outputs of the relevant checks.

The worked local certificate also illustrates a useful simplification:
its 1217-variable representation reduces, after collecting terms and
applying the triangle-incidence identity, to a sum of two nonnegative
expressions per vertex. This explicit reduction connects the stored
coefficients with the graph-counting proof of the 314-edge bound.

\begin{thebibliography}{III.99}
\bibitem[II.1]{method:count}
B.~D.~McKay and S.~P.~Radziszowski,
\emph{Subgraph counting identities and Ramsey numbers},
Journal of Combinatorial Theory, Series B \textbf{69} (1997), 193--209.
\url{https://users.cecs.anu.edu.au/~bdm/papers/r55.pdf}

\bibitem[II.2]{method:r55}
V.~Angeltveit and B.~D.~McKay, \emph{$R(5,5)\leq46$},
Journal of Graph Theory \textbf{112} (2026), 198--208.
\url{https://doi.org/10.1002/jgt.70029};
\url{https://arxiv.org/html/2409.15709v2}

\bibitem[II.3]{method:data}
B.~D.~McKay, \emph{Ramsey Graphs}, complete graph catalogues.
\url{https://users.cecs.anu.edu.au/~bdm/data/ramsey.html}

\bibitem[II.4]{method:survey}
S.~P.~Radziszowski, \emph{Small Ramsey Numbers},
Electronic Journal of Combinatorics, Dynamic Survey DS1,
revision 18, 24 April 2026, Table Ib.
\url{https://www.cs.rit.edu/~spr/ElJC/ejcram18.pdf}
\end{thebibliography}