% Generated from the current standalone source; edit that source.
% Only title/contents wrappers and reference namespaces are changed.
\begin{abstract}
This supplement specifies the finite calculations in the accompanying proof that every graph on $84$ vertices contains a clique of order $5$ or an independent set of order $6$. Assuming a counterexample, we count configurations in the graph and derive equations and inequalities that these counts must satisfy. Explicit rational weights combine these constraints into a contradiction. The weights on inequalities are nonnegative, so adding the weighted inequalities preserves their direction; equations may be multiplied by signed weights. The verification checks these combinations using exact arithmetic. This document defines the quantities being counted, derives the constraints, gives representative calculations, and provides the commands and expected outputs for checking the supplied numerical files. Published Ramsey bounds and the completeness of the cited small-graph catalogues are stated external inputs.
\end{abstract}

\clearpage

\section{Notation and external inputs}\label{specification:sec:notation}
All graphs are finite, undirected, simple graphs. For a graph $X$, write $V(X)$ and $E(X)$ for its vertex and edge sets, $|X|=|V(X)|$ for its order, $N_X(v)=\{u\in V(X):\{u,v\}\in E(X)\}$ for a vertex neighborhood, and $d_X(v)=|N_X(v)|$ for its degree. For $S\subseteq V(X)$, $X[S]$ is the induced subgraph on $S$. The complement $\overline X$ has the same vertices and exactly the missing pairs as edges. The clique number $\omega(X)$ and independence number $\alpha(X)$ are the largest orders of a complete and an edgeless induced subgraph, respectively. Subscripts on $N$ and $d$ may be omitted when the ambient graph is specified.

For positive integers $s,r$ and an integer $n\geq0$, let
\[
\R(s,r,n)=\{X:|X|=n,\ \omega(X)<s,\ \alpha(X)<r\}.
\]
Graphs in this family are considered up to isomorphism whenever they are enumerated. The Ramsey number $R(s,r)$ is the least $n$ for which the family is empty. Define the following graph statistics:
\begin{align*}
e(X)&=|E(X)|,\\
t(X)&=\bigl|\{S\subseteq V(X):|S|=3,\ X[S]\cong K_3\}\bigr|,\\
w(X)&=\sum_{v\in V(X)}\binom{d_X(v)}2,
& q(X)&=w(X)-t(X).
\end{align*}
Thus $w$ counts a center and an unordered pair of its neighbors, including pairs that are adjacent. An induced three-vertex path contributes $1$ to $q$ and a triangle contributes $2$; all other three-vertex induced types contribute zero. The profile of $X$ is the four-tuple $(|X|,e(X),t(X),q(X))$. Induced-copy counts count vertex subsets, not labelled embeddings. Other counts, such as paths that need not be induced, are specified separately.

The symbols $K_m,P_m,C_m$ denote the complete graph, path, and cycle on $m$ vertices; $K_{1,3}$ is the three-leaf star, $+$ denotes disjoint union, and $K_4-e$ means $K_4$ with one edge removed. We use $\1_{\mathcal A}=1$ if a condition $\mathcal A$ holds and $0$ otherwise. Empty sums are zero, empty products are one, and $\binom{S}{k}$ denotes the set of $k$-element subsets of a finite set $S$. For nonnegative integer $m$, $\binom mk=0$ when $k<0$ or $k>m$. For vectors and matrices, superscript $T$ denotes transpose and $M\succeq0$ means $z^TMz\geq0$ for every real vector $z$ of the appropriate dimension. All expectations below are with respect to the explicitly specified uniform finite sample.

The starting Ramsey facts are
\[
R(3,5)=14,\quad R(3,6)=18,\quad R(4,4)=18,
\quad R(4,5)=25,
\]
\[
R(4,6)\leq40,\qquad R(5,5)\leq46.
\]
The last bound is Theorem~1.1 of Angeltveit--McKay~\cite{specification:r55}. The $R(4,6)$ bound is recorded in Radziszowski's survey~\cite[Table~Ib]{specification:survey}, which attributes it to Angeltveit and McKay with personal communications from 2020 and 2024. The survey is the source used here for that bound.

A \emph{complete catalogue} for a graph family is a finite list containing a representative of every isomorphism class in that family. Relabelling a graph does not change the counts $e,t,q$, so one representative per class is sufficient for these calculations. The catalogues used here are Brendan McKay's published collections~\cite{specification:data} for the following small families:
\begin{center}
\begin{tabular}{ll}
Family&Which graphs the supplied files cover\\\hline
$\R(3,5,n)$&Supplied orders up to $13$\\
$\R(3,6,n)$&Every order $13,14,15,16,17$\\
$\R(4,4,n)$&Every order from $5$ through $17$\\
$\R(4,5,24)$&All $352366$ isomorphism classes\\
$\R(4,5,n)$, $19\leq n\leq23$&The fixed-edge classes listed below
\end{tabular}
\end{center}
For example, $\R(3,6,17)$ means triangle-free graphs on $17$ vertices with no independent set of six vertices; its catalogue contains seven graphs. The complete extreme-edge classes have the following integer edge counts:
\begin{center}
\begin{tabular}{c|l}
Order $n$&Edge counts with complete supplied catalogues\\\hline
19&57, 58, 90, 91, 92\\
20&68, 69, 98, 99, 100\\
21&77, 78, 106, 107\\
22&88, 89, 113, 114\\
23&101, 102, 103, 104, 119, 120, 121, 122
\end{tabular}
\end{center}
Each entry is a complete catalogue only for its stated order and edge count. For instance, \file{r4523.101.g6} contains the $(4,5)$-graphs on $23$ vertices with exactly $101$ edges. The $26$ classes in the table are precisely the catalogue cases used in the recursive polygon construction.

For the $(4,6)$ families on $38$ or $39$ vertices, the $(5,5)$ families on $44$ or $45$ vertices, and the hypothetical $(5,6)$ family on $84$ vertices, the proof uses counting equations and information about smaller graphs. These larger families are treated through numerical constraints satisfied by every member, without enumerating their graphs. Where a complete catalogue is unavailable, we use a proved containing region for the possible profiles, defined in Section~\ref{specification:sec:local-variables}.

Catalogue completeness is an external mathematical input from the cited source. The supplied programs check that the archived records and derived profiles agree, and that the record counts match the catalogue descriptions. The completeness assumption concerns the catalogue enumeration itself. A further established input, used for lower-order $(3,6)$ outer profiles, is the small-order edge formula in \cite[Theorem~2]{specification:trianglefree}; its specialization is stated in Section~\ref{specification:sec:small-order}.

The edge intervals used for $\R(4,5,n)$ are
\begin{center}
\begin{tabular}{c|rrrrrr}
$n$&19&20&21&22&23&24\\\hline
$e_{\min}$&57&68&77&88&101&116\\
$e_{\max}$&92&100&107&114&122&132
\end{tabular}
\end{center}
These lower and upper edge bounds are recorded in \cite[Appendix~A, Table~1]{specification:r55}. They describe intervals containing every possible edge count. For orders $19$ through $23$, the $26$ listed catalogue classes are treated directly and every other integer edge count in these intervals receives a containing polygon justified by further counting arguments. This supplies profile information for every edge class in the intervals.

\subsection{Complement profiles}
For a graph of order $n$, the exact complement transformation is
\begin{align}
e(\overline X)&=\binom n2-e(X),\label{specification:eq:comp1}\\
t(\overline X)&=\binom n3-(n-2)e(X)+q(X),\label{specification:eq:comp2}\\
q(\overline X)&=2\binom n3-(n-2)e(X)+t(X).\label{specification:eq:comp3}
\end{align}
This permits a supplied catalogue to serve both $\R(s,r,n)$ and $\R(r,s,n)$. The transformation is affine in the profile coordinates; it therefore commutes with taking convex combinations.

\section{Proof structure and verification}
The theorem asserts that $\R(5,6,84)$ is empty. A hypothetical member would have $84$ vertices, no five pairwise adjacent vertices, and no six pairwise nonadjacent vertices. The proof proceeds by assigning numerical counts to such a graph and showing that those counts would satisfy contradictory inequalities.

A \emph{counting model} in this document is a list of numerical variables and equations or inequalities that every graph in a stated family must satisfy. For example, the number of vertices of each degree is nonnegative, and the sum of those numbers is the order of the graph. A \emph{relaxation} allows real values for its variables and imposes only the listed conditions. It may therefore allow numerical assignments that no graph can realize. Infeasibility of these weaker conditions therefore implies that the graph family is empty.

A \emph{certificate} is a supplied list of rational coefficients for combining already justified equations and inequalities. Their weighted sum gives the required bound or contradiction. Verification consists of checking the supplied coefficients by exact addition, multiplication, and comparison. Section~\ref{specification:sec:duals} first explains this weighted-sum argument without matrix notation and then specifies its matrix representation.

The proof has two main counting models. The first is applied to graphs on $19$--$23$, $38$, $39$, $44$, or $45$ vertices to establish local bounds. Its variables describe neighborhoods, nonneighborhoods, and four-vertex subsets. The second is applied to the hypothetical $84$-vertex graph. Its variables are the proportions of seven-vertex subsets inducing each of the $979$ allowed types. The local bounds supply some of the inequalities for that second model. A final weighted sum rules out every possible vector of those proportions.

\subsection{A route through the mathematics and the programs}
For mathematical review, first check the definitions and the triple count in the next section. Then follow the construction of the local variables and the equations they satisfy: this establishes that every graph gives an allowed numerical assignment. Next check the weighted-sum principle and the representative local calculation. The remaining sections derive the seven-vertex averages, the squared expressions, and the final contradiction. The separate \emph{Explanation of the method} gives a longer worked derivation of one local bound, $e(X)\leq314$ for $X\in\R(4,6,38)$.

For computational reproduction, use the commands in Section~\ref{specification:sec:execution}. They check the supplied numerical coefficients and their links to the counting formulas. The default command runs the main certificate checks; the full command also re-extracts profiles from every raw catalogue record. The output is evidence that the submitted data satisfy the specified finite arithmetic tests. The mathematical review establishes why those tests imply statements about graphs. Both parts are needed.

A reader writing another verifier can use the displayed equations as the specification and the saved coefficients as input. In that case the essential comparisons are equality of rational numbers and completeness of the required cases. The stored ordering of variables and rows specifies how positions in the numerical arrays correspond to the definitions. A different ordering is valid if every dependent coefficient is permuted consistently.

\subsection{Locating the files}
The complete electronic verification archive is named \file{verification.tar.xz}. Extracting it creates a folder named \file{verification}, which contains \file{README.txt}, \file{verify_package.py}, and the subfolders used by the programs. The file \file{FILE_INDEX.tsv} maps each basename cited here to its location within that extracted folder. This document cites files by basename; the execution recipes give the required relative paths.

A JSON certificate is a text file containing labelled fields, such as a list of rational multipliers. A saved audit report records the outcome of a previous program run. The certificate is input to the verifier; the report records the checks performed and their outcomes.

