\section{Exact verification and accompanying files}
\label{sec:reproducibility}
The computer-assisted claims are finite algebraic inequalities. Their
inputs are the matching comparisons and constructions proved in the
preceding sections. The verification programs reconstruct the relevant
quadratic forms and check the signs, identities, and parameter ranges
with integer and rational arithmetic. Numerical optimization is not
needed to run them. This use of exact certificates after numerical
exploration is related to the rational certification methods discussed
by Peyrl and Parrilo~\cite{PP}.

\subsection{Contents and commands}
The source archive contains \texttt{main.tex}, the included section
files, and an \path{anc/} directory containing all verification
programs and data. The bibliography is in \texttt{references.tex};
there is no external bibliography database or downloaded data set.
The root file \texttt{main.tex} compiles with PDFLaTeX. For a local
compilation, run it until the log no longer requests another pass:
\begin{verbatim}
pdflatex -interaction=nonstopmode -halt-on-error main.tex
pdflatex -interaction=nonstopmode -halt-on-error main.tex
pdflatex -interaction=nonstopmode -halt-on-error main.tex
\end{verbatim}
The source uses the standard packages \texttt{geometry},
\texttt{amsmath}, \texttt{amssymb}, \texttt{amsthm}, \texttt{mathtools},
\texttt{booktabs}, \texttt{microtype}, \texttt{xurl}, and \texttt{hyperref}.

For verification, use Python 3.9 or later with its standard library.
No additional Python packages, numerical solvers, network access, or
external research directories are required. From the root of the
extracted source archive, run
\begin{verbatim}
python3 anc/check_package.py
python3 anc/verify_all.py
\end{verbatim}
The first command checks the file inventory and SHA-256 hashes. The
second runs every mathematical certificate. Successful completion
has exit status zero and ends with
\begin{verbatim}
PASS: all exact certificates.
\end{verbatim}
Run Python normally: its \texttt{-O} option disables the assertions
used by the checkers and must not be used. The driver rejects such
an invocation. To run an individual checker, use the paths listed
below relative to \path{anc/}. The working directory does not
matter because paths to data are resolved relative to each script.

The programs print progress as each group of certificates passes.
They may take several minutes, particularly for the matching-flow
and stability calculations. Three deterministic summaries are
regenerated: \path{general-certificate/verified-general-table.json},
\path{general-certificate/path-budget-certificates.json}, and
\path{lower-certificate/neutral-pair-exact-results.json}. These are
included in the archive so that their contents can also be inspected
without running Python.

\subsection{What each computation verifies}
\begin{enumerate}
\item \path{verify_global.py} proves the algebraic part of the
four-label upper bound. It reconstructs the quadratic comparisons
from Sections~\ref{sec:neutral-core}--\ref{sec:certificates}, checks
the signs of their rational weights, verifies the matrix
factorizations, and checks that the parameter subregions cover the
entire required domain. The JSON files beside it contain the weights
and subdivisions. The helper modules in the same directory are
included in full.

\item \path{general-certificate/verify_general.py} checks the
explicit general-label upper bounds, the rational choices giving
the numerical table in the introduction, and the finite quadratic
formula in Theorem~\ref{thm:general-full-budget}. It also brackets
the optimizing weight for the fixed path-length choice. The
alternating-path counting arguments and the asymptotic expansion
are given in the text.

\item \path{lower-certificate/verify_algebraic.py} checks the
sextic polynomial, root isolation, mass normalization and positivity,
and the identities for the three matching flows in
Section~\ref{sec:lower-exact}. It then invokes
\path{lower-certificate/verify_flow_bound.py}, which enumerates the feasible
vertices of the reduced matching-flow polytope and checks all their
bilinear pairings. The latter step bounds every feasible flow, not
only the vertices. The separate script
\path{lower-certificate/verify_elimination_independent.py} checks the elimination
that produces the algebraic value.

\item \path{lower-certificate/verify_atom_stability.py},
\path{lower-certificate/check_neutral_pairs_exact.py}, and
\path{lower-certificate/verify_stationarity.py} check the finite profile and
matrix calculations used in Appendix~\ref{sec:lower-local-stability}.
The appendix states precisely which perturbations are covered.
\end{enumerate}

The general lower bound of Theorem~\ref{thm:general-lower} and its
weight-optimality statement have complete elementary proofs in
Section~\ref{sec:general-lower}; neither depends on a computation.

The verification programs check the finite algebra arising from the
proofs. The mathematical justification that each inequality applies
to actual matchings is provided in the preceding sections. Classical
matching theorems and the alternating-path bound of~\cite{CP} are
stated where used and cited to the literature. In particular,
computer verification is not being used to infer a universal
combinatorial assertion from a finite sample of graphs.