\documentclass[11pt]{article}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage{lmodern}
\usepackage[margin=1.02in]{geometry}
\usepackage{amsmath,amssymb,amsthm,mathtools}
\usepackage{booktabs,array,graphicx,microtype,xcolor,longtable}
\usepackage[hidelinks]{hyperref}
\hypersetup{pdftitle={The covering number C(13,7,4) is 30},pdfauthor={John Tripodo},pdfsubject={Covering designs and exact finite verification}}
\setlength{\parskip}{2.3pt}
\setlength{\parindent}{15pt}
\newcommand{\bin}[2]{\binom{#1}{#2}}
\newcommand{\coverfam}{\mathcal F}
\newcommand{\cat}{\mathcal C}
\newcommand{\dom}{\mathcal D}
\newcommand{\penc}{\mathcal P}
\newcommand{\XX}{X}
\newcommand{\YY}{Y}
\newcommand{\Star}{\operatorname{St}}
\newcommand{\sig}{\operatorname{sig}}
\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{corollary}[theorem]{Corollary}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}
\definecolor{navy}{RGB}{24,46,67}
\title{\vspace{-1.3em}\bfseries The covering number $C(13,7,4)$ is $30$\\[0.32em]
\large\normalfont A classification-assisted exact proof}
\author{John Tripodo\\\small ORCID: \href{https://orcid.org/0009-0006-9180-4953}{0009-0006-9180-4953}}
\date{29 October 2026}
\begin{document}
\maketitle
\vspace{-1.3em}
\begin{abstract}\noindent
We prove that $C(13,7,4)=30$, using the classification of minimum
$(12,6,3)$ coverings by Gordon, Patashnik, Petro and Taylor.
A hypothetical $29$-block cover has at least five points lying in exactly
$15$ blocks. The link at one of these points leaves only $14$ blocks
outside it. The other four points force complete families of outside
blocks whose overlaps must agree. An exhaustive computation shows that
every compatible choice requires $15$ outside blocks, giving a
contradiction. The known $30$-block construction is therefore optimal.
We give reproducible exact computations and a public Lean formalization
of a second argument for the finite obstruction. The Lean theorem
states the published minimum bound and classification as explicit
hypotheses; it does not reprove those results.
\end{abstract}
\noindent\textbf{Keywords:} covering designs; covering numbers; finite classification;
exact enumeration; computational proof; Lean formalization.
\medskip

\section{The result and its context}
For positive integers $v\geq k\geq t$, a $(v,k,t)$ \emph{covering} is a
family $\coverfam\subseteq\bin{X}{k}$, where $|X|=v$, such that every
$T\in\bin{X}{t}$ is contained in some $B\in\coverfam$. Its minimum cardinality
is the covering number $C(v,k,t)$. The problem considered here asks for the
minimum number of seven-element blocks on thirteen points needed to cover
every four-element subset.

\begin{theorem}[Main result]\label{thm:main}
\[
\boxed{C(13,7,4)=30.}
\]
\end{theorem}

An explicit construction supplies the upper bound $30$; the contribution
is the global exclusion of $29$ blocks. Prior tabulations gave the interval
$28\leq C(13,7,4)\leq30$ \cite{LJCR}, and a separately published,
formally checked elimination of one minimum-link type does not resolve
all $68$ types \cite{Dwares}. Krug recently determined the different covering number
$C(12,6,4)=41$ \cite{Krug}.

The one external mathematical ingredient is the work of Gordon,
Patashnik, Petro and Taylor \cite{GPPT}: their Theorem 4.4 proves
$C(12,6,3)=15$, and their Theorem 5.9 classifies the minimum
$(12,6,3)$ covers by a Figure~1 completion family and a single
exceptional Figure~6 cover. Their $68$ nonisomorphic minimum covers
are \emph{input}, not an original classification claimed here.
The proof below explains why that classification is enough and
isolates the precise role of the computation.

\paragraph{Outline of the proof.}
Every point of a hypothetical $29$-block covering occurs in at least
$15$ blocks, and there are only eight degree units above that baseline;
hence at least five points have degree exactly $15$. Root at one such
point. Its $15$ incident blocks determine a classified link, leaving
just $14$ blocks not containing the root. Each of four further minimum
points forces a full set of outside blocks. The classification supplies
exhaustive finite domains for those sets. The computation proves that
four mutually compatible choices always need at least $15$ outside
blocks. This is the contradiction.

\section{Why five minimum points are unavoidable}
Write $X=Y\cup\{\infty\}$ with $|Y|=12$ once a root is chosen.
For any point $x\in X$, define its degree and link by
\[
 d_\coverfam(x):=|\{B\in\coverfam:x\in B\}|,\qquad
 L_x(\coverfam):=\{B\setminus\{x\}:B\in\coverfam,\ x\in B\}.
\]
If $\coverfam$ covers every four-set of $X$, then $L_x(\coverfam)$ covers every
three-set of $X\setminus\{x\}$. The cited minimum-cover theorem
therefore implies $d_\coverfam(x)\geq15$ for every $x$.

\begin{lemma}[Five minimum points]\label{lem:five}
If a $(13,7,4)$ covering has exactly $29$ distinct blocks, at least
five points have degree $15$.
\end{lemma}
\begin{proof}
Double-count incidences between points and blocks:
\[
 \sum_{x\in X}d_\coverfam(x)=7|\coverfam|=7\cdot29=203
 =13\cdot15+8.
\]
Each degree exceeds $15$ by a nonnegative integer. At most eight
points can have positive excess, leaving at least five of degree $15$.
\end{proof}

Choose such a point $\infty$. The root link
$L:=L_\infty(\coverfam)$ has exactly $15$ blocks and is one of the
published minimum $(12,6,3)$ covers up to relabelling. The
\emph{outside family}
\[
 \coverfam^\circ:=\{B\in\coverfam:\infty\notin B\}
\]
contains exactly $29-15=14$ blocks, all seven-subsets of $Y$.
Choose four other degree-$15$ points $Q\subseteq Y$,
$|Q|=4$. We now show how they constrain $\coverfam^\circ$.

\paragraph{Why use several minimum points?}
A single minimum point gives a $15$-block link but leaves a difficult
extension problem on the other twelve points. Every additional
minimum point specifies \emph{all} outside blocks through that point.
Consequently these local specifications must agree on every shared
block. Their union gives a lower bound on the number of outside
blocks. The useful obstruction here is the gap $15>14$ obtained from
four such specifications. It is an obstruction to compatible local
links, not a new construction of the upper-bound cover.

\section{From classified links to complete outside pencils}
Let $\cat$ be a set of representatives of the $68$ published
isomorphism classes of minimum $(12,6,3)$ coverings, each with
$15$ distinct six-subsets of a labelled twelve-element set.
Fix a labelled root link $L\in\cat$. For $q\in Y$,
the root-containing part of the $q$-link is already fixed:
\begin{equation}\label{eq:star}
 S_L(q):=\big\{\{\infty\}\cup(A\setminus\{q\}):
                 A\in L,\ q\in A\big\}.
\end{equation}
This is a family of six-subsets of $X\setminus\{q\}$.

Take a classified source link $K\in\cat$ on a twelve-point set $W$,
a source point $c\in W$, and a bijection
$\phi:W\to X\setminus\{q\}$ such that $\phi(c)=\infty$ and
\begin{equation}\label{eq:starmatch}
 \big\{\phi(A):A\in K,\ c\in A\big\}=S_L(q).
\end{equation}
Define the associated \emph{complete outside pencil}
\begin{equation}\label{eq:pencil}
 P(L,q;K,c,\phi):=
 \big\{\{q\}\cup\phi(A): A\in K,\ c\notin A\big\}
 \subseteq\bin{Y}{7}.
\end{equation}
The domain $D_L(q)$ consists of all pencils in
\eqref{eq:pencil} over all $K,c,\phi$ satisfying
\eqref{eq:starmatch}. In computation we may first prune $c$ by the
necessary equality $d_K(c)=d_L(q)$, but the definition of the
domain itself is unrestricted.

\begin{lemma}[Domain completeness]\label{lem:domain}
Suppose $\coverfam$ is a $29$-block $(13,7,4)$ covering with root link
$L$ and $d_\coverfam(q)=15$. Then
\[
 P_q:=\{B\in\coverfam^\circ:q\in B\}\in D_L(q).
\]
In particular, $P_q$ records \emph{every} outside block through $q$,
not an arbitrarily chosen subfamily.
\end{lemma}
\begin{proof}
The full link $L_q(\coverfam)$ is a minimum $(12,6,3)$ cover.
The cited classification gives a source $K\in\cat$ and a bijection
from its twelve points onto $X\setminus\{q\}$ carrying $K$ to
$L_q(\coverfam)$. If $c$ maps to $\infty$, the blocks of $K$ containing
$c$ map precisely to the known star $S_L(q)$.
The remaining blocks of $K$ are exactly the blocks of the $q$-link
that avoid $\infty$. Reattaching $q$ to their images gives
\eqref{eq:pencil}, which is exactly $P_q$.
\end{proof}

The enumeration searches all bijections on the remaining eleven
source points that satisfy the star equality. This is needed for
Lemma~\ref{lem:domain}: searching only a chosen automorphism subgroup
would not suffice.

\paragraph{Equivariance of domain reuse.}
The implementations may reuse a domain when two known stars are
isomorphic. This does not require choosing every isomorphism between
the target stars. If $g$ is one such isomorphism, extend it by mapping
the distinguished target point to the new distinguished target point.
Composition with $g$ bijects every classified source embedding for the
first star with an embedding for the second, with inverse composition
by $g^{-1}$. Applying this bijection to all complete pencils proves
that the transported domain is the entire second domain. Equality of
coarse invariants alone is never used to authorize transport.

\section{Agreement conditions and the finite obstruction}
For distinct $q,r\in Q$ and pencils $P\in D_L(q)$,
$R\in D_L(r)$, call $(P,R)$ \emph{compatible} when
\begin{equation}\label{eq:pair}
 \{B\in P:r\in B\}=\{B\in R:q\in B\}.
\end{equation}
The two sides are the outside seven-blocks through both points.
Thus the actual pencils $P_q,P_r$ supplied by Lemma~\ref{lem:domain}
are pairwise compatible. Also, because each $P_q\subseteq\coverfam^\circ$,
\begin{equation}\label{eq:budget}
 \left|\bigcup_{q\in Q}P_q\right|\leq|\coverfam^\circ|=14.
\end{equation}
The central finite statement is the following.

\begin{proposition}[Exhaustive four-pencil obstruction]
\label{prop:finite}
For every $L\in\cat$ and every $Q\in\bin{Y}{4}$, there are
no choices $P_q\in D_L(q)$, $q\in Q$, which satisfy every pair
compatibility equation \eqref{eq:pair} and the union budget
\eqref{eq:budget}.
\end{proposition}

\begin{proof}[Exact computer-assisted verification]
The exhaustive input space contains
$68\bin{12}{4}=68\cdot495=33{,}660$ \emph{labelled} pairs $(L,Q)$.
No orbit reduction of the $Q$-sets is needed for this claim.

The computation first rejects an input if some pair of selected points
has no compatible pair of possible pencils. It then enforces arc
consistency: any pencil with no compatible partner in another
selected domain is removed, and this rule repeats until stable.
These are sound necessary filters. To see the latter formally,
consider a putative compatible four-pencil choice. Initially each
actual choice lies in its full domain. If all four remain after a
round, each is a compatible partner for each of the other three,
so none can be removed in the next round. By induction a genuine
compatible choice is never eliminated.

The recorded exact census is:
\begin{table}[ht]
\centering\small
\begin{tabular}{@{}p{0.59\linewidth}r@{}}
\toprule
Exhaustive stage & Labelled root/fourset inputs \\
\midrule
A pair has no compatible pencil choices & 31,263\\
Additional inputs closed by sound arc consistency & 2,355\\
Inputs retained for the final four-way join & 42\\
\midrule
Total: $68\bin{12}{4}$ & 33,660\\
\bottomrule
\end{tabular}
\caption{Partition of all labelled root/four-set inputs in the finite search.}\label{tab:filter}
\end{table}

For each of the $42$ residual inputs, a separately written routine
constructs all six pair-compatibility relations and enumerates every
four-pencil tuple satisfying them. This final routine
\emph{does not prune by union size}; it computes the literal union
after joining. Its result is:
\begin{table}[ht]
\centering\small
\begin{tabular}{@{}lrrr@{}}
\toprule
Root type & Residual inputs & Compatible tuples per input
 & Total tuples \\
\midrule
Figure 1 completion types & 37 & 216 & 7,992\\
Exceptional Figure 6 type & 5 & 54,432 & 272,160\\
\midrule
Total & 42 & & 280,152\\
\bottomrule
\end{tabular}
\caption{Independent unpruned join. Every one of the $280{,}152$
compatible tuples has a union of exactly $15$ distinct outside blocks.}
\label{tab:join}
\end{table}

The reconstruction of domains uses the $68$-link catalog,
with an independent route rebuilding all $28^3=21{,}952$ literal
Figure-1 completions from the published core and short blocks,
recovering $67$ completion classes under the construction action,
and separately including the exceptional Figure-6 link.
Both implementations reconstruct $68\cdot12=816$ root/point domains,
agree on the canonical digest of every domain, and obtain
Tables~\ref{tab:filter} and \ref{tab:join}.
Python ordinary and optimized executions agree; a distinct C++
implementation reproduced the decisive totals. The source, manifests,
independent joins and build receipts are itemized in
Appendix~\ref{app:reproduce}. No floating-point optimization
status, solver timeout or unverified infeasibility declaration enters
the conclusion. Every residual compatible union has $15>14$ blocks,
so \eqref{eq:budget} is impossible.
\end{proof}

\section{Proof of optimality}
\begin{proof}[Proof of Theorem~\ref{thm:main}]
Suppose a covering has at most $29$ blocks. Removing duplicate blocks,
if any, preserves coverage; we can pad with previously unused
seven-subsets to obtain a covering with exactly $29$ distinct blocks,
since $\bin{13}{7}=1716$.

By Lemma~\ref{lem:five}, choose five degree-$15$ points. Relabel one
as $\infty$ and normalize its minimum link to a representative
$L\in\cat$; this induces a relabelling of the twelve ordinary points.
Choose the other four minimum points as $Q$.
Lemma~\ref{lem:domain} supplies one complete outside pencil
$P_q\in D_L(q)$ for each $q\in Q$. All six compatibility equations
hold, and the pencils jointly occupy at most the $14$ outside blocks.
This contradicts Proposition~\ref{prop:finite}. Therefore
$C(13,7,4)\ge30$. The explicit $30$-block covering in
Appendix~\ref{app:cover}, checked against every one of the
$\bin{13}{4}=715$ four-subsets, supplies $C(13,7,4)\le30$.
\end{proof}

\section{A public Lean proof relative to the published classification}
\label{sec:lean}
The repository accompanying this paper contains the complete local
source closure for a second proof of the lower bound. This proof
works directly with actual covering families. It does not use the
Python verifier as an oracle and does not merely import a Boolean
claim that the Python search succeeded.

\subsection{The mathematical interface}
The ground type \texttt{C13.Point} is \texttt{Fin 13}. A family is
a finite set of finite subsets. The predicate
\texttt{IsCoverOn U F k t} requires every block of $F$ to be a
$k$-subset of $U$ and every $t$-subset of $U$ to lie in a block.
Thus the formal conclusion concerns the same simple covering
number as Theorem~\ref{thm:main}; duplicate blocks are not counted.

The principal endpoint is
\begin{quote}\small
\texttt{C13.Global.exact30\_after\_published\_results}.
\end{quote}
It proves the following implication, expressed here without Lean
syntax:
\[
\begin{gathered}
\mathsf{PublishedMinimumBound}\ \wedge\
\mathsf{PublishedClassification1995}\\
\Longrightarrow\quad
\left(\exists F\text{ a $(13,7,4)$ cover},\ |F|=30\right)
\ \wedge\
\left(\forall F\text{ a $(13,7,4)$ cover},\ |F|\ge30\right).
\end{gathered}
\]
The first hypothesis is the lower-bound part of the published
Theorem~4.4. The second is the relabelling coverage supplied by
Theorem~5.9 together with the minimum value from Theorem~4.4.
They are ordinary theorem hypotheses, not additional Lean axioms.
They are nevertheless substantive mathematical assumptions. An
axiom audit cannot discharge an explicit hypothesis.

The classification predicate is stated using the literal Figure~1
completion family and Figure~6. The source-to-catalog theorem
\texttt{catalog\_covers\_all\_raw\_sources} then covers every one
of the $28^3=21{,}952$ completion triples and the exceptional source.
The needed direction is coverage by the catalog. Pairwise
nonisomorphism of catalog entries under every permutation is not
needed for the lower bound.

\subsection{The actual-cover certificate argument}
For a catalog link $K$ and a four-set $Q$, the predicate
\texttt{ActualObstruction K Q} excludes an actual global cover
whose root link is $K$, whose points in $Q$ have degree $15$, and
whose outside family has at most $14$ blocks. The definition
retains the classification hypothesis. It is not the stronger
statement that every abstract assignment of local pencils is
impossible without the global covering constraints.

The formal census uses the same $33{,}660$ labelled positions, with
the following distinct partition:
\begin{center}
\begin{tabular}{@{}lr@{}}
\toprule
Formal exclusion mechanism & Positions\\
\midrule
Empty-support certificates & $31{,}762$\\
Exact integer-dual certificates and checked transports & $1{,}893$\\
Exceptional Figure-6 predecessor certificates & $5$\\
\midrule
Total & $33{,}660$\\
\bottomrule
\end{tabular}
\end{center}
This is not the Python partition of Table~\ref{tab:filter}.
The integer-dual branch contains $964$ representative positions
and $929$ positions reached by checked root automorphisms.
The empty-support branch uses $3{,}636$ certificates, some of
which exclude more than one four-set.

The formal argument includes the full $792=\binom{12}{7}$ outside
block universe, complete-coverer masks, and all $816=68\cdot12$
root/point alphabet bindings. A block containing none of the
selected points is handled separately; it cannot be silently
discarded from the outside-block budget. Row-validity theorems
derive the covering and incidence constraints from genuine covers
before a dual inequality is used. The checked census and
\texttt{all\_catalog\_foursets} feed into
\texttt{no\_cover29}; the final theorem combines this with padding
and the unconditional $30$-block witness.

\subsection{Paper-to-Lean correspondence}
The following modules are under \path{lean/} in the public repository.
The correspondence is semantic; it does not assert that the Lean
certificate search follows the Python search instruction for instruction.
\begin{center}\small
\begin{tabular}{@{}p{0.42\linewidth}p{0.53\linewidth}@{}}
\toprule
Mathematical step & Formal source\\
\midrule
Links, degrees, incidence sum, five minimum points, padding &
\path{C13Covering/Reduction.lean}\\[2pt]
Literal historical classification predicate &
\path{C13Covering/SourceFigures.lean}\\[2pt]
Coverage of all raw classified sources by the catalog &
\path{C13Covering/OrbitAllSources.lean}\\[2pt]
Complete semantic alphabets and unrestricted star transport &
\path{C13RawStarRecovery/StarTranslation.lean}\\[2pt]
Actual-cover obstruction, covering of all four-sets, transport &
\path{C13Global/CensusCore.lean}\\[2pt]
Validity of exact covering/degree rows and dual implications &
\path{C13Global/RowValidity.lean},
\path{C13Global/DualBridge.lean}\\[2pt]
All $68$ roots; no $29$-cover; exact-covering endpoint &
\path{C13Global/Final.lean}\\[2pt]
Unconditional $30$-block witness and model transport &
\path{C13/Known30.lean},
\path{C13Covering/PositiveBridge.lean}\\
\bottomrule
\end{tabular}
\end{center}

An additional endpoint,
\texttt{exact30\_after\_published\_classification}, derives the
minimum-bound parameter from the stated all-size-$15$
classification predicate and checked private-triple irredundancy
of every catalog block. This is a valid implication within that
formal interface. It is not a claim that the historical proof of
Theorem~5.9 is independent of Theorem~4.4, nor a new proof of the
1995 classification.

\section{Reproducibility, assurance and limitations}\label{sec:release}
The paper, Lean sources and verification programs are available at
\begin{center}\small
\url{https://github.com/jjtripodo-lgtm/c13-covering-number}.
\end{center}
The formalization cited here is frozen at public commit
\begin{center}\small\ttfamily
254ee82fdbc215ad73f732f807a83d69be7c1e22
\end{center}
The
\href{https://github.com/jjtripodo-lgtm/c13-covering-number/blob/254ee82fdbc215ad73f732f807a83d69be7c1e22/lean/C13Global/Final.lean}{main theorem}
is directly accessible. The repository also provides a paper-to-proof map,
pinned dependencies, and commands for reproducing the checks
(Appendix~\ref{app:reproduce}). No private repository is required.

The Python computations were rerun for this edition in both ordinary and
optimized modes, including the independent domain reconstruction and
unpruned join. They reproduce Tables~\ref{tab:filter} and~\ref{tab:join}.
The native C++ implementation agrees. The known upper-bound construction
passes all $715$ coverage tests; malformed inputs and small brute-force
comparisons test the verification routines.

For Lean, the release includes $1{,}751$ unchanged local source modules,
authenticated against their original Git objects and recorded source
hashes. The preserved historical audit checked $76{,}982$ project
declarations in $1{,}750$ modules, allowing only \texttt{propext},
\texttt{Classical.choice} and \texttt{Quot.sound}, with no unsafe project
declarations. A later recorded check recompiled the endpoint and ran
negative controls using authenticated cached dependencies. These records
are not a fresh build of the new public package: that build has not been
run in this release environment. The distinction is recorded alongside
the source and reproduction instructions.

Both arguments rely on the published minimum bound and classification.
The literal input families are printed in Appendix~\ref{app:literal};
the repository preserves the source-transcription audit. The theorem
wording was checked against the author-posted preprint for this edition,
but a fresh visual comparison of its figures was not completed. This
result determines one covering number and does not classify all optimal
$30$-block covers.

\begingroup\interlinepenalty=10000
\section*{Acknowledgments and use of AI}
The author thanks the authors of the published classification and the
maintainers of the La Jolla Covering Repository for making their work
available. Anthropic Claude and OpenAI ChatGPT/Codex were used extensively
in developing the arguments, programs, formalization, and manuscript.
The text is primarily AI-generated. John Tripodo directed the project
and is responsible for the submitted work. No part of the contribution
is attested as having been checked and understood by a human, and no
independent human referee review is claimed. The computational checks
and recorded Lean audits described above are separate forms of evidence.
\endgroup

\clearpage
\appendix
\section[An explicit optimal 30-block covering]{An explicit optimal $30$-block covering}\label{app:cover}
The blocks below are the published Nurmela--\"Osterg\r{a}rd
upper-bound construction tabulated by the La Jolla Covering Repository
\cite{LJCR}, not a new construction claimed here. They are seven-subsets
of $\{1,2,\ldots,13\}$. Each four-subset is contained in at least one
of the $30$ blocks. The
accompanying independent standard-library checker enumerates all
$715$ possible four-subsets, verifies distinctness and confirms
$1{,}050=30\bin{7}{4}$ total block/fourset incidences.
\begin{center}
\begingroup\footnotesize\setlength{\tabcolsep}{6pt}
\begin{tabular}{@{}ll@{}}
\toprule
Block & Block\\
\midrule
$\{1,2,5,6,7,8,9\}$ & $\{1,3,4,5,6,8,10\}$\\
$\{2,3,6,7,8,9,10\}$ & $\{2,3,4,5,8,9,11\}$\\
$\{1,3,5,7,8,10,11\}$ & $\{1,2,4,8,9,10,11\}$\\
$\{1,2,3,5,7,10,12\}$ & $\{1,3,4,5,9,10,12\}$\\
$\{1,2,4,5,6,11,12\}$ & $\{1,3,6,7,9,11,12\}$\\
$\{2,6,7,8,9,11,12\}$ & $\{4,6,7,8,9,11,12\}$\\
$\{2,3,4,6,10,11,12\}$ & $\{5,6,7,9,10,11,12\}$\\
$\{3,4,5,6,7,9,13\}$ & $\{1,2,3,5,6,10,13\}$\\
$\{1,4,6,7,9,10,13\}$ & $\{1,2,3,4,7,11,13\}$\\
$\{2,4,7,8,9,11,13\}$ & $\{2,4,5,7,10,11,13\}$\\
$\{1,3,5,9,10,11,13\}$ & $\{1,4,5,7,8,12,13\}$\\
$\{2,4,6,7,8,12,13\}$ & $\{1,2,3,8,9,12,13\}$\\
$\{3,4,7,8,10,12,13\}$ & $\{2,5,8,9,10,12,13\}$\\
$\{3,5,6,8,11,12,13\}$ & $\{2,4,6,9,11,12,13\}$\\
$\{6,7,8,9,11,12,13\}$ & $\{1,6,8,10,11,12,13\}$\\
\bottomrule
\end{tabular}
\endgroup
\end{center}
The example is different from the separate $30$-block cover in
\path{known30_control.json}. Both were checked independently on all $715$
four-subsets in the preparation packet.

\section{Reproducing the computations and formal proof}\label{app:reproduce}
Download the public repository linked in Section~\ref{sec:release}.
From its top-level directory, run:
\begin{verbatim}
python3 verify_release.py
python3 computation/reproduce.py
python3 computation/reproduce.py --native
\end{verbatim}
The first command checks source hashes, local Lean imports, dependency
pins and the preserved historical axiom log; it does not run Lean.
The second runs the exact Python proof, checks both ordinary and
optimized executions against frozen outputs, and runs the controls.
The optional third command adds the C++ and undefined-behaviour-sanitizer
cross-checks; it requires a C++17 compiler and OpenSSL development files.
The Python checks use only the standard library and run without network
access. Each run writes its outputs and a machine-readable receipt to
\path{computation/replay-output/}.

The lower-bound programs are \path{verify_pencils.py} and
\path{independent_raw_replay.py}; the independent unpruned join is in
\path{peer_union_join.py}. They reside in the repository's
\path{computation/source/research/horizonmath/c13_classified_pencils/}
directory. The input catalog, domain digests and expected outputs are
listed in the manifests alongside them. These identities distinguish a
reproduction of the released computation from a run on altered inputs.

For the formal proof, install the version in \path{lean/lean-toolchain}
and obtain the revision-pinned dependencies in \path{lean/lake-manifest.json}.
Then, from \path{lean/}, run:
\begin{verbatim}
lake build C13Global.Final C13Global.Statistics
lake env lean --trust=0 -j 1 -M3072 C13Global/AuditFinal.lean
\end{verbatim}
Start with no local build objects to recompile the included proof modules.
Using upstream Mathlib caches does not rebuild Mathlib itself; a complete
source rebuild must also rebuild the upstream dependencies. The original
checks used a 3~GiB per-process memory cap. Resource requirements and the
historical check boundaries are documented in \path{lean/README.md}.
The Lean package is not required to reproduce the Python proof.

\section{Literal classification input}\label{app:literal}
For transcription checking, the Figure~1 core is the following list on
$\{0,1,\ldots,9,A,B\}$, with $A=10$ and $B=11$:
\begin{center}\ttfamily\small
014589\quad 0167AB\quad 2345AB\quad 236789\\
02468A\quad 02579B\quad 13469B\quad 13578A\\
03478B\quad 03569A\quad 12479A\quad 12568B.
\end{center}
To this core add one six-set extending each of $0123$, $4567$ and
$89AB$, choosing the other two points from the complementary eight.
The program enumerates all $28^3$ choices, including choices equivalent
under relabelling. The construction group has order $576$ and gives
$67$ representative completions. For completeness of the search it is
sufficient that every literal completion is in one of these orbits;
no claim that arbitrary cover isomorphisms preserve the core is needed.

For Figure~6 the labels are $0123456789TE$, with $T=10$ and $E=11$:
\begin{center}\ttfamily\small
012345\quad 012678\quad 0129TE\quad 0378TE\quad 0456TE\\
045789\quad 034569\quad 13689E\quad 14579E\quad 14568T\\
13457T\quad 23679T\quad 24589T\quad 24567E\quad 23458E.
\end{center}
These are transcriptions of the cited classification inputs, not a new
classification proof. Source-figure comparison and the applicability of
the published classification must be checked independently of the code.

\section{Finite-verifier logic in pseudocode}\label{app:algorithm}
The following specifies the logical search performed by the exact
finite verifier, independently of implementation-level optimizations.
Full reproducibility requires the released source and input catalog.
\begin{quote}\small\ttfamily
for each root link L in the 68-link catalog:\\
\hspace*{1em}for each Q among the 495 ordinary foursets:\\
\hspace*{2em}build each complete domain D[L,q], q in Q\\
\hspace*{2em}if some pair of domains has no compatible pair: continue\\
\hspace*{2em}repeat: discard values lacking support in another domain\\
\hspace*{2em}until no change\\
\hspace*{2em}if some domain is empty: continue\\
\hspace*{2em}enumerate all four-tuples matching all six pair relations\\
\hspace*{2em}for each compatible tuple, measure its literal block union\\
\hspace*{2em}assert union cardinality exceeds 14
\end{quote}
Arc-consistency deletion is valid by the induction in the proof of
Proposition~\ref{prop:finite}. Domain construction is exhaustive by
Lemma~\ref{lem:domain}, \emph{provided} the cited published
classification is correct and fully transcribed. The final join enumerates compatible tuples directly; it uses no
external infeasibility oracle.

\begin{thebibliography}{9}
\bibitem{GPPT}
D.~M. Gordon, O.~Patashnik, J.~Petro and H.~Taylor,
\emph{Minimum $(12,6,3)$ Covers},
Ars Combinatoria \textbf{40} (1995), 161--177.
\url{https://combinatorialpress.com/ars-articles/volume-040-ars-articles/minimum-12-6-3-covers/}.

\bibitem{LJCR}
D.~M. Gordon, \emph{La Jolla Covering Repository},
$(v,k,t)=(13,7,4)$, historic upper and lower bounds.
\url{https://ljcr.dmgordon.org/cover/table.html} and
\url{https://ljcr.dmgordon.org/cover/low_tab.html}.

\bibitem{Dwares}
E.~Dwares, \emph{Formal elimination of link class 52 in the
$C(13,7,4)$ search}, public certification project (2026),
\url{https://github.com/edwares/class52-formal-certification}.
The certification concerns one class, not the full optimum.

\bibitem{Krug}
C.~Krug, \emph{The covering number $C(12,6,4)$ is 41},
preprint (2026), arXiv:2607.23766,
\url{https://arxiv.org/abs/2607.23766}.
\end{thebibliography}
\end{document}