\section{The first counting reduction}
Suppose $X\in\R(5,6,84)$. For each vertex $v$, set
\[
A_v=X[N(v)],\quad B_v=X[V(X)\setminus(N(v)\cup\{v\})],
\quad d_v=d_X(v).
\]
A four-clique in $A_v$, together with $v$, would be a forbidden five-clique in $X$. An independent six-set in $A_v$ would already be forbidden in $X$. Thus $A_v\in\R(4,6,d_v)$. Similarly, $B_v$ has no five-clique, and an independent five-set in $B_v$ would extend with $v$ to an independent six-set; hence $B_v\in\R(5,5,83-d_v)$. The bounds $R(4,6)\leq40$ and $R(5,5)\leq46$ give $d_v\leq39$ and $83-d_v\leq45$, respectively. Therefore
\begin{equation}\label{specification:eq:degrees}
d_v\in\{38,39\}.
\end{equation}
If $x$ vertices have degree $39$, handshaking gives $2e(X)=3192+x$. In particular $x$ is even. The local cases are
\begin{center}
\begin{tabular}{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{tabular}
\end{center}
The next identity holds for any graph $X$ of order $n$. In this general identity, $A_v=X[N_X(v)]$, $B_v=X[V(X)\setminus(N_X(v)\cup\{v\})]$, and $d_v=d_X(v)$. Double counting yields
\begin{equation}\label{specification:eq:triple}
\sum_v\left[e(B_v)-e(A_v)-d_v\left(\frac n2-d_v\right)\right]=0.
\end{equation}
To prove it, first count a triangle together with one of its vertices. The other two vertices form an edge in the chosen vertex's neighborhood, and each triangle is counted three times. Hence $\sum_v e(A_v)=3t(X)$. For an edge $uw$, the number of vertices adjacent to neither endpoint is
\[
n-d_u-d_w+|N(u)\cap N(w)|.
\]
Summing this expression over all edges counts each edge of each $B_v$ exactly once. The sum of $d_u+d_w$ over all edges $uw$ is $\sum_vd_v^2$, because each vertex occurs as an endpoint of $d_v$ edges. The common-neighbor terms count each triangle three times. Therefore
\[
\sum_v e(B_v)=ne(X)-\sum_vd_v^2+3t(X).
\]
Subtracting the neighborhood sum and using $\sum_vd_v=2e(X)$ proves \eqref{specification:eq:triple}. This is the $m=2$ instance of the general counting identity in~\cite{specification:count}, also stated in~\cite{specification:r55}.

For $n=84$, the contribution is $d_v(42-d_v)$: it equals $152$ at degree $38$ and $117$ at degree $39$. These constants will combine with local edge bounds. The identity alone does not distinguish all possible local profiles, so the proof retains additional counts of triangles and wedges.

\section{Variables of the local profile model}\label{specification:sec:local-variables}
Fix a family $\R(s,r,n)$ and take $X$ to be an arbitrary member. The construction in this section applies to each local family needed in the proof, including $(4,6,38)$ and $(5,5,45)$.

The local model records neighborhood profiles using containing polygons in the $(t,q)$-coordinates. The vertices of these polygons provide a finite set of coordinates for the model. A possible neighborhood profile can be a convex combination of several polygon vertices; its contribution is therefore split among them. The resulting variables are nonnegative weights, not necessarily integers. The construction below states exactly what the polygons contain, what labels the variables, and how every actual graph supplies values for them.

\subsection{Actual profile sets and their outer polygons}
For a family $\R(s,r,m)$ and an integer $0\leq\eta\leq\binom m2$, define the finite set
\begin{equation}\label{specification:eq:actual-profile-set}
\mathcal S_{s,r,m,\eta}
=\{(t(Y),q(Y)):Y\in\R(s,r,m),\ e(Y)=\eta\}
\subseteq\mathbb Z_{\geq0}^2.
\end{equation}
The coordinate $\eta$ is held fixed in this definition. In particular, profiles with different edge counts are not combined in a single polygon.

For each required parameter tuple, the input supplies a bounded rational convex polygon $\mathcal P_{s,r,m,\eta}\subseteq\mathbb R^2$ with
\begin{equation}\label{specification:eq:outer-inclusion}
\mathcal S_{s,r,m,\eta}\subseteq\mathcal P_{s,r,m,\eta}.
\end{equation}
Here ``polygon'' includes a line segment or a single point. An empty polygon is permitted only for a class independently justified to contain no graphs. Write
\[
\mathcal V_{s,r,m,\eta}=\operatorname{vert}(\mathcal P_{s,r,m,\eta}),
\qquad \mathcal P_{s,r,m,\eta}=\operatorname{conv}(\mathcal V_{s,r,m,\eta}).
\]
The finite set $\operatorname{vert}(P)$ consists of the extreme points of $P$. A convex combination of points $v_1,\ldots,v_k$ is a sum $\theta_1v_1+\cdots+\theta_kv_k$ with $\theta_i\geq0$ and $\sum_i\theta_i=1$; the set $\operatorname{conv}(V)$ consists of all such combinations of points in $V$. We set $\operatorname{conv}(\varnothing)=\varnothing$. All elements of $\mathcal V$ have rational coordinates, denoted $(\tau,\kappa)$; these are candidate triangle and $q$ coordinates, respectively.

There are two constructions of $\mathcal P$. If a complete catalogue is available for the edge class, take the convex hull of its extracted $(t,q)$ pairs. In that case $\mathcal P=\operatorname{conv}(\mathcal S)$. Otherwise take the intersection of finitely many certified half-planes
\[
L_\ell\leq\alpha_\ell\tau+\beta_\ell\kappa\leq U_\ell
\qquad(\ell=1,\ldots,m_0),
\]
where $m_0$ is the number of support directions and all displayed coefficients are rational. Each support is proved for the fixed family, order, and edge count. Section~\ref{specification:sec:polygons} specifies the recursive instances, directions, and files. An extreme point of such an outer polygon need not be the profile of any graph. Inclusion~\eqref{specification:eq:outer-inclusion} ensures that every graph profile has a convex representation using the polygon vertices.

\subsection{The finite coordinate sets}
Fix the ambient local family $\R(s,r,n)$, with $s,r\geq2$. Let $\mathcal D\subseteq\{0,\ldots,n-1\}$ be the supplied set of admissible degrees, meaning that every vertex degree of every graph in this family lies in $\mathcal D$. Write $\mathcal D^B=\{n-1-d:d\in\mathcal D\}$. For every $d\in\mathcal D$, a neighborhood belongs to $\R(s-1,r,d)$ and a nonneighborhood belongs to $\R(s,r-1,n-1-d)$. Define
\begin{align}
\mathcal I_A=\bigl\{(d,\eta,\tau,\kappa):{}&d\in\mathcal D,\quad
\eta\in\mathbb Z,\quad 0\leq\eta\leq\tbinom d2,\notag\\
& (\tau,\kappa)\in\mathcal V_{s-1,r,d,\eta}\bigr\},\label{specification:eq:IA}\\
\mathcal I_B=\bigl\{(h,\eta,\tau,\kappa):{}&h\in\mathcal D^B,\quad
\eta\in\mathbb Z,\quad 0\leq\eta\leq\tbinom h2,\notag\\
& (\tau,\kappa)\in\mathcal V_{s,r-1,h,\eta}\bigr\}.\label{specification:eq:IB}
\end{align}
The four subscripts therefore have separate roles: local order, exact local edge count, polygon triangle coordinate, and polygon $q$ coordinate. Empty vertex sets supply no coordinates. Each edge class must have either a justified covering polygon or a proof of emptiness. The full degree ranges and edge-class coverage are checked in Section~\ref{specification:sec:polygons}.

The profile variables of the linear program are one independent real variable for each element of these finite sets:
\[
a_{d,\eta,\tau,\kappa}\geq0\quad((d,\eta,\tau,\kappa)\in\mathcal I_A),
\qquad
b_{h,\eta,\tau,\kappa}\geq0\quad((h,\eta,\tau,\kappa)\in\mathcal I_B).
\]
The variable $a_{d,\eta,\tau,\kappa}$ is the total weight assigned to the specified neighborhood profile vertex, and $b_{h,\eta,\tau,\kappa}$ is the analogous nonneighborhood weight. The following construction gives this statement a precise meaning for an actual graph.

\subsection{From a graph to nonnegative weights}
Let $X\in\R(s,r,n)$, and for $v\in V(X)$ put
\[
d_v=d_X(v),\quad h_v=n-1-d_v,\quad
A_v=X[N_X(v)],\quad B_v=X[V(X)\setminus(N_X(v)\cup\{v\})],
\]
\[
\eta_v^A=e(A_v),\qquad \eta_v^B=e(B_v).
\]
By~\eqref{specification:eq:outer-inclusion}, choose nonnegative numbers
$\lambda^A_{v,\tau,\kappa}$, indexed by
$(\tau,\kappa)\in\mathcal V_{s-1,r,d_v,\eta_v^A}$, such that
\begin{equation}\label{specification:eq:local-barycentric}
\sum_{\tau,\kappa}\lambda^A_{v,\tau,\kappa}=1,
\qquad
\sum_{\tau,\kappa}\lambda^A_{v,\tau,\kappa}(\tau,\kappa)
=(t(A_v),q(A_v)).
\end{equation}
Choose $\lambda^B_{v,\tau,\kappa}$ in the same way using
$\mathcal V_{s,r-1,h_v,\eta_v^B}$ and $(t(B_v),q(B_v))$.
All sums in~\eqref{specification:eq:local-barycentric} run over the displayed vertex set. Extend each $\lambda$ by zero outside that set. Now define
\begin{align}
a_{d,\eta,\tau,\kappa}
&=\sum_{\substack{v\in V(X):\ d_v=d\\ \eta_v^A=\eta}}
\lambda^A_{v,\tau,\kappa},\label{specification:eq:aggregate-A}\\
b_{h,\eta,\tau,\kappa}
&=\sum_{\substack{v\in V(X):\ h_v=h\\ \eta_v^B=\eta}}
\lambda^B_{v,\tau,\kappa}.\label{specification:eq:aggregate-B}
\end{align}
These formulas also define zero values when there are no vertices in the indicated degree and edge class. A graph need not determine unique weights: convex representations can be nonunique. The required counting identities hold for every such choice.

Define the degree-class masses
\[
m_d^A=\sum_{\substack{(d',\eta,\tau,\kappa)\in\mathcal I_A\\d'=d}}
a_{d',\eta,\tau,\kappa},\qquad
m_h^B=\sum_{\substack{(h',\eta,\tau,\kappa)\in\mathcal I_B\\h'=h}}
b_{h',\eta,\tau,\kappa}.
\]
For the graph-derived weights they equal $|\{v:d_v=d\}|$ and
$|\{v:h_v=h\}|$. Consequently the relaxation includes
\begin{equation}\label{specification:eq:match}
\sum_{d\in\mathcal D}m_d^A=n,\qquad
m_d^A=m_{n-1-d}^B\quad(d\in\mathcal D).
\end{equation}
Arbitrary feasible weights of the relaxation, including these masses, are allowed to be fractional. Integrality is used only for statistics known to come from a graph, never assumed for the profile weights themselves.

\begin{lemma}[Preservation of local affine counts]\label{specification:lem:affine}
Let $F$ be a real-valued function on the index set whose dependence on $(\tau,\kappa)$, for each fixed $(d,\eta)$, extends to an affine function on $\mathbb R^2$. The graph-derived weights satisfy
\[
\sum_{(d,\eta,\tau,\kappa)\in\mathcal I_A}
 F(d,\eta,\tau,\kappa)a_{d,\eta,\tau,\kappa}
=\sum_{v\in V(X)} F(d_v,\eta_v^A,t(A_v),q(A_v)).
\]
The analogous identity holds on the $B$ side with $h_v$ and $\eta_v^B$.
\end{lemma}
\begin{proof}
Substitute~\eqref{specification:eq:aggregate-A}, interchange the finite sums, and apply~\eqref{specification:eq:local-barycentric} separately for each vertex. The constant term is preserved because its weights sum to one; the two linear terms are preserved by the coordinate equation. The order and edge count stay fixed throughout each convex combination.
\end{proof}

\subsection{A catalogue example of fractional weights}
The supplied file \file{r36_13.g6.gz.profiles} has, at edge count $16$, exactly the pairs
\[
\mathcal S_{3,6,13,16}=\{(0,25),(0,26),(0,28)\}.
\]
Its polygon is the segment with extreme points $(0,25)$ and $(0,28)$. The middle catalogue profile is represented by
\[
(0,26)=\frac23(0,25)+\frac13(0,28).
\]
If a vertex of an ambient $(4,6)$-graph has this neighborhood profile, that single vertex contributes $2/3$ to $a_{13,16,0,25}$ and $1/3$ to $a_{13,16,0,28}$. Its total contribution to mass is $1$, to local edges is $16$, to local triangles is $0$, and to local $q$ is $26$. There is no coordinate $a_{13,16,0,26}$ in the extreme-point model. The fractions are the coefficients representing this single catalogue profile as a convex combination of polygon vertices. The construction applies whenever such a neighborhood occurs.

\subsection{Ambient statistics as linear functionals}
For any profile weight vector $a$, define
\begin{align}
\mathcal E(a)&=\frac12\sum_{\mathcal I_A}d\,a_{d,\eta,\tau,\kappa},\label{specification:eq:ec}\\
\mathcal T(a)&=\frac13\sum_{\mathcal I_A}\eta\,a_{d,\eta,\tau,\kappa},\label{specification:eq:tc}\\
\mathcal W(a)&=\sum_{\mathcal I_A}\binom d2 a_{d,\eta,\tau,\kappa},\label{specification:eq:wc}\\
\mathcal Q(a)&=\mathcal W(a)-\mathcal T(a).
\end{align}
Here $\sum_{\mathcal I_A}$ means a sum over every four-tuple in~\eqref{specification:eq:IA}. For weights constructed from $X$, these functionals equal $e(X),t(X),w(X),q(X)$, respectively. Handshaking proves the first identity; each triangle contributes one edge to each of its three neighborhoods, proving the second; the degree-class masses prove the third. These functionals are defined even at a relaxed point that corresponds to no graph.

The implementation names their coefficient vectors \texttt{ec}, \texttt{tc}, \texttt{wc}, and \texttt{qc}. The metadata key \texttt{model.t} denotes the independence parameter $r$; the vector \texttt{tc} and profile coordinate \texttt{tr} denote triangles. If the ambient edge count is fixed at the integer $e_0$, add $\mathcal E(a)=e_0$. The neighborhood edge counts $\eta$ still range over their allowed values.

\section{Four-vertex variables and bulk equations}
Let $\mathcal F_4$ contain one representative of each of the eleven isomorphism classes of graphs on four vertices. Introduce a real variable $z_F\geq0$ for every $F\in\mathcal F_4$. The value assigned by an actual graph $X$ is
\[
z_F(X)=\bigl|\{S\in\tbinom{V(X)}4:X[S]\cong F\}\bigr|.
\]
An arbitrary relaxed $z_F$ need not be an integer. Define $u(F)=|\{v\in V(F):d_F(v)=3\}|$ and $i(F)=|\{v\in V(F):d_F(v)=0\}|$, the numbers of universal and isolated vertices. The remaining entries in the following table are $e(F),t(F),w(F)$ as defined in Section~\ref{specification:sec:notation}. Every sum over $F$ in the local model ranges over $\mathcal F_4$.
\begin{center}
\begin{tabular}{lrrrrr}
\toprule
$F$&$e$&$t$&$w$&$u$&$i$\\\midrule
$4K_1$&0&0&0&0&4\\
$K_2+2K_1$&1&0&0&0&2\\
$2K_2$&2&0&0&0&0\\
$P_3+K_1$&2&0&1&0&1\\
$K_3+K_1$&3&1&3&0&1\\
$K_{1,3}$&3&0&3&1&0\\
$P_4$&3&0&2&0&0\\
$C_4$&4&0&4&0&0\\
Paw&4&1&5&1&0\\
$K_4-e$&5&2&8&2&0\\
$K_4$&6&4&12&4&0\\\bottomrule
\end{tabular}
\end{center}
The paw is a triangle with a pendant vertex. The code uses the NetworkX graph-atlas ordering; another ordering is acceptable if every corresponding column and objective is permuted consistently.

These variables connect local information at different vertices: the same four-set may be seen from several roots, but must receive one consistent induced type. The following four equations count all four-sets and the edges, triangles, or wedges contained in them:
\begin{align}
\sum_Fz_F&=\binom n4,\\
\sum_Fe(F)z_F&=\binom{n-2}{2}\mathcal E(a),\\
\sum_Ft(F)z_F&=(n-3)\mathcal T(a),\\
\sum_Fw(F)z_F&=(n-3)\mathcal W(a).
\end{align}
An edge lies in $\binom{n-2}{2}$ four-sets; a triangle or wedge occupies three vertices and lies in $n-3$ four-sets. The counted edge, triangle, or wedge need not be induced within the four-set.

Some four-vertex counts are known to be zero before any numerical calculation. If $s\leq4$, a graph in $\R(s,r,n)$ cannot contain a $K_4$, so $z_{K_4}=0$. If $r\leq4$, it cannot contain an independent four-set, so $z_{4K_1}=0$. These are the coordinates called \emph{fixed to zero} in the certificate description. For example, the model for $\R(4,6,38)$ has $z_{K_4}=0$ because a four-clique is forbidden. Thus the family definition determines these zero coordinates. All other retained coordinates are constrained to be nonnegative. Their role in the weighted-sum check is explained in Section~\ref{specification:sec:duals}.

\section{Triple types and rooted incidence equations}
For an integer order $m$ and coordinates $(\eta,\tau,\kappa)$, define the four-component polynomial vector
\begin{align}\label{specification:eq:T}
T(m,\eta,\tau,\kappa)=\bigl(&\tbinom m3-(m-2)\eta+\kappa,\notag\\
&(m-2)\eta-2\kappa+\tau,\ \kappa-2\tau,\ \tau\bigr).
\end{align}
Write $T_k$ for its component indexed by $k\in\{0,1,2,3\}$ in the displayed order. When $(m,\eta,\tau,\kappa)$ is a graph profile, $T_k$ is the number of its induced three-sets with exactly $k$ edges. Indeed, these counts sum to $\binom m3$, their edge incidence sum is $(m-2)\eta$, and $T_2+3T_3=w=\kappa+\tau$, while $T_3=\tau$. These relations give~\eqref{specification:eq:T}. The polynomial also defines the coefficients at rational polygon vertices.

For $k\in\{0,1,2,3\}$ and $F\in\mathcal F_4$, let $U_k(F)$ count degree-$3$ vertices of $F$ whose deletion leaves $k$ edges, and let $Z_k(F)$ count degree-$0$ vertices with that property. The rooted incidence rows are
\begin{align}
\sum_{\mathcal I_A}T_k(d,\eta,\tau,\kappa)a_{d,\eta,\tau,\kappa}
 &=\sum_F U_k(F)z_F,\label{specification:eq:U}\\
\sum_{\mathcal I_B}T_k(h,\eta,\tau,\kappa)b_{h,\eta,\tau,\kappa}
 &=\sum_F Z_k(F)z_F.\label{specification:eq:Z}
\end{align}
These eight equations count a triple together with a universal or isolated fourth vertex. To obtain their coefficients, observe that removing a universal vertex deletes exactly three edges, whereas removing an isolated vertex deletes none. Therefore
\[
U_k(F)=u(F)\1_{e(F)-3=k},\qquad
Z_k(F)=i(F)\1_{e(F)=k}.
\]
For example, removing the universal vertex of a paw leaves one edge, so it contributes to $U_1$. The isolated vertex of $K_3+K_1$ contributes to $Z_3$.

The local model also includes the separate triple identity~\eqref{specification:eq:triple}, in the explicit linear form
\begin{equation}\label{specification:eq:triple-model}
\sum_{\mathcal I_B}\eta\,b_{h,\eta,\tau,\kappa}
-\sum_{\mathcal I_A}\left[\eta+d\left(\frac n2-d\right)\right]a_{d,\eta,\tau,\kappa}=0.
\end{equation}
This identity is included as its own row in the model. Lemma~\ref{specification:lem:affine} proves that the graph-derived weights preserve every local count in these equations.

The rooted equations require the neighborhood and nonneighborhood triple patterns to fit into a common four-vertex distribution. They express compatibility between local counts at different vertices.

\section{Joint degrees, disjoint edges, and paths}
The smaller model called version 3 contains profile matching, the optional fixed-edge row, the triple identity, four bulk identities, and eight rooted identities. Version 4 additionally uses the constraints in this section.

When $e(X)=e_0$ is fixed, count pairs of disjoint edges:
\begin{equation}\label{specification:eq:disjoint}
\mathcal W(a)+\sum_F\left(\binom{e(F)}2-w(F)\right)z_F=\binom{e_0}{2}.
\end{equation}
With $e_0$ fixed, the right-hand side is constant and this is a linear equation in the model variables. It is included only in models with a prescribed edge count.

For each $d,f\in\mathcal D$ with $d\leq f$, introduce a real variable $j_{d,f}\geq0$. At the point assigned by a graph, $j_{d,f}$ counts unordered edges whose endpoint degrees, in increasing order, are $(d,f)$. In particular, $j_{d,d}$ counts each edge within a degree class once. Count the ends of edges incident with vertices of degree $d$. The left-hand side below counts $d$ ends per vertex in that degree class; the right-hand side groups the same ends according to the degree of the other endpoint. This gives, for every $d\in\mathcal D$,
\begin{equation}\label{specification:eq:stubs}
d m_d^A=2j_{d,d}+\sum_{\substack{f\in\mathcal D\\f<d}}j_{f,d}+\sum_{\substack{f\in\mathcal D\\f>d}}j_{d,f}.
\end{equation}
The diagonal factor is $2$ because each edge within a class has two ends in that class.

Let $p(Y)$ count unoriented paths with three edges and four distinct vertices in a graph $Y$, with additional edges permitted among their vertices. Equivalently, it is half the number of ordered injective four-tuples $(v_1,v_2,v_3,v_4)$ with all three consecutive pairs adjacent. The path row is
\begin{equation}\label{specification:eq:path}
\sum_Fp(F)z_F=\sum_{\substack{d,f\in\mathcal D\\d\leq f}}(d-1)(f-1)j_{d,f}-3\mathcal T(a).
\end{equation}
Choose the middle edge $uv$. There are $(d_u-1)(d_v-1)$ choices of outer endpoints before requiring them to be distinct. Each common neighbor gives one invalid coincidence, and these total $3t(X)$ over all edges. On a graph-derived point the left-hand side is $p(X)$, and the coefficients can be computed from
\[
p(F)=\sum_{uv\in E(F)}(d_F(u)-1)(d_F(v)-1)-3t(F).
\]
This provides another linear equation.

Put $D_0=|\mathcal D|$ and let $F_0=1$ when the ambient edge count is fixed, and $F_0=0$ otherwise. Version 3 has $D_0+14+F_0$ rows and version 4 has $2D_0+15+2F_0$. The closure auditor checks these row counts and verifies that the version 3 matrix contains precisely its specified variables and equations.

\begin{proposition}[Every graph gives a feasible local point]\label{specification:prop:embedding}
Suppose the admissible degree and profile coverage conditions above hold. Every $X\in\R(s,r,n)$ gives a feasible point of version 3 and version 4, and of their fixed-edge variants when $e(X)=e_0$.
\end{proposition}
\begin{proof}
Choose the weights by~\eqref{specification:eq:local-barycentric}--\eqref{specification:eq:aggregate-B}; take $z_F=z_F(X)$ and the actual joint-degree edge counts $j_{d,f}$. Nonnegativity and degree matching follow from the definitions. The bulk equations count subsets containing a fixed edge, triangle, or wedge. Lemma~\ref{specification:lem:affine} converts the rooted incidence counts and~\eqref{specification:eq:triple} into~\eqref{specification:eq:U}--\eqref{specification:eq:triple-model}. Stub matching counts ends of edges. The disjoint-edge equation partitions edge pairs into those meeting at a vertex and those on four vertices, and the path equation follows from its middle-edge count. Forbidden four-vertex variables vanish. Finally $\mathcal E(a)=e(X)$, so the optional fixed-edge row also holds. The model imposes necessary conditions for membership in the graph family.
\end{proof}

\section{Checking a bound by a weighted sum}\label{specification:sec:duals}
The variables of the local model are the neighborhood weights $a_{d,\eta,\tau,\kappa}$, nonneighborhood weights $b_{h,\eta,\tau,\kappa}$, four-vertex counts $z_F$, and, in version 4, edge counts $j_{d,f}$ by endpoint degree. Every actual graph supplies nonnegative values satisfying the equations, as Proposition~\ref{specification:prop:embedding} proves. A certificate combines these equations to bound an edge or triangle count.

\subsection{The principle before matrix notation}
Suppose, as a small algebraic example, that nonnegative real numbers $u_1,u_2,u_3$ satisfy
\[
u_1+u_2=5,\qquad u_2+u_3=4.
\]
Multiply the first equation by $2$ and the second by $1$, and add:
\[
2u_1+3u_2+u_3=14.
\]
The quantity $3u_1+3u_2+u_3$ is therefore at least $14$, since
\[
3u_1+3u_2+u_3=14+u_1\geq14.
\]
The pair of multipliers $(2,1)$ is a certificate for the bound. Verification consists of adding the two weighted equations and checking that the remaining coefficient is nonnegative.

The Ramsey certificates use exactly this argument with more variables and equations. For example, $e(X)$ is the linear expression $\mathcal E(a)$ defined above, and an upper bound on it is obtained by proving a lower bound on $-\mathcal E(a)$. A claimed upper bound is thus ultimately an identity expressing $-\mathcal E(a)$ as a constant plus a nonnegative combination of the model variables. The certificate supplies the equation multipliers needed to obtain that identity.

\subsection{How the equations become a matrix}
Choose the saved ordering of the variables and place their values in a column vector $\mathbf u$. Let $N_{\rm var}$ be its length and $m_{\rm eq}$ the number of equations. In each equation move all variable terms to the left and leave the constant on the right. Define $M_{\ell j}$ to be the coefficient of the $j$th variable in the $\ell$th equation, and $\mathbf b_\ell$ to be that equation's right-hand side. Thus
\[
M\in\mathbb Q^{m_{\rm eq}\times N_{\rm var}},\qquad
\mathbf b\in\mathbb Q^{m_{\rm eq}},\qquad
M\mathbf u=\mathbf b,\qquad \mathbf u\geq0.
\]
The matrix records the coefficients of the counting equations. For instance, the mass equation has coefficient $1$ at every neighborhood-weight coordinate, coefficient $0$ at all other coordinates, and right-hand side $n$. The entries of $\mathbf b$ are constants; the nonneighborhood weights are among the coordinates of $\mathbf u$.

Let $\mathbf c\in\mathbb Q^{N_{\rm var}}$ record the coefficients of the quantity to be bounded; this quantity is $\mathbf c^T\mathbf u$. It is called the \emph{objective}. For an edge lower bound its coefficients are those of $\mathcal E(a)$: $d/2$ at the neighborhood coordinate $(d,\eta,\tau,\kappa)$ and zero at the other coordinates. For an edge upper bound the signs of those coefficients are reversed. A triangle objective uses $\eta/3$ instead.

Now let $\mathbf y\in\mathbb Q^{m_{\rm eq}}$ give one multiplier per equation. Multiplying the $\ell$th equation by $\mathbf y_\ell$ and summing gives
\[
\sum_{j=1}^{N_{\rm var}}\left(\sum_{\ell=1}^{m_{\rm eq}}
 M_{\ell j}\mathbf y_\ell\right)\mathbf u_j
=\sum_{\ell=1}^{m_{\rm eq}}\mathbf y_\ell\mathbf b_\ell.
\]
The inner sum is the $j$th coordinate of $M^T\mathbf y$. It is the sum of the contributions to one variable from all the weighted equations.

\subsection{What signs must be checked}
Let $J_0$ be the set of variable positions occupied by counts already known to be zero, such as $z_{K_4}$ in a $K_4$-free family. Let $J_+$ be the other positions. The certificate is valid if
\[
\mathbf c_j-(M^T\mathbf y)_j\geq0\qquad(j\in J_+).
\]
Subtracting the weighted equation sum from the objective proves the explicit identity
\begin{equation}\label{specification:eq:duality}
\mathbf c^T\mathbf u-\mathbf y^T\mathbf b
=\sum_{j\in J_+}
 \left(\mathbf c_j-(M^T\mathbf y)_j\right)\mathbf u_j\geq0.
\end{equation}
Every term on the right is nonnegative. A coordinate in $J_0$ contributes zero regardless of its coefficient, so it is omitted from this sign comparison. The equation multipliers may be negative because they multiply equalities. By contrast, the coefficients remaining on the nonnegative variables must have the displayed sign.

The multiplier vector $\mathbf y$ is called a \emph{dual certificate}. Its validity follows directly from~\eqref{specification:eq:duality}. Verification has two parts: proving that the rows of $M$ are valid counting equations, and checking that the supplied $\mathbf y$ gives nonnegative residual coefficients.

\subsection{Matching the displayed equations to the stored rows}
The mathematical triple identity is equation~\eqref{specification:eq:triple-model}. For integer coefficient storage, the implementation records twice that row. It also records twice the fixed-edge equation, twice the four-set edge-incidence equation, and three times the four-set triangle-incidence equation; the other displayed rows retain their stated scale. Multiplying an equation by a nonzero constant leaves its solutions unchanged, but changes the multiplier needed in a certificate. Accordingly, the verifier uses the stored row scales and the stored multipliers together. To use the displayed equations, multiply each stored certificate multiplier by the corresponding row's storage factor.

For example, the mathematical fixed-edge equation is $\mathcal E(a)=e_0$. Its stored version has coefficient $d$ at each neighborhood variable and right-hand side $2e_0$. The worked-method document shows the analogous conversion explicitly for the triple row in the $314$-edge example.

\subsection{Files, exact arithmetic, and the check to perform}
A local JSON certificate records the family parameters, the objective coefficients, the equation multipliers, the rounding threshold, and the exact resulting lower bound. Rational entries are strings such as \texttt{"3/7"}, with numerator and denominator separated by a slash. The fields named \texttt{objective} and \texttt{dual} contain $\mathbf c$ and $\mathbf y$, respectively. The model parameters tell the verifier which profile sets and counting equations to reconstruct.

The verifier first reconstructs the objective from the mathematical claim and compares it with the stored objective. It then calculates every residual coefficient in~\eqref{specification:eq:duality}, checks its sign, and computes $\mathbf y^T\mathbf b$. Finally it checks that this rational bound is strong enough for the stated integer conclusion. The saved field \texttt{max\_dual\_violation} records a diagnostic result; the verifier recomputes the residuals from the multiplier vector.

Integer arithmetic can perform all these steps. Let positive integers $L,D$ clear denominators in $M,\mathbf b$ and in $\mathbf y,\mathbf c$, respectively, and define
\[
A=LM,\quad B=L\mathbf b,\quad
Y=D\mathbf y,\quad C=LD\mathbf c.
\]
Here $A$ is an integer matrix and $B,Y,C$ are integer vectors used only for this arithmetic representation. The sign check is $(A^TY)_j-C_j\leq0$ for $j\in J_+$, and the resulting bound is $Y^TB/(LD)$. The replay uses arbitrary-precision integers, so accumulation does not wrap at a fixed machine word size. The common matrix denominators occurring in the required chain are $1$ and $6$.

The program \file{replay_required_local_certificates.py} performs these checks for every required local claim. Its report names the checked certificates and records their hashes. The derivations above justify the model variables and rows. The program verifies each resulting rational weighted sum by the exact residual and threshold tests.

\section{Recursive profile coverage and exact polygons}\label{specification:sec:polygons}
The weighted-sum principle is first used to supply the smaller local information needed by later models. For example, a neighborhood of a vertex in a $(4,6)$-graph is a $(3,6)$-graph, while its nonneighborhood is a $(4,5)$-graph. Complete $(3,6)$ catalogues are available at the required orders, but not every required $(4,5)$ edge class has a complete catalogue. The following construction supplies proved containing polygons for the latter classes.

The $\R(4,5,n)$ inputs for $19\leq n\leq23$ consist of $149$ edge classes. Of these, $26$ use complete catalogue hulls; the remaining $123$ use certified support polygons. They are stored in \file{computed_v3_45_19.json} through \file{computed_v3_45_23.json}.

For each of the $123$ edge classes without a complete catalogue, a smaller counting model gives both a lower and an upper bound on $at+bq$. Each such linear bound is called a support inequality. The eight fixed coefficient pairs $(a,b)$ are:
\[
(1,0),(0,1),(1,1),(1,-1),(1,2),(2,1),(1,-2),(2,-1).
\]
Thus there are $123\cdot8\cdot2=1968$ support certificates. Since $t,q$ are integers for a graph, $at+bq$ is integral for an integer direction $(a,b)$. To prove $at+bq\leq U$, a certificate gives
\[
-(at+bq)>-U-1.
\]
The strict inequality and integrality imply the desired bound. Equality with $-U-1$ would not justify it.

To reconstruct a polygon, intersect pairs of nonparallel rational boundary lines, retain intersections satisfying all half-planes, and compute their exact convex hull. Orientation tests use
\[
(x_2-x_1)(y_3-y_1)-(y_2-y_1)(x_3-x_1).
\]
Segments and singletons are handled without perturbation. The largest denominator of the reconstructed rational polygon vertices is $3$. The JSON coordinates include decimal approximations to thirds; they are not all exact terminating decimals. The polygon auditor recovers rational coordinates with denominator at most $10^6$ and checks a discrepancy below $10^{-10}$, then independently verifies equality with the exact half-plane or catalogue hull. The local replay recovers matrix coefficients with denominator at most $6$ and checks a discrepancy below $10^{-8}$. These closeness tests identify the intended rational data; the final residual inequalities and polygon comparisons are performed exactly.

The script \file{audit_recursive_polygons.py} compares stored vertices with the exact intersection of the support half-planes, or with the exact catalogue hull as appropriate. The dual replay establishes the support inequalities used in that intersection.

The models include the following complete degree ranges:
\begin{center}
\begin{tabular}{c|c}
Family&Degrees\\\hline
$\R(4,5,n)$, $19\leq n\leq23$&$n-18,\ldots,13$\\
$\R(4,6,38)$&$13,\ldots,17$\\
$\R(4,6,39)$&$14,\ldots,17$\\
$\R(5,5,44)$&$19,\ldots,24$\\
$\R(5,5,45)$&$20,\ldots,24$
\end{tabular}
\end{center}
For example, in a $(4,6,38)$ graph a neighborhood has no triangle and no independent six-set, so its order is at most $17$; the nonneighborhood is a $(4,5)$ graph of order at most $24$, so the degree is at least $38-1-24=13$. The other ranges follow in the same way from the displayed small Ramsey bounds. The closure audit checks that the program includes each degree in these ranges and every integer edge class allowed for its two local families. Every degree and edge class in the required ranges must be covered before the model can be used.

\section{Endpoints, integrality, and the five local facets}
The endpoint chain gives
\begin{center}
\begin{tabular}{c|rr}
Family&Lower edge bound&Upper edge bound\\\hline
$\R(4,6,38)$&267&314\\
$\R(4,6,39)$&288&324\\
$\R(5,5,44)$&432&514\\
$\R(5,5,45)$&460&530
\end{tabular}
\end{center}
The following certificates prove the endpoints of these intervals. The lower certificates \file{edge_46_38_min.json} and \file{edge_46_39_min.json} give, respectively,
\[
e\geq\frac{43377}{163}>266,\qquad
 e\geq\frac{16965}{59}>287.
\]
Thus their integer lower endpoints are $267$ and $288$. The upper certificates \file{edge_55_44_max.json} and \file{edge_55_45_max.json} give
\[
-e\geq-\frac{113652}{221}>-515,\qquad
-e\geq-\frac{73710}{139}>-531,
\]
so their integer upper endpoints are $514$ and $530$.

The file \file{edge_46_38_max.json} certifies $-e\geq-26125/83$. Since $83\cdot314=26062<26125<26145=83\cdot315$, this gives $e\leq314$. Its model has $25$ rows and $1217$ variables; $17$ dual multipliers are nonzero.

The order-$44$ file \file{edge_55_44_min.json} gives $e\geq95414/221>431$, so $e\geq432$. For order $45$, \file{edge_55_45_min.json} gives
\[
e\geq\frac{12137627230191}{26402663302}>459,
\]
so $e\geq460$. The rational bounds are compared with integer thresholds by exact cross multiplication.

For $\R(4,6,39)$, \file{edge_46_39_max.json} gives $-e\geq-325$, hence $e\leq325$. With $e=325$, two further certificates give
\[
t\geq1612/3,\qquad -t\geq-1612/3.
\]
Thus $t=1612/3$, impossible for a graph. This excludes the last edge count and proves $e\leq324$. The files are \file{exclude_4639e325_t_gt537.json} and \file{exclude_4639e325_t_lt538.json}.

Apply these bounds to the neighborhoods $A_v$ and nonneighborhoods $B_v$ of a hypothetical $84$-vertex graph $X$. The relevant four edge bounds alone do not contradict~\eqref{specification:eq:triple}: at degree $38$, its summand is bounded below by $460-314-152=-6$, and at degree $39$ by $432-324-117=-9$. An argument using only those four bounds therefore stops short of a contradiction. The proof also retains relationships among local edges, triangles, and wedges.

The next table states five such relationships. In each row $Y$ means the local graph named in the first column. The quantity $d_v$ is the degree of its root $v$ in the $84$-vertex graph $X$; in particular, when $Y=B_v$, its order is $83-d_v$. The five numbers $\gamma_d,\gamma_e,\gamma_t,\gamma_q,\gamma_0$ are fixed coefficients of the inequality
\[
\gamma_d d_v+\gamma_e e(Y)+\gamma_t t(Y)+\gamma_q q(Y)+\gamma_0\leq0.
\]
Each table row is a universal assertion for the indicated neighborhood or nonneighborhood family: it must hold at every vertex of any hypothetical $X$.
\begin{center}\small
\begin{tabular}{c|r|rrrrr}
$Y$&File ID&$\gamma_d$&$\gamma_e$&$\gamma_t$&$\gamma_q$&$\gamma_0$\\\hline
$A_v$&203&770&-269&-6&12&5940\\
$B_v$&595&-732&-76&-1&2&49239\\
$B_v$&603&-701&-75&-1&2&47596\\
$B_v$&658&-483&-35&-2&1&29877\\
$B_v$&681&-403&-37&-1&1&26296
\end{tabular}
\end{center}
For example, the first row spells out
\[
770d_v-269e(A_v)-6t(A_v)+12q(A_v)+5940\leq0,
\]
and the second spells out
\[
-732d_v-76e(B_v)-t(B_v)+2q(B_v)+49239\leq0.
\]
The file IDs $203,595,603,658,681$ identify these five coefficient tuples in the saved data. The metadata file \file{exact_candidate_used_facets.json} lists the IDs, their coefficient tuples, and which side they concern. The list in \file{local_profile_facets.json} is indexed by putting the neighborhood list before the nonneighborhood list, with indexing starting at zero. The data files call these inequalities \emph{facets}. Each is used as a valid supporting inequality; the proof requires validity on all relevant profiles.

To prove each inequality for graphs on $38$, $39$, $44$, or $45$ vertices, fix the order of $Y$ and an integer value $e(Y)=e_0$ from the proved intervals. Construct the local counting model for that family with this fixed edge count. A rational weighted sum of its equations then bounds the remaining expression in $t(Y)$ and $q(Y)$. Since every possible $Y$ supplies a feasible assignment, that single calculation proves the inequality for every graph in the chosen order and edge class. The next paragraph gives one such calculation explicitly.

For example, facet 203 at $d_v=38,e=314$ becomes $-6t+12q\leq49266$. The file \file{facet203_46_n38_e314.json} proves
\[
6t-12q\geq-541956/11>-49272.
\]
The strict gap is $36/11$, since $49272\cdot11-541956=36$. Because $-6t+12q$ is a multiple of $6$, it is at most $49266$.

In general, abbreviate $t=t(Y)$ and $q=q(Y)$ for this calculation. At fixed $e(Y)=e_0$, put $K=-\gamma_d d_v-\gamma_e e_0-\gamma_0$ and $g=\gcd(|\gamma_t|,|\gamma_q|)$. The next possible value of $\gamma_t t+\gamma_q q$ above $K$ is $g(\lfloor K/g\rfloor+1)$. Its exclusion is the strict dual threshold. The proved edge intervals determine the complete set of calculations. The neighborhood inequality has $48+37=85$ cases, for the $48$ possible edge counts at order $38$ and the $37$ at order $39$. Each of the four nonneighborhood inequalities has $83+71=154$ cases, for orders $44$ and $45$. Hence the five inequalities require $85+4\cdot154=701$ fixed-edge certificates. Including the $10$ endpoint/exclusion certificates and $1968$ prerequisite support certificates gives $2679$ required local certificates in total.

To check the table computationally, the reader runs \file{replay_required_local_certificates.py} as specified in Section~\ref{specification:sec:execution}. That program determines the required cases from the intervals and coefficient tuples, reconstructs each counting matrix and objective, and verifies its exact weighted-sum certificate. Its successful output must account for all $701$ cases and their prerequisites. Each JSON certificate covers one fixed-edge case.

\clearpage
\section{Seven-vertex probabilities and completeness}
Let $\HH$ contain one representative of each isomorphism class of seven-vertex graphs containing neither $K_5$ nor an independent six-set. Each representative has the fixed labelled vertex set $\{0,\ldots,6\}$ for computations. It has $979$ members. In the remaining counting arguments, let $X$ be a hypothetical member of $\R(5,6,84)$. For each $H\in\HH$, define
\[
p_H=\frac{\#\{W\subseteq V(X):|W|=7,\ X[W]\cong H\}}{\binom{84}{7}}.
\]
Then $p_H\geq0$ and $\sum_Hp_H=1$. Every induced seven-set statistic is linear in this probability vector. All coefficient arrays use the same representative order, stored in \file{profile_cache.npz}.

The set of seven-vertex types is enumerated directly as follows. The probabilities $p_H$ are unknown because $X$ is hypothetical. The coefficient of any stated seven-vertex statistic can be evaluated on each of the $979$ representatives. An inequality for its average is therefore a linear inequality in the unknown $p_H$. Proving that no nonnegative probabilities with sum one can satisfy all those inequalities rules out $X$.

The graph atlas supplies the representative list, and exhaustive labelled enumeration checks its completeness. Encode a labelled seven-vertex graph by its $21$ adjacency bits, enumerate all $2^{21}=2097152$ masks, and directly test all five-subsets and six-subsets. Exactly $2062423$ labelled graphs survive.

For each saved representative, compute its minimum adjacency mask (the integer encoding defined below) over all $7!$ permutations. Verify these canonical masks are distinct, and count each representative's automorphisms. Here $\operatorname{Aut}(H)$ is the group of permutations of $V(H)$ preserving adjacency. Its orbit has $7!/|\operatorname{Aut}(H)|$ labelled graphs. The sums of orbit sizes, separately by edge count, must equal the exhaustive labelled counts. This proves both nonduplication and completeness of the $979$ types.

The script \file{audit_seven_graph_completeness.py} performs this full finite enumeration. It verifies completeness of the seven-vertex type set within the supplied suite.

All dependent arrays use this representative ordering. Hashes and index maps check their consistency. A reimplementation using another order can compare coefficients by graph type.

\section{Exact finite sampling}\label{specification:sec:sampling}
The local inequalities concern quantities such as the degree of a root or the number of edges in a common neighborhood. A seven-set usually contains only part of that information. We therefore assign weights to the portions it contains so that averaging over all seven-sets recovers the full quantity exactly. The sampling formulas below describe these exact averages.

A \emph{root} is a vertex that has been distinguished and whose role must be preserved when configurations are compared. A \emph{flag} is a finite graph together with specified distinguished vertices (roots), whose roles are either an ordered tuple or distinguished unordered groups. Its \emph{type} is its isomorphism class under maps preserving these roles. Vertices not designated as roots form its tail. The flag order $f$ counts both roots and tail vertices. A placement of a fixed labelled flag $F$ into a graph $Y$ is an injective map $\phi:V(F)\to V(Y)$ inducing all edges and nonedges of $F$ and carrying its distinguished roles to the chosen roots. Denote the finite set of such maps by $\operatorname{Emb}(F,Y)$. Taking orbits under automorphisms of $F$ preserving the roles gives the unlabelled placements used by several builders; the conventions are specified in the next section.

Fix a placement of a flag on $f\leq7$ vertices in a graph of order $N=84$, and let $W$ be its vertex image. An \emph{exterior} vertex means a vertex in $V(X)\setminus W$. A seven-set containing the flag samples $7-f$ vertices without replacement from the remaining $N-f$. For $0\leq m\leq7-f$, a specified configuration using $m$ distinct exterior vertices is included with probability
\[
\frac{\binom{N-f-m}{7-f-m}}{\binom{N-f}{7-f}}
=\frac{\binom{7-f}{m}}{\binom{N-f}{m}}.
\]
Thus its observed count is multiplied by
\begin{equation}\label{specification:eq:weight}
W_{f,m}=\frac{\binom{N-f}{m}}{\binom{7-f}{m}}
\end{equation}
to obtain an \emph{unbiased estimate}: a quantity whose average over all choices of the sampled vertices is exactly the full count being studied. Here ``conditional on the flag'' means that its vertices and induced adjacencies are held fixed while the exterior vertices vary.

For example, a fixed six-vertex flag has $78$ exterior vertices. A seven-set containing it selects one of those $78$ vertices uniformly. If exactly $c$ of the exterior vertices lie in a particular cell, its membership indicator is $1$ for $c$ choices and $0$ for the others. Multiplying that indicator by $78$ gives average $c$. For a pair or triple of exterior vertices the same argument gives the binomial factors above.

\begin{lemma}
For a sum of weighted configurations using at most $7-f$ distinct exterior vertices, multiply each observed configuration by \eqref{specification:eq:weight}, classified by its number of distinct exterior vertices. The conditional expectation is exactly the original statistic.
\end{lemma}
\begin{proof}
The inclusion probability cancels the factor separately for each configuration. Sum these equalities by linearity of expectation.
\end{proof}
The word ``distinct'' is essential for products. In $d_xd_y$, one exterior vertex may contribute to both degrees; that term uses one vertex, not two. Repeated positions in a tuple must be handled before assigning a sampling weight.

More explicitly, suppose $I(X,\phi)\leq0$ for every placement $\phi\in\operatorname{Emb}(F,X)$, and let $\widehat I(H,\phi)$ be an estimator formed by the lemma. Its conditional expectation over seven-sets containing the image of $\phi$ is $I(X,\phi)$. Define the coefficient of a seven-vertex representative by
\[
U_F(H)=\sum_{\phi\in\operatorname{Emb}(F,H)}\widehat I(H,\phi).
\]
Interchanging the finite sums over placements and seven-sets proves
\begin{equation}\label{specification:eq:lift-explicit}
\sum_{H\in\HH}p_HU_F(H)
=\frac{\binom{84-f}{7-f}}{\binom{84}{7}}
\sum_{\phi\in\operatorname{Emb}(F,X)}I(X,\phi)\leq0.
\end{equation}
Indeed, each fixed placement belongs to $\binom{84-f}{7-f}$ seven-sets. Equalities lift in the same manner. Counting unlabelled placements divides both sides by the same positive role-preserving automorphism count. Integer scaling and normalization are subsequently recorded in the row metadata. This operation is called \emph{lifting} a local inequality to a global coefficient row.

For flags of sizes $6,5,4$, the exterior population sizes are $78,79,80$. These explain the numerical constants throughout the builders. They are computed for the target order $84$.

\section{Root conventions and canonical masks}
Ordered roots are fixed pointwise under isomorphism. For an unordered clique group $C$ and independent group $D$, permutations within each group are allowed, but the groups are not exchanged. Unrooted flag vertices may be permuted among themselves. These conventions are implemented by \texttt{canon} and \texttt{group\_canon}.

For any ambient graph $Y$, define $a_{uv}=\1_{\{u,v\}\in E(Y)}$ for distinct vertices $u,v$, and $a_{uu}=0$. Given an ordered list $(v_0,\ldots,v_{f-1})$ of distinct vertices of $Y$, encode its induced adjacency by
\[
\operatorname{mask}(Y;v_0,\ldots,v_{f-1})
=\sum_{0\leq i<j<f}a_{v_iv_j}2^{\iota_f(i,j)},
\qquad
\iota_f(i,j)=\frac{i(2f-i-1)}2+j-i-1.
\]
Thus pairs are in lexicographic order, starting with exponent $0$ for $(0,1)$. A graph with its specified vertex order has this mask; root masks use the induced ordered root list. Canonicalization takes the least mask over the allowed permutations. The resulting integer identifies the rooted isomorphism type.

The builders generally enumerate unordered root groups and canonicalize. Several auditors deliberately use a different representation: enumerate all ordered injections inducing the fixed representative mask, then divide by the number of automorphisms preserving the distinguished groups. This division is checked to be exact. It reproduces the same placements and tests root multiplicities independently of the original enumeration.

The Gram construction, by contrast, sums over ordered root tuples and ordered pairs of unordered extension sets. The stored row scales and final multipliers correspond to these counting conventions.

Key files therefore form part of the computational interface. A zero row may be omitted and row order may follow insertion order. An independent implementation should match semantic keys or preserve the saved index ordering exactly.

\section{Base degree and common-neighborhood rows}
Condition on a six-vertex flag rooted at $v$. If $r_0$ counts its neighbors within the flag and $a$ indicates adjacency to the single exterior sample, then $\widehat d=r_0+78a$ is unbiased for $d_v$. The two degree inequalities give the rows $\widehat d-39$ and $38-\widehat d$.

An edge has at most $17$ common neighbors, since its common neighborhood is a $(3,6)$-graph. A nonedge has at most $24$ common nonneighbors, since they form a $(5,4)$-graph. A triangle has at most $5$ common neighbors, and an independent triple has at most $13$ common nonneighbors. If $r_0$ counts the appropriate cell inside a six-vertex flag and $\chi$ marks the exterior vertex, the estimator is $r_0+78\chi$. Subtracting the capacity produces a nonpositive row.

\subsection{Degree-square equalities}
The binary degree condition gives $(d_v-38)(d_v-39)=0$. Condition on a five-vertex flag. If $r_0$ counts root neighbors inside it and $a,b$ are adjacency indicators for the two exterior samples, twice an unbiased estimator is
\begin{equation}\label{specification:eq:square-est}
2\cdot79\cdot78ab+(2r_0-76)79(a+b)+2(r_0-38)(r_0-39).
\end{equation}
Indeed, let $m_{\rm ext}$ be the number of exterior neighbors, so $d_v=r_0+m_{\rm ext}$. Then $\E(a+b)=2m_{\rm ext}/79$ and $\E(ab)=m_{\rm ext}(m_{\rm ext}-1)/(79\cdot78)$. The expectation of \eqref{specification:eq:square-est} is
\[
2m_{\rm ext}(m_{\rm ext}-1)+2(2r_0-76)m_{\rm ext}+2(r_0-38)(r_0-39)
=2(d_v-38)(d_v-39).
\]
The rows are homogeneous equalities. Probability normalization is stored separately and is not treated as another zero-right-hand-side equation.

The builder is \file{finite_profiles.py}. The auditor \file{audit_used_base_rows.py} reconstructs the required rows by labelled injections and weighted subset counts. For degree squares it uses the equivalent expression $2\binom d2-76d+1482$, confirming the polynomial through a different expansion.

\section{Mixed common-neighborhood cells}
Let $C,D\subseteq V(X)$ be disjoint vertex sets, where $C$ is a clique and $D$ is independent. We seek vertices adjacent to every member of $C$ and nonadjacent to every member of $D$. Their set, called a \emph{mixed cell}, is
\[
\mathcal C(C,D)=\{x\in V(X)\setminus(C\cup D):x\sim c\ \forall c\in C,
\quad x\not\sim d\ \forall d\in D\}.
\]
Here $x\sim c$ means $\{x,c\}\in E(X)$, and $x\not\sim d$ means $\{x,d\}\notin E(X)$. Write $p=|C|$ and $h=|D|$, with $0\leq p\leq4$ and $0\leq h\leq5$. The induced cell graph $X[\mathcal C(C,D)]$ belongs to $\R(5-p,6-h,|\mathcal C(C,D)|)$. A forbidden clique inside it extends with $C$, and a forbidden independent set extends with $D$.

The sizes of these cells are bounded by small Ramsey numbers. The following table records the maximum allowed size used for each displayed pair $(p,h)$; the indices $p$ and $h$ are the two root-group sizes:
\begin{center}\small
\begin{tabular}{c|rrrrrrrrrr}
$(p,h)$&(1,1)&(1,2)&(1,3)&(1,4)&(2,1)&(2,2)&(2,3)&(3,1)&(3,2)&(4,1)\\\hline
$|\mathcal C(C,D)|\leq$&24&17&8&3&13&8&5&4&3&0
\end{tabular}
\end{center}
Each entry is $\operatorname{cap}(p,h):=R(5-p,6-h)-1$, using standard small Ramsey numbers or the immediate formulas for a parameter $1$ or $2$.

For a six-vertex flag containing the root groups, let $r_0$ count cell vertices already in its tail. For the exterior sample $z$, set
\[
\chi(z)=\prod_{c\in C}a_{cz}\prod_{d\in D}(1-a_{dz}).
\]
The row contribution is
\[
r_0+78\chi(z)-\operatorname{cap}(p,h).
\]
The roots are excluded from the cell. This is especially important if $C$ is empty: an independent root is nonadjacent to itself under the zero diagonal convention, so omitting the exclusion would count roots incorrectly.

The builder is \file{mixed_cells.py}; \file{audit_used_exact_rows.py} reconstructs selected rows with ordered injections and group-preserving automorphism factors. It derives the capacities from the corresponding Ramsey bounds.

\section{Cell integrality and binary degree products}
For integers $c,k$,
\begin{equation}\label{specification:eq:int}
(c-k)(c-k-1)\geq0.
\end{equation}
Here $c$ is the actual integer size of a mixed cell and $k$ is any chosen integer threshold. Condition on a five-vertex flag containing its roots. Let $r_0$ count cell vertices in that flag, let $u,v$ be the two distinct exterior samples, and let $a=\1_{u\in \mathcal C(C,D)}$, $b=\1_{v\in \mathcal C(C,D)}$. Twice an unbiased estimate of \eqref{specification:eq:int} is
\[
2\cdot79\cdot78ab+2(r_0-k)79(a+b)+2(r_0-k)(r_0-k-1).
\]
The stored row is its negative, since every global inequality uses the nonpositive convention. The final certificate uses $131$ rows of this type.

The auditor constructs estimates of $c$ and $\binom c2$ by counting subsets and then applies
\[
(c-k)(c-k-1)=2\binom c2-2kc+k(k+1).
\]
This checks the expanded formula and its sample factors without reusing the original expansion.

\subsection{Products of degrees}
Put $\varepsilon_v=d_v-38\in\{0,1\}$. For two ordered roots $x,y$, the three quantities
\[
\varepsilon_x\varepsilon_y,\qquad(1-\varepsilon_x)(1-\varepsilon_y),\qquad \varepsilon_x(1-\varepsilon_y)
\]
are nonnegative. Reversing the root order supplies the complementary mixed product.

Condition on a five-vertex flag containing the two ordered roots $x,y$. Let $u,v$ be the two distinct exterior sample vertices. Put $r_x=|N_X(x)\cap W|$ and $r_y=|N_X(y)\cap W|$, where $W$ is the flag vertex set, and define $x_u=a_{xu}$, $x_v=a_{xv}$, $y_u=a_{yu}$, $y_v=a_{yv}$. Twice the degree estimates are
\[
D_x=2r_x+79(x_u+x_v),\quad D_y=2r_y+79(y_u+y_v).
\]
Twice an unbiased estimate of $d_xd_y$ is
\begin{align}
P_{xy}={}&2r_xr_y+79\bigl(r_x(y_u+y_v)+r_y(x_u+x_v)\bigr)\notag\\
&+79(x_uy_u+x_vy_v)+79\cdot78(x_uy_v+x_vy_u).\label{specification:eq:prod}
\end{align}
The terms in which the same sample serves both degrees have coefficient $79$, not $79\cdot78$.

Define $H_x=D_x-76$, $H_y=D_y-76$, and
\[
H_{xy}=P_{xy}-38(D_x+D_y)+2\cdot38^2.
\]
Twice the three nonnegative products are estimated by $H_{xy}$, $2-H_x-H_y+H_{xy}$, and $H_x-H_{xy}$. Their negatives give the stored rows; $69$ occur in the final sum. The independent auditor enumerates ordered neighbor pairs, permits coincident positions, and chooses weights by the number of distinct exterior vertices.

\section{Edge and profile inequalities inside cells}
Let $Y$ be the induced graph $X[\mathcal C(C,D)]$ when edges of $X$ are being counted, and let $Y=\overline{X[\mathcal C(C,D)]}$ when nonedges are being counted. We call these the red and blue cases, respectively. Suppose rational constants $\alpha,\beta$ give a valid support $e(Y)\geq\alpha|Y|+\beta$ for the relevant family. Condition on a five-vertex flag with vertex set $W$ containing the roots. Put $I=\mathcal C(C,D)\cap W$, $r_0=|I|$, and let $e_I$ count pairs from $I$ that are edges in the selected color. For exterior vertices $u,v$, let $\chi_u,\chi_v$ be cell indicators and
\[
z_u=\chi_u\sum_{w\in I}\epsilon_{uw},\quad
z_v=\chi_v\sum_{w\in I}\epsilon_{vw},
\]
where, for distinct $u,w$, $\epsilon_{uw}=a_{uw}$ in red and $\epsilon_{uw}=1-a_{uw}$ in blue. The indicators are $\chi_u=\1_{u\in \mathcal C(C,D)}$ and $\chi_v=\1_{v\in \mathcal C(C,D)}$. The following $C_2$ and $E_2$ are twice unbiased estimates of $|Y|$ and $e(Y)$, respectively:
\begin{align}
C_2&=2r_0+79(\chi_u+\chi_v),\\
E_2&=2e_I+79(z_u+z_v)+79\cdot78\chi_u\chi_v\epsilon_{uv}.
\end{align}
The expression $\alpha C_2+2\beta-E_2$ has average $2(\alpha|Y|+\beta-e(Y))\leq0$, so summing it over flag placements produces a valid global inequality. In $E_2$, the term $2e_I$ counts edges already inside the fixed flag; $79(z_u+z_v)$ accounts for edges with one endpoint outside it; and the final term accounts for edges with both endpoints outside it. These three cases explain every sampling factor in the formula.

The final sum uses two rows from \file{cell_edge_cuts.py}. The auditor checks that these selected supports concern the $(4,4)$ family and verifies them on every supplied profile point. These two selected rows are the cell-edge supports used in the final weighted sum.

\subsection{Full cell profiles}
Let $\mathcal A\subseteq\mathbb Q^4$ be a finite set whose convex hull contains the profile $(|Y|,e(Y),t(Y),q(Y))$ of every graph $Y$ in the cell family under consideration. Write $(c,e,t,q)$ for coordinates in this four-dimensional space; thus $c$ is the order of the cell graph. If fixed rational coefficients $\gamma_c,\gamma_e,\gamma_t,\gamma_q,\gamma_0$ satisfy
\[
\gamma_c c+\gamma_e e+\gamma_t t+\gamma_q q+\gamma_0\leq0
\qquad\text{for every }(c,e,t,q)\in\mathcal A,
\]
then the inequality holds on $\operatorname{conv}(\mathcal A)$ and hence on every actual cell profile. The points in $\mathcal A$ need not all be actual profiles. The saved integer normals are checked on every point. Any collection of valid supporting inequalities gives a containing region for the profiles.

The general cell-profile builder uses the following types:
\begin{center}
\begin{tabular}{cccl}
$|C|$&$|D|$&Counted color&Profile family\\\hline
2&0&red&$(3,6)$\\
0&3&blue&$(3,5)$\\
2&1&red&$(3,5)$\\
1&2&red or blue&$(4,4)$\\
2&2&red&$(3,4)$\\
1&3&blue&$(3,4)$
\end{tabular}
\end{center}
The blue profiles are those of the complement of the induced cell graph.

Condition on a four-vertex flag and use three exterior samples. Multiplying by $6$ gives integer weights
\begin{equation}\label{specification:eq:w6}
6\frac{\binom{80}{m}}{\binom3m}=6,160,6320,492960
\quad(m=0,1,2,3).
\end{equation}
For each coordinate, enumerate the corresponding subsets of the cell visible in the seven-set: single vertices for $c$, edges for $e$, and three-sets with their triangle or $q$ contribution. Give a subset with $m$ vertices outside the flag the corresponding weight in~\eqref{specification:eq:w6}; give the constant coordinate weight $6$. The resulting five-component vector estimates $6(c,e,t,q,1)$ without bias. A three-set contributes $1$ to $t$ if it is a triangle, and contributes $1$ or $2$ to $q$ if it is an induced path or triangle, respectively. Its scalar product with $(\gamma_c,\gamma_e,\gamma_t,\gamma_q,\gamma_0)$ estimates six times the valid inequality. Summing over flag placements as in~\eqref{specification:eq:lift-explicit} gives the row.

\subsection{Small-order outer sets}\label{specification:sec:small-order}
The $(3,5)$ and $(4,4)$ point sets are built from supplied complete catalogues, together with directly enumerable lower orders. The $(3,4)$ set is extracted by filtering the relevant $(3,5)$ graphs. For $(3,6)$ below order $13$, the builder uses the following explicit outer regions. For $1\leq c\leq12$, each integer edge count satisfies
\[
\ell(c)\leq e\leq\min\{\lfloor5c/2\rfloor,\lfloor c^2/4\rfloor\},
\qquad
\ell(c)=\begin{cases}0&c\leq5,\\c-5&6\leq c\leq10,\\3c-25&11\leq c\leq12.\end{cases}
\]
The lower bounds are the $k=5$ cases of \cite[Theorem~2]{specification:trianglefree}; this is an additional established mathematical input. A neighborhood in a triangle-free graph is independent, so the independence restriction gives maximum degree $5$; handshaking gives the first upper bound. Mantel's theorem gives the second upper bound. At order zero, the single profile is $(0,0,0,0)$.

Triangle-freeness gives $t=0$ and $q=w$. For $c\geq1$, define the Euclidean quotients and remainders by $2e=ck+r_0$ with $0\leq r_0<c$, and $2e=5s_0+r_1$ with $0\leq r_1<5$. Then convexity of $\binom d2$ on integer degrees gives
\[
c\binom k2+r_0k\leq q\leq10s_0+\binom{r_1}{2}.
\]
The lower bound balances the degrees as evenly as possible; the upper bound fills degrees to $5$ before using a remainder. Graphicality is not assumed for these extremizing degree lists, so the interval is safely an outer bound. The builder adds both endpoints at each $(c,e)$ and takes their hull. This constructs the containing region from degree bounds at these lower orders.

The packaged bridge audit regenerates the point arrays and links the saved arrays to these rules. The regenerated arrays therefore connect the checked facet coefficients to the stated catalogue and degree bounds.

\section{Restricted edge cores and critical order 17}
For an edge $uv$, its common neighborhood has at most $17$ vertices. It has at least $13$, since the neighbors of $u$ other than $v$ that are not adjacent to $v$ form a $(4,5)$-graph and hence number at most $24$:
\[
|N(u)\cap N(v)|\geq d_u-1-24\geq13.
\]
If $d_u=39$, this improves to $14$. Thus complete $(3,6)$ catalogues of orders $13$ through $17$ suffice for the edge core. Restricted profile hulls from these catalogues are stronger than a hull allowing all smaller orders. Nine such lifted rows occur in the final sum.

The files are \file{restricted_edge_core_points.npy}, \file{restricted_edge_core_facets.json}, and \file{restricted_edge_core_profile_cuts.npz}. The auditor verifies facets on points and reconstructs the lifts. It additionally checks \file{degree_core_defect_cuts.npz}, although none of those rows has a nonzero final weight.

\subsection{A cubic inequality from the seven critical graphs}
The seven graphs in $\R(3,6,17)$ have every degree in $\{4,5\}$. For a triangle $uvw$ with distinguished edge $uv$, define
\[
c=|N(u)\cap N(v)|,\qquad
\tau=|N(u)\cap N(v)\cap N(w)|.
\]
If $c=17$, then $\tau$ is the degree of $w$ in the critical edge core and belongs to $\{4,5\}$. If $c\leq16$, both $16-c$ and the integer polynomial $(\tau-4)(\tau-5)$ are nonnegative. Hence
\begin{equation}\label{specification:eq:cubic}
(16-c)(\tau-4)(\tau-5)\geq0.
\end{equation}
The related linear inequality $\tau\geq2c-30$ follows from $\tau\geq0$ when $c\leq15$. When $c=16$, consider the nonneighbors of $w$ inside the edge core. They form a $(3,5)$-graph, so there are at most $13$ of them; hence $16-1-\tau\leq13$ and $\tau\geq2$. When $c=17$, the catalogue gives $\tau\geq4$. The four selected critical-core rows are cubic.

Condition on a four-vertex flag with vertex set $W$ containing $u,v,w$. Let $\mathcal O=V(X)\setminus W$, and define
\[
c_0=|W\cap N(u)\cap N(v)|,\qquad
\tau_0=|W\cap N(u)\cap N(v)\cap N(w)|.
\]
For $i\in\mathcal O$, set $p_i=\1_{i\in N(u)\cap N(v)}$ and $q_i=\1_{i\in N(u)\cap N(v)\cap N(w)}$. Put $P=\sum_{i\in\mathcal O}p_i$ and $Q=\sum_{i\in\mathcal O}q_i$, so $c=c_0+P$, $\tau=\tau_0+Q$, and $q_i\leq p_i$. Every index in the following sums ranges over $\mathcal O$; pairs and triples are ordered and obey the displayed distinctness conditions. The overlap expansions are
\[
Q^2=Q+\sum_{i\ne j}q_iq_j,\qquad
PQ=Q+\sum_{i\ne j}p_iq_j,
\]
\[
PQ^2=Q+\sum_{i\ne j}p_iq_j+2\sum_{i\ne j}q_iq_j
+\sum_{i,j,k\text{ distinct}}p_iq_jq_k.
\]
They separate all-equal, one-pair-equal, and all-distinct tuples. Assigning weights from \eqref{specification:eq:w6} gives the exact cubic estimator. The auditor evaluates ordered products directly, including coincidences, to check the original expanded formula independently.

\section{Lifting the four local edge bounds and five facets}
At degrees $38$ and $39$, the local edge bounds are equivalent to
\[
e(A_v)\leq10d_v-66,\qquad e(B_v)\geq1524-28d_v.
\]
For a five-vertex flag rooted at $v$, let $r_0$ count neighbors in the flag and let $x,y$ be exterior samples. Put
\[
D_2=2r_0+79(a_{vx}+a_{vy}).
\]
Using the preceding edge estimator for either cell, the lifted rows are
\[
E_2(A_v)-10D_2+132,
\qquad -E_2(B_v)-28D_2+3048.
\]
The underlying bounds are established by local dual certificates; this construction establishes their finite averaged coefficients. 

For a full local facet, choose $Y=A_v$ or $Y=B_v$ as specified by that facet. Condition on a four-vertex flag rooted at $v$ and take three exterior samples. Define its five-component feature vector by the same weighted subset procedure, counting the root's neighbors for the degree coordinate and subsets of $Y$ for the remaining graph statistics. It is three times an unbiased estimate of
\[
(1,d_v,e(Y),t(Y),q(Y)).
\]
The integer sampling factors are
\[
3\frac{\binom{80}{m}}{\binom3m}=3,80,3160,246480.
\]
The same degree coordinate $d_v$ is used for both $Y=A_v$ and $Y=B_v$. The feature array \file{local_profile_features.npy} is contracted with coefficient vector $(\gamma_0,\gamma_d,\gamma_e,\gamma_t,\gamma_q)$.

The exact matrix builder performs the contraction in integer arithmetic. The packaged bridge audit checks that the five used coefficient tuples agree with the certified facet metadata.

The feature auditor reconstructs the array through the general cell estimator at scale $6$, checks divisibility by $2$, and compares with the scale-$3$ array. For the nonneighborhood case, it still uses the red root-degree coordinate and only changes the edge, triangle, and $q$ cell coordinates. Thus its degree feature represents $d_v$ on both sides.

\section{The exact finite Gram identity}\label{specification:sec:gram}
The preceding sections obtained inequalities from degrees, cell sizes, and local profiles. We now add inequalities of another elementary kind: the square of any real expression is nonnegative. The expressions to be squared are linear combinations of counts of small configurations extending fixed roots. Expanding a square introduces pairs of such configurations. Their union has at most seven vertices, so its contribution can be expressed in the seven-vertex probabilities.

The matrices below organize this expansion. A \emph{Gram matrix} here is a sum of matrices $ff^T$ formed from count vectors $f$. For a real coefficient vector $z$, the corresponding quadratic expression is a sum of squares $(z^Tf)^2$ and is nonnegative. The following counting identity expresses the averaged matrix in this form.
Fix nonnegative integers $\ell,k$ with $\ell+2k\leq7$. A root type $\sigma$ is a graph on the ordered vertex set $\{1,\ldots,\ell\}$. Let $\mathcal F_{\sigma,k}$ be the finite set of isomorphism classes of graphs on $\ell+k$ vertices that have neither $K_5$ nor an independent six-set, and whose first $\ell$ distinguished ordered vertices induce $\sigma$. Isomorphisms fix every distinguished root and may permute the $k$ remaining vertices. Fix the saved ordering of these classes, with indices $i\in\{1,\ldots,m_{\sigma,k}\}$, where $m_{\sigma,k}=|\mathcal F_{\sigma,k}|$.

For an ordered tuple $\rho=(v_1,\ldots,v_\ell)$ of distinct vertices in a graph $Y$ with neither $K_5$ nor an independent six-set, let $V(\rho)=\{v_1,\ldots,v_\ell\}$. The notation $Y[\rho]=\sigma$ means that $v_i\mapsto i$ identifies the root adjacencies with $\sigma$. For $S\in\binom{V(Y)\setminus V(\rho)}{k}$, write $\operatorname{type}_Y(\rho,S)$ for the index in $\mathcal F_{\sigma,k}$ of the induced graph on $V(\rho)\cup S$ with this ordered root tuple. For each such $\rho$ in $X$, define
\begin{align*}
f_i(\rho)&=\bigl|\{S\in\tbinom{V(X)\setminus V(\rho)}{k}:
\operatorname{type}_X(\rho,S)=i\}\bigr|,\\
f(\rho)&=(f_1(\rho),\ldots,f_{m_{\sigma,k}}(\rho))^T.
\end{align*}

For a fixed root tuple, $f_i(\rho)$ counts the ways to choose $k$ additional vertices of type $i$. Consequently, $f_i(\rho)f_j(\rho)$ counts ordered pairs of choices of types $i$ and $j$, including choices that share additional vertices. Gathering these products into a matrix and summing over root tuples gives
\[
\sum_{\rho:X[\rho]=\sigma}f(\rho)f(\rho)^T\succeq0,
\]
because for every real vector $z$ its contraction is a sum of squares
\[
\sum_{\rho:X[\rho]=\sigma}\left(\sum_i z_i f_i(\rho)\right)^2\geq0.
\]
To express this on seven-vertex graphs, consider roots and an ordered pair of unordered extension sets $S,T$. Their union with the roots has $\ell+|S\cup T|$ vertices. It occurs in exactly
\[
\binom{84-\ell-|S\cup T|}{7-\ell-|S\cup T|}
\]
seven-sets. Give it the reciprocal of this number as weight. For a representative $H\in\HH$, let $\mathcal D_H$ consist of all triples $(\rho,S,T)$ such that $\rho$ is an ordered $\ell$-tuple of distinct vertices of $H$ inducing $\sigma$, and $S,T\in\binom{V(H)\setminus V(\rho)}{k}$. The pair $(S,T)$ is ordered, and $S\cap T$ may have any size from $0$ to $k$. Define the symmetric $m_{\sigma,k}\times m_{\sigma,k}$ matrix
\begin{equation}\label{specification:eq:MH}
M_H(i,j)=\sum_{(\rho,S,T)\in\mathcal D_H}
\frac{\1_{\operatorname{type}_H(\rho,S)=i}\1_{\operatorname{type}_H(\rho,T)=j}}
{\binom{84-\ell-|S\cup T|}{7-\ell-|S\cup T|}}.
\end{equation}
The denominator is positive because $\ell+|S\cup T|\leq7$. This definition applies to any allowed seven-vertex graph and is invariant under relabelling, so $M_{X[W]}$ denotes the same matrix as the isomorphic representative in $\HH$. Summing over all seven-sets of $X$ counts each global pair exactly once:
\[
\sum_{W\in\binom{V(X)}7}M_{X[W]}=\sum_{\rho:X[\rho]=\sigma}f(\rho)f(\rho)^T.
\]
Dividing by $\binom{84}{7}$ proves
\begin{equation}\label{specification:eq:PSD}
\sum_Hp_HM_H\succeq0.
\end{equation}
All overlap sizes, including $S=T$, occur in the product of the two configuration counts and hence in~\eqref{specification:eq:PSD}.

Individual matrices $M_H$ need not be positive semidefinite. The statement is about their average under a distribution arising from an $84$-vertex graph. This is why a small graph can have a positive coefficient in a row whose global average is necessarily nonpositive.

\section{Integer blocks, square vectors, and overflow checks}
A \emph{block} is the matrix family belonging to one fixed choice of root type $\sigma$ and extension size $k$. We use $(\ell,k)=(0,3),(1,3),(2,2),(3,2)$. There is one root type at each of orders $0$ and $1$, two at order $2$ (an edge and a nonedge), and four at order $3$ (zero, one, two, or three edges). Thus there are $1+1+2+4=8$ blocks. The dimensions in the table count the possible rooted extension types, so matrices from different blocks need not have the same size. Clearing denominators in \eqref{specification:eq:MH} gives $I_H=LM_H$ with integer entries:
\begin{center}
\begin{tabular}{ccrr}
\toprule
$(\ell,k)$&Root mask&Dimension&$L$\\\midrule
$(0,3)$&0&4&6654960\\
$(1,3)$&0&20&246480\\
$(2,2)$&0&20&246480\\
$(2,2)$&1&20&246480\\
$(3,2)$&0&72&6162\\
$(3,2)$&1&72&6162\\
$(3,2)$&3&72&6162\\
$(3,2)$&7&71&6162\\\bottomrule
\end{tabular}
\end{center}
Here the dimension is $m_{\sigma,k}$, and $L$ is the least common multiple of the overlap denominators for the indicated block; its value depends on $(\ell,k)$. In the saved block names, the field \texttt{r} records the root order $\ell$. For each saved integer vector $z\in\mathbb Z^{m_{\sigma,k}}$ belonging to this block, the row
\[
Q_z(H)=-z^TI_Hz
\]
has nonpositive average by \eqref{specification:eq:PSD}. Its entries can have either sign.

The file \file{rational_psd_vectors.json} stores block names, integer vectors, and positive normalization denominators. The file \file{rational_psd_numerators.npy} stores their rows. There are $448$ saved vectors and $194$ used vectors. The used vectors have $11048$ nonzero entries in total.

The program \file{rebuild_integer_moments.py} enumerates ordered roots and every ordered pair of extension subsets, assigns rooted type indices from \file{moment_keys.json}, and adds the integer overlap weight. In check-only mode it compares the result with \file{moment_integer_verified.npz}.

One independent replay uses arbitrary-precision Python integers for every contraction. Another uses fixed-width arrays only after checking a sufficient bound. If entries of $I_H$ are nonnegative and at most $B$, then
\[
|z^TI_Hz|\leq B\left(\sum_i|z_i|\right)^2.
\]
The latter quantity must be below $2^{63}$ before signed 64-bit arithmetic is used. The final separation accumulation also uses exact integers. Both implementations evaluate the contractions in the Gram identity.

\section{Row normalization and exact source linkage}
At this stage each valid inequality has been converted into a list of $979$ rational coefficients, one for each seven-vertex type $H$. We call such a list a \emph{row}. Its statement is that the weighted average of its entries, with weights $p_H$, is nonpositive. A homogeneous equality row instead has weighted average zero. The word ``homogeneous'' means that the right-hand side is zero. Probability normalization has right-hand side one, so it must be kept separate.

The numerical files collect these rows in matrices. This section specifies their ordering and scales so that a reader can match the previously justified formulas to the precise rows multiplied by the final certificate.
Use the fixed ordering of the $979$ representatives $H\in\HH$ as column indices. The file \file{exact_linear_model.npz} stores an integer matrix $U$ with $4876$ rows and an integer matrix $E$ with $90$ rows, together with positive integer denominator vectors $U_{\rm den}$ and $E_{\rm den}$. The indices in the data files are zero-based: $i\in\{0,\ldots,4875\}$ for $U$ and $j\in\{0,\ldots,89\}$ for $E$. In each case the denominator is the maximum absolute entry in that row, with denominator $1$ for a zero row. Positive scaling preserves a homogeneous equality or a nonpositive inequality.

The first $89$ rows of $E$ are homogeneous degree-square equalities. The last row, indexed by $89$, is all ones with denominator $1$ and expresses probability normalization, with right-hand side $1$. Define the normalized homogeneous row functions only for $j<89$ by
\[
E_j(H)=\frac{E_{jH}}{E_{{\rm den},j}}
\qquad(0\leq j<89).
\]
The square data contain $448$ ordered entries. For square index $a\in\{0,\ldots,447\}$, let $z_a$ be its saved integer vector, let $Q_a(H)=-z_a^TI_Hz_a$ use its specified block, and let $d_a>0$ be its saved normalization denominator. This denominator is verified to equal $\max_H|Q_a(H)|$. Define all normalized inequality rows by
\[
U_i(H)=
\begin{cases}
U_{iH}/U_{{\rm den},i},&0\leq i<4876,\\
Q_{i-4876}(H)/d_{i-4876},&4876\leq i<5324.
\end{cases}
\]
The necessary global constraints, in addition to $p_H\geq0$ and $\sum_Hp_H=1$, are precisely
\[
\sum_{H\in\HH}U_i(H)p_H\leq0\quad(0\leq i<5324),
\qquad
\sum_{H\in\HH}E_j(H)p_H=0\quad(0\leq j<89).
\]
The final sum uses $87$ homogeneous rows and excludes the normalization row from this zero-right-hand-side system. 

The file \file{exact_linear_model_keys.json} maps each linear row to its source family and source index. For local profile rows, integer coefficients are reconstructed from the facet and feature arrays rather than rounded from a numerical matrix.

The program \file{audit_packaged_model.py} checks the complete source linkage of all $4876$ linear rows and all $89$ homogeneous equalities, their normalization denominators, and the five final facet tuples. It also regenerates the cell-profile point arrays from their declared catalogue and outer-bound sources. The resulting point counts are $42,215,611,3638$ for families $(3,4),(3,5),(3,6),(4,4)$ respectively, and $358$ for the restricted edge-core set.

This check identifies the rows used in the final weighted sum with the rows reconstructed from the counting formulas.

\section{The separating sum and its strict margin}\label{specification:sec:separation}
The file \file{exact_separation_certificate.json} supplies the final equation and inequality multipliers. They are rational numbers with common positive denominator $W=10^{12}$. Complete its two lists with zero values at unlisted indices, thereby defining
\[
\lambda_i\in\mathbb Q_{\geq0}\ (0\leq i<5324),\qquad
\mu_j\in\mathbb Q\ (0\leq j<89).
\]
The supports $I_*:=\{i:\lambda_i\ne0\}$ and $J_*:=\{j:\mu_j\ne0\}$ have sizes $816$ and $87$, respectively. The total number of nonzero multipliers is $903$. Put
\[
C(H)=\sum_{i=0}^{5323}\lambda_iU_i(H)+\sum_{j=0}^{88}\mu_jE_j(H).
\]
The average of $C$ under any valid probability vector $(p_H)_{H\in\HH}$ is nonpositive. This follows by multiplying each inequality by its nonnegative $\lambda_i$, each equality by its signed $\mu_j$, and adding. Equality multipliers may have either sign because an equality remains true when multiplied by a negative number. Inequality multipliers must be nonnegative to preserve their direction.

The remaining finite calculation evaluates $C(H)$ separately for every one of the $979$ columns. It uses the saved rational multipliers and the row coefficients already linked to the counting formulas. The aim is to prove that every one of these $979$ numbers is positive. If this succeeds, any nonnegative weighted average with total weight one would also be positive, contradicting the previous paragraph. Thus no search over unknown probability vectors is required during verification.

For a precise description of the integer lower-bound calculation, form the disjoint term index set
\[
\mathcal K=(\{\mathrm{ineq}\}\times I_*)\ \cup\ (\{\mathrm{eq}\}\times J_*).
\]
For a term $k\in\mathcal K$, denote its integer multiplier numerator by $w_k$, its integer row numerator at $H$ by $a_{kH}$, and its positive integer row denominator by $d_k$. These are obtained from the corresponding linear row or square row just defined. Thus its contribution to $C(H)$ is $w_ka_{kH}/(Wd_k)$. With the additional positive scale $F=10^{12}$,
\[
\frac{w_ka_{kH}}{Wd_k}
\geq\frac{\lfloor Fw_ka_{kH}/d_k\rfloor}{WF}.
\]
Floor division is required also for negative numerators. Truncating toward zero would give an upper rather than a lower approximation for negative terms.

For each $H\in\HH$, compute the integer
\[
L_H=\sum_{k\in\mathcal K}\left\lfloor\frac{Fw_ka_{kH}}{d_k}\right\rfloor,
\qquad C(H)\geq\frac{L_H}{WF}.
\]
The minimum is
\begin{equation}\label{specification:eq:margin}
\min_HL_H=3146981978575629437>0.
\end{equation}
Thus $C(H)\geq\delta$ for every $H$, where
\[
\delta=\frac{3146981978575629437}{10^{24}}>0.
\]
The weighted constraints give the first inequality below, the columnwise positive bounds give the second, and probability normalization gives the equality:
\[
0\geq\sum_Hp_HC(H)\geq\delta\sum_Hp_H=\delta>0.
\]
This proves $\R(5,6,84)=\varnothing$, subject to the stated external inputs.

Any strictly positive lower bound on every coefficient yields this contradiction. Downward rounding preserves the required lower-bound direction.

\section{Which rows have nonzero final weights}
The following table counts the rows with nonzero weight in the final certificate.
\begin{center}
\begin{tabular}{lr}
\toprule
Inequality family&Used rows\\\midrule
Base degree and capacity rows&315\\
Mixed-cell capacities&29\\
Cell edge supports&2\\
Cell integrality&131\\
Binary degree products&69\\
General cell profiles&31\\
Restricted edge-core profiles&9\\
Critical-core cubic inequalities&4\\
Neighborhood edge bounds&9\\
Neighborhood profile inequalities&23\\
Integer-vector squares&194\\\midrule
Total&816\\\bottomrule
\end{tabular}
\end{center}
There are also $87$ homogeneous equality terms. These counts provide useful checks of the selected-row interface.

The $23$ neighborhood profile rows arise by conditioning the five local facets on different rooted flag types. The stored degree-core defect rows are audited and have zero weight in the final sum.

Several auditors check a larger collection containing all rows selected by the final certificate. Their reports specify this coverage, so their row counts may exceed those in the table.

The final JSON and row-key arrays determine the rows used in the proof. Some auditors read \file{phase1_duals.npz} or \file{phase1_used_rows.json} to select a larger set of rows to check. These files are runtime dependencies; their role is to select checks, and their numerical weights are not premises of the final weighted sum.

\section{Catalogue extraction and its precise trust boundary}
A graph6 catalogue stores graphs; a \file{.profiles} file stores distinct tuples $(n,e,t,q)$. The local model uses the set of possible profiles. Graphs sharing a profile therefore contribute a single tuple. The header separately records the total graph-record count.

The program \file{catalogue_profiles.cpp} decodes every record into adjacency bitsets. It counts edges while decoding, computes $w=\sum_v\binom{d_v}{2}$, and computes triangles from
\[
6t=\sum_{(u,v):uv\in E}^{\text{ordered}}|N(u)\cap N(v)|.
\]
Each triangle contributes six times. The program checks divisibility by six, stores $(n,e,t,w-t)$ in an ordered set, and writes all distinct tuples.

The catalogue audit programs count every record but independently decode only a sample of roughly $100$ profiles per catalogue. The closure audit verifies exact hull containment of all supplied profile points. Full extraction from the raw graph records is checked by the following separate program.

The program \file{regenerate_catalogue_profiles.py} compiles the supplied extractor in a temporary directory, copies raw catalogues there, runs the extractor on all records, and compares complete distinct profile sets and graph counts with the supplied files. Header source paths are not mathematical data and are ignored in the comparison. The collection contains $58$ catalogue files and $11400325$ graph records.

This exhaustively replays the supplied extractor. The sampled NetworkX decoder uses a separate implementation on its selected records. Completeness of the raw catalogue families remains the published external input.

The logical stages are therefore separate: external catalogue completeness; reproducible decoding and profile extraction; exact hull and recursive support verification; exact global coefficient construction; and exact final separation. The extraction replay uses the supplied extractor; the sampled decoder and the specified coefficient auditors provide distinct implementations of their respective calculations.

\section{Environment and safe execution}
The pinned Python requirements are NumPy $2.3.5$, SciPy $1.16.3$, and NetworkX $3.6$. The tested Python version is $3.13.9$. The intended reproduction environment is a fresh Python 3.13 virtual environment with these package versions. NumPy 2.x is relevant because the seven-graph auditor uses \texttt{bitwise\_count}.

From the extracted verification tree, installation is typically
\begin{verbatim}
python3.13 -m venv .venv
. .venv/bin/activate
python -m pip install -r proof_84/requirements.txt
\end{verbatim}
The package README specifies the outer layout and platform variants. Installing packages may require network access; the verification itself uses the supplied data and does not need a solver or online service.

SciPy supplies sparse-matrix operations and hull helpers. The verification commands execute exact checks without invoking an optimization solver.

Full profile regeneration additionally requires a C++11 compiler and zlib development support. On Debian-like systems these are normally provided by compiler and zlib development packages; on macOS a command-line developer toolchain supplies a suitable compiler and system zlib. The wrapper uses a temporary workspace and compares data without rewriting the archived originals.

\paragraph{Assertions must be active.}
Do not run with Python's \texttt{-O} option and do not set \texttt{PYTHONOPTIMIZE}. The supplied programs use assertions for checks; optimized execution disables them. The packaged launcher guards against this condition. A run with assertions disabled is not a verification run.

Use a fresh writable extraction. The driver and auditors create logs and reports. Set \texttt{PYTHONDONTWRITEBYTECODE=1} if desired to avoid bytecode caches, but this does not suppress intended reports. Preserve the original archive for comparison rather than expecting the working copy to remain byte-for-byte unchanged after execution.

\section{Execution recipes and expected output}\label{specification:sec:execution}
The commands below begin from a folder containing the complete file \file{verification.tar.xz}. This is the inner verification archive, not the outer arXiv upload archive. A reader who obtained the full arXiv source upload finds it under \file{anc}; a reader who obtained the separate verification distribution already has this file. Extract it and enter the folder it creates:
\begin{verbatim}
tar -xJf verification.tar.xz
cd verification
\end{verbatim}
The terminal's current folder is now the extracted folder named \file{verification}. It contains \file{verify_package.py}, \file{README.txt}, \file{input_manifest.json}, and the subfolders \file{proof_84}, \file{lp_research}, \file{literature_research}, \file{root_research}, and \file{structural_research}. Every remaining command in this section is run from that folder. The commands neither assume nor use the author's research workspace.

\paragraph{If the compact archive was chosen.}
Its inner archive has the same name but omits the $58$ raw public catalogue files. Restore them before verification by following its \file{START_HERE.txt}. For example,
\begin{verbatim}
python3 restore_catalogues.py --download
\end{verbatim}
uses the network to retrieve the named catalogues and checks each against its recorded SHA256 digest. Alternatively, \texttt{--from-archive} reads them from the complete verification archive. After restoration, the compact route checks the same data by the same programs; it skips no mathematical test. This restoration step is unnecessary for the complete archive.

\paragraph{Install the Python environment once.}
With Python $3.13$ installed, run the following macOS/Linux commands from the extracted \file{verification} folder:
\begin{verbatim}
python3.13 -m venv .venv
. .venv/bin/activate
python -m pip install -r proof_84/requirements.txt
\end{verbatim}
The last command installs the exact package versions used by the supplied verifier and needs network access unless local installation files are available. Subsequent commands use \texttt{python} from this activated environment. A reader who opens a new terminal later must return to the same extracted folder and activate \file{.venv} again. Windows activation instructions are in \file{README.txt}.

\paragraph{Start with one interpretable calculation.}
To reproduce the worked $314$-edge example after installing the dependencies, run
\begin{verbatim}
python check_local_example.py --root .
\end{verbatim}
The dot means the extracted \file{verification} folder, which is the current folder. The checker evaluates the explicitly stated local inequalities on the required profile points and compares the resulting weighted identity with the saved certificate. The worked-method document explains those inequalities and coefficients on paper. This command is a small entry point into the argument; it does not replace the checks of the prerequisite containing polygons or the final seven-vertex contradiction.

\paragraph{Replay the complete certificate.}
Run
\begin{verbatim}
python verify_package.py
\end{verbatim}
A successful run must exit normally and print a final summary with \texttt{"all\_passed": true}. A partial success message followed by an error is not a successful run. The launcher first checks input hashes, then runs the main proof checks, the additional source-linkage check, and the worked-example calculation. Its reports identify which steps succeeded. No optimization solver and no network connection are needed for this replay.

The package-level launcher is \file{verify_package.py}. The package README documents its supported modes and their exact command lines. Its default mode checks package integrity, runs the $18$ jobs in \file{verify_all.py}, performs the source-linkage audit, and runs the worked-example checker. The \texttt{--full} mode also regenerates all catalogue profiles, runs the three additional finite-estimator audits, and checks the separate degree-$24$ strengthening. The finite-estimator tests exhaust samples on their specified test graphs or populations; they test the estimator formulas on those specified finite populations. After installing the C++11 compiler and zlib support described in the preceding section, request the additional extraction and supplementary checks with
\begin{verbatim}
python verify_package.py --full
\end{verbatim}
The commands below isolate parts of that full run for diagnosis or focused review. They still start from the same extracted \file{verification} folder with the environment active. The $18$-job verification suite can be run directly:
\begin{verbatim}
python proof_84/verify_all.py
\end{verbatim}
It launches $18$ jobs with at most three running in parallel. A successful summary has \texttt{all\_passed: true} and \texttt{check\_count: 18}. It records \texttt{solver\_used: false} and \texttt{network\_used: false}. The following sections describe the jobs executed by this command.

For the local chain alone, run
\begin{verbatim}
python literature_research/replay_required_local_certificates.py
\end{verbatim}
It must verify $2679$ certificates: $1968$ support bounds, $10$ endpoints/exclusions, and $701$ facet cases. The corresponding report is \file{required_local_certificate_audit.json}.

After the input rows have been justified by the preceding mathematical arguments and row checks, the final $979$ column sums can be replayed separately with
\begin{verbatim}
python root_research/verify_exact_separation.py --replay
\end{verbatim}
It must report strict separation and the numerator in \eqref{specification:eq:margin}. This command by itself does not prove validity of its row inputs; those are established by the local chain, row audits, and mathematical derivations.

The explicit package bridge and complete extraction checks can be run separately:
\begin{verbatim}
python audit_packaged_model.py
python regenerate_catalogue_profiles.py
\end{verbatim}
If a check fails, retain the log and investigate rather than changing tolerances or bypassing assertions. Missing files, inconsistent row orders, changed package versions, stale data, or a genuine mathematical or programming error must be distinguished. Previous successful reports do not override a reproducible failure on the submitted data.

\section{The 18-job suite: local and catalogue checks}
This section and the next two describe all jobs launched by \file{verify_all.py}, grouped by the part of the proof they check.

\subsection{Required local dual replay}
\file{replay_required_local_certificates.py} derives the required claims from support directions, edge intervals, and selected facets. It reconstructs each model and objective, parses rational duals, forms integer residuals, and checks strict rounding thresholds. It compares the reconstructed objective with the saved objective. The report contains a hash for every required certificate.

\subsection{Recursive polygons}
\file{audit_recursive_polygons.py} reconstructs all $149$ polygons. It checks exact intersections of the $123$ support systems and exact hulls for $26$ catalogue edge classes. Support validity is established by the dual replay, not by this geometric comparison alone.

\subsection{Dependency closure}
\file{audit_dependency_closure.py} compares the model's selected catalogue hull vertices with exact hulls of supplied profile points. Its current scope is $58$ profile files, $331$ edge-class hulls, and $7624$ distinct profile entries across files. It also verifies full degree ranges, edge-bin coverage, row counts, and the version 3 restriction of the version 4 model.

\subsection{Small catalogue records}
\file{audit_catalogues.py} checks record counts against saved source-page information, computes hashes, and independently decodes sampled records. Its sampled profile checks are not exhaustive recomputation. The additional extraction wrapper described above supplies the latter replay.

\subsection{The \texorpdfstring{$(4,5)$}{(4,5)} catalogues}
\file{audit_r45_catalogues.py} checks the order-$24$ catalogue of $352366$ graphs and the selected complete extreme-edge classes of orders $19$ through $23$. It checks all record counts and samples decoded profiles. The expected counts for extreme classes are recorded in supplied headers; mathematical completeness remains external.

Together, these jobs check the catalogue records, their profile hulls, and the local dual inequalities that depend on them.

\section{The 18-job suite: global coefficients}
\subsection{Seven-vertex completeness}
\file{audit_seven_graph_completeness.py} enumerates all $2^{21}$ labelled graphs and compares allowed counts with exact orbit sizes of the saved representatives. It also checks pairwise nonisomorphism. This is a full finite enumeration, unlike the extraction sampling just described.

\subsection{Base rows}
\file{audit_used_base_rows.py} reconstructs degree-square equalities and base capacity inequalities by labelled injections and finite subset weights. It checks every final-used base row and additional stored rows.

\subsection{Mixed cells and general profiles}
\file{audit_used_exact_rows.py} independently reconstructs the selected mixed capacities and general cell-profile rows. It checks the Ramsey family corresponding to each color, tests each selected facet on all stored points, and uses group-preserving automorphism factors.

\subsection{Integrality and binary degrees}
\file{audit_used_integer_rows.py} reconstructs cell-integrality and binary-degree rows by direct subset and ordered-pair enumeration. In degree products, coincident neighbor choices are allowed and weighted according to the number of distinct exterior vertices.

\subsection{Critical cores}
\file{audit_used_core17_rows.py} reconstructs selected cubic rows by enumerating products in the edge and triangle cores, including repeated positions. It checks coefficients on every seven-vertex representative. The underlying catalogue degree fact supplies the sign of the cubic polynomial.

\subsection{Cell edge supports}
\file{audit_used_cell_edge_rows.py} validates the selected supporting lines on the $(4,4)$ point set and reconstructs their lifted coefficients. 

\subsection{Neighborhood edges}
\file{audit_used_neighborhood_edge_rows.py} reconstructs the finite lifts of the four local edge bounds. The local dual chain supplies their mathematical validity; this job checks finite sampling and multiplicity.

\subsection{Neighborhood profile features}
\file{audit_root_local_features.py} recomputes the complete local feature array via the general cell estimator at twice the stored scale, checks divisibility, and compares entries. The packaged bridge then checks its integer contraction with the selected five facets into the exact global matrix.

\subsection{Restricted edge cores}
\file{audit_restricted_core_rows.py} checks all restricted profile rows and additional degree-core defect rows. It tests inequalities on restricted profile points and independently reconstructs averages. Some checked rows have zero final multiplier.

\section{The 18-job suite: Gram matrices and final sum}
\subsection{Integer Gram reconstruction}
\file{rebuild_integer_moments.py} with \texttt{--check-only} rebuilds all eight integer Gram blocks by explicit overlap counting and compares them with \file{moment_integer_verified.npz}. It writes an audit report but does not replace the checked matrix file in this mode.

\subsection{Direct separation replay}
\file{verify_exact_separation.py} with \texttt{--replay} checks multiplier signs and unique indices, verifies named file hashes, recomputes square rows with a checked overflow bound, and accumulates the exact floor lower bounds. It explicitly separates probability normalization from homogeneous equalities.

\subsection{Arbitrary-precision replay}
\file{replay_global_certificate.py} recomputes the square contractions with Python integers and reproduces the final sum by arbitrary-precision arithmetic. This avoids reliance exclusively on fixed-width array contractions for the critical numerical part.

\subsection{A further global auditor}
\file{audit_global_exact_certificate.py} provides another exact replay and coefficient consistency check. Where fixed-width contractions are used, a sufficient no-overflow bound is checked first. The final accumulated separation is exact.

These four jobs, the nine global coefficient jobs, and the five local/catalogue jobs make the $18$ jobs in \file{verify_all.py}. The package launcher also offers the source-linkage audit, exhaustive extraction replay, finite-estimator checks, and the optional strengthening checks described above.

\paragraph{Scope of independence.}
The auditors use different enumerations for important formulas, but share some data, conventions, and helper functions. Here an independent check means a distinct implementation of the specified calculation. Reimplementing the displayed formulas in another language and comparing exact outputs would provide another useful level of review.

\section{Writing a verifier from this specification}
A fresh implementation can be divided into five components. This keeps the trusted mathematical code understandable even though it processes many files.

First, decode graph6 into symmetric zero-diagonal adjacency matrices and recompute profiles. Preserve the difference between graph-record counts and distinct-profile counts. Gzip compression affects storage only.

Second, generate the local variables and equations from the profile sets. Use a declared order or named coordinates with an explicit translation to certificate positions. Check all degree and edge ranges before building the matrix. Missing input must cause an error.

Third, implement the rational certificate kernel:
\begin{verbatim}
for each required claim:
    M, b, active = construct_model(claim.model)
    c = construct_objective(claim)
    y = parse_rationals(certificate.dual)
    assert c == parse_rationals(certificate.objective)
    for j in active:
        assert c[j] - sum(M[i,j]*y[i] for i) >= 0
    lower = sum(y[i]*b[i] for i)
    assert lower == certificate.exact_lower_bound
    assert lower > claim.rounding_threshold
\end{verbatim}
Use strict thresholds appropriate to the integer conclusion, not rounded decimal values. Equality rows may receive signed multipliers, whereas nonnegative slack coefficients must have the stated sign.

Fourth, enumerate rooted flag placements on all $979$ graph types and reconstruct each used global coefficient by finite sampling. Validate the underlying inequality independently of its lift. This links each reconstructed row to the counting statement that gives its sign.

Fifth, enumerate Gram extension pairs with overlaps, contract integer vectors, and form the final rational sum or conservative floor lower bound. Check positivity for all columns and apply normalization only in the final contradiction.

These components use the supplied rational multipliers. Graph canonicalization, hull calculation, and sparse storage can be implemented differently, provided the resulting coefficients agree exactly after matching graph types, variables, and rows.

\section{Small arithmetic checks and common errors}
\paragraph{Complement conventions.}
For $K_3$, $(n,e,t,q)=(3,3,1,2)$. Equations~\eqref{specification:eq:comp1}--\eqref{specification:eq:comp3} give the empty graph profile $(3,0,0,0)$. For $P_3$, the profile $(3,2,0,1)$ becomes $(3,1,0,0)$, as expected.

\paragraph{Four-vertex paths.}
For $P_4$, $e=3,t=0,w=q=2$. Equation~\eqref{specification:eq:T} gives triple counts $(0,2,2,0)$. In \eqref{specification:eq:path}, the middle edge contributes $1$ and the two end edges contribute zero. For a triangle, the sum over middle edges gives $3$, and the correction $3t=3$ removes every coincident outer-endpoint choice.

\paragraph{A degree-square coefficient.}
If a five-vertex flag has $r_0=2$ and the actual degree is $38$, the exterior neighbor count is $m_{\rm ext}=36$. The expected value of \eqref{specification:eq:square-est} is
\[
2\cdot36\cdot35+2(4-76)36+2(-36)(-37)=0.
\]
This checks both the linear coefficient and the constant in a concrete case.

\paragraph{Two and three exterior vertices.}
A specified edge outside a five-vertex flag appears with probability $1/\binom{79}{2}$. The factor $79\cdot78$ estimates twice its count. A specified triple outside a four-vertex flag appears with probability $1/\binom{80}{3}$; the factor $80\cdot79\cdot78$ estimates six times its count.

\paragraph{Negative floor division.}
For a term $-1/3$ and scale $10$, use $\lfloor-10/3\rfloor=-4$, giving a valid lower bound $-0.4$. Truncating toward zero gives $-0.3$, which is larger than $-1/3$ and therefore invalid as a lower bound.

\paragraph{Signs and colors.}
Every global inequality row uses nonpositive average. A nonnegative square is therefore negated. A support $e\geq ac+b$ becomes $ac+b-e\leq0$. For blue cells, all internal edge-based statistics refer to the complement consistently, while a root's degree parameter in a neighborhood facet still refers to $X$.

\paragraph{Order and degree.}
A nonneighborhood $B_v$ has order $83-d_v$. Substituting that order into a coefficient intended for $d_v$ changes the inequality. A root that is excluded from a cell remains excluded even if its diagonal adjacency entry happens to satisfy the cell's zero-one tests.

\section{What a successful reproduction establishes}
A complete reproduction establishes a chain of different statements:
\begin{enumerate}
\item The external Ramsey bounds and catalogue completeness assumptions are precisely identified.
\item Supplied graph and profile data are linked by counts, hashes, and the specified extraction checks.
\item Recursive polygons contain all justified profiles, with no omitted degree or edge class.
\item Every required local dual has the correct exact residual signs and strict threshold.
\item Every used global row is the correct finite average of a valid underlying inequality or identity.
\item The seven-vertex type set is complete and consistently ordered.
\item Every square row comes from the exact finite Gram identity with all overlaps.
\item The final signed and nonnegative multipliers produce a strictly positive coefficient on every allowed type.
\end{enumerate}
The resulting contradiction proves $R(5,6)\leq84$ by exact rational arithmetic.

The argument combines the stated external catalogue and Ramsey results, the mathematical derivations of the counting identities, and the exact finite checks performed by the supplied programs. Reproduction relies on the correctness of the software and arithmetic environment used for those checks.

The separate strengthening that every $X\in\R(5,5,45)$ has $e(X)\geq462$ discussed in the manuscript is not needed for the certificate. The proof above uses the bound $460$. Its optional audit verifies that separate statement. The coefficients of the final model are those specified above.

The package supports four levels of review: understanding the reasoning, checking a worked local example, replaying supplied programs, and independently reconstructing the calculations from this specification. The mathematical derivations establish the validity of the rows; the executable checks verify their numerical coefficients and weighted sums.

\begin{thebibliography}{III.99}
\bibitem[III.1]{specification:survey}S.~P.~Radziszowski, \emph{Small Ramsey Numbers}, Electronic Journal of Combinatorics, Dynamic Survey DS1, revision 18, 24 April 2026. \url{https://doi.org/10.37236/21}. See Table~Ib for $R(4,6)\leq40$.
\bibitem[III.2]{specification: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}. See Theorem~1.1 and Appendix~A, Table~1.
\bibitem[III.3]{specification: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[III.4]{specification:data}B.~D.~McKay, \emph{Ramsey Graphs}, catalogue collection and descriptions. \url{https://users.cecs.anu.edu.au/~bdm/data/ramsey.html}.
\bibitem[III.5]{specification: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. \url{https://doi.org/10.37236/2824}. Theorem~2. Author manuscript: \url{https://www.cs.rit.edu/~spr/PUBL/e3k12.pdf}.
\bibitem[III.6]{specification:supp}Electronic verification supplement to the accompanying manuscript (2026). Local mathematical input is documented in \file{LOCAL_CERTIFICATES.txt}; the 18-job verification driver is \file{verify_all.py}; the packaged launcher is \file{verify_package.py}; the final weighted sum is \file{exact_separation_certificate.json}. The package README specifies installation and the archived layout.
\end{thebibliography}