\documentclass[
    10pt,
    a4paper,
    oneside,
    reqno
]{amsart}
\usepackage{parskip}
\usepackage{booktabs}
\usepackage{array}
\usepackage[T1]{fontenc}
\usepackage{lmodern}
\usepackage{microtype}
\usepackage{siunitx}
\usepackage{xurl}
\usepackage{needspace}
\usepackage{enumitem}
\usepackage{xcolor}
\usepackage[style=numeric, sorting=nty, maxcitenames=2, maxbibnames=99, backend=biber]{biblatex}
\addbibresource{chromatic-r12.bib}
% hyperref loads after biblatex and before caption and cleveref, which both must follow
% hyperref. Loading hyperref is what makes references, citations and URLs clickable;
% colorlinks colors the link text and draws no link boxes. The PDF string fields are
% given here in ASCII, since the title carries math.
\usepackage[colorlinks,
  pdftitle={The independence number of the generalized Johnson graph J(13,5,3)},
  pdfauthor={Mustafa Stanikzai}]{hyperref}

% Hyperlink colors
\definecolor{webbrown}{HTML}{990000}
\definecolor{RoyalBlue}{HTML}{0047AB}
\definecolor{webgreen}{HTML}{008000}

\hypersetup{
    urlcolor=webbrown,
    linkcolor=RoyalBlue,
    citecolor=webgreen
}
\usepackage{caption}
\usepackage[capitalise]{cleveref}

\raggedbottom

% amsart sets \subsection as a run-in heading (afterskip -.5em); the definition below
% makes it a block heading.
\makeatletter
\def\subsection{\@startsection{subsection}{2}%
  \z@{.5\linespacing\@plus.7\linespacing}{.5\linespacing}%
  {\normalfont\bfseries\boldmath}}
\makeatother

\newcommand{\R}{\mathbb{R}}

\theoremstyle{plain}
\newtheorem{theorem}{Theorem}[section]
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{claim}[theorem]{Claim}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{question}[theorem]{Question}
\crefname{claim}{Claim}{Claims}
\crefname{question}{Question}{Questions}

% The optional argument is the running head; the PDF /Title string in the hyperref
% options must be edited whenever the full title changes.
\title[The independence number of $J(13,5,3)$]{The independence number of the
generalized Johnson graph {\boldmath$J(13,5,3)$}}
\author{Mustafa Stanikzai}
\address{Independent researcher}
\email{m.st87nk@gmail.com}
\date{November 11, 2026}
\subjclass[2020]{05C15, 05C69, 52C10, 05E30, 68V05}
\keywords{Chromatic number of Euclidean space, unit-distance graph, generalized
Johnson graph, independence number, maximum clique, proof logging}

\begin{document}

\begin{abstract}
Let $J(13,5,3)$ be the graph on the 5-element subsets of a 13-element set, two subsets
being adjacent when they share exactly 3 elements. We prove that $\alpha(J(13,5,3)) = 33$.
The graph is an explicit unit-distance graph in $\R^{12}$, so
$\chi(\R^{12}) \ge \lceil 1287/33 \rceil = 39$; earlier bounds from explicit finite
graphs give at most 38. A recent preprint of Davies gives much larger bounds, none from
an explicit finite graph. An explicit independent set gives $\alpha \ge 33$. For the
upper bound, a symmetry reduction splits the problem into 200 clique subproblems, and a
certifying solver refutes each one with a proof log that the checker VeriPB accepts. An
uncertified computation reproduces the value $\alpha(J(13,6,4)) = 46$ reported by Exoo
and Ismailescu, which gives $\chi(\R^{12}) \ge 38$.
\end{abstract}

\maketitle

\section{Introduction}\label{sec:intro}

For $n \ge 1$ the chromatic number $\chi(\R^n)$ is the least number of colors needed to
color the points of $\R^n$ so that no two points at Euclidean distance exactly 1 receive
the same color.

In a fixed dimension $n$, finite unit-distance graphs give lower bounds on $\chi(\R^n)$:
a finite graph $G$ drawn in $\R^n$ with every edge of length 1 gives
$\chi(\R^n) \ge \chi(G) \ge \lceil |V(G)|/\alpha(G) \rceil$, where $\alpha(G)$ is the
independence number of $G$.

\begin{theorem}\label{thm:main}
Let $J(13,5,3)$ be the graph whose vertices are the 5-element subsets of
$\{1, \dots, 13\}$. Two of its vertices are adjacent when they share exactly 3 elements.
Then $\alpha(J(13,5,3)) = 33$. Consequently
$\chi(\R^{12}) \ge \lceil 1287/33 \rceil = 39$.
\end{theorem}

For $n = 12$, \textcite{KT2014} obtained $\chi(\R^{12}) \ge 32$ by computation.
\textcite{EI2014} computed the independence number of the generalized Johnson graph
$J(13,6,4)$ (\cref{def:johnson}) as 46 with two independent programs; this value gives 38
through \eqref{eq:counting}, although they state the bound as 36 (\cref{sec:j1364}). The
largest bound stated in the literature from an explicit finite unit-distance graph is 37,
which \textcite{CKR2018} proved from a closed form for the independence number of a
$\{-1,0,1\}$ distance graph. \Cref{thm:main} raises this bound to 39. In dimensions 13
and 14 the theorems of \cite{CKR2018} give 46 and 52, above the bound 39 that
\cref{thm:main} gives there by monotonicity.

In a recent preprint, \textcite{Davies2026} proves that for $n \ge 4$ the chromatic
number of $\R^n$ equals its measurable chromatic number. With the lower bounds of
\textcite{BPT2015} on the measurable chromatic number, the theorem gives
$\chi(\R^{12}) \ge 164$, and with the density certificates of \cite{Davies2026} it gives
$\chi(\R^n) \ge \num{2516}$, \num{5616} and \num{12688} for $n = 12, 13, 14$. By the
de Bruijn--Erd\H{o}s theorem \cite{dBE1951}, each of these bounds implies that a finite
unit-distance graph with at least that chromatic number exists; none has been exhibited.
If these bounds stand, the contribution
of \cref{thm:main} is the exact value of $\alpha(J(13,5,3))$ and an explicit
\num{1287}-vertex unit-distance graph of chromatic number at least 39.

A literature search in October 2026, including Brouwer's tables of constant-weight codes,
the OEIS and the literature on codes with forbidden distances, found no published value
of $\alpha(J(13,5,3))$. In coding terms, $\alpha(J(13,5,3))$ is the largest number of
binary words of length 13 and constant weight 5 with no two at Hamming distance exactly
4. In this quantity one distance is forbidden, whereas in the quantity $A(n,d,w)$ of the
standard tables of constant-weight codes every distance below $d$ is forbidden.
\textcite{BPT2015} tabulate bounds on $\alpha(J(n,k,t))$, which they write
$\alpha(J(n,w,i))$; their table has rows for $J(13,5,2)$ and $J(13,6,2)$, none for the
two graphs studied here, and its exact values end at $\alpha(J(12,5,2)) = 57$.
\textcite{BCL2026} determine the asymptotic order of the independence number of the graph
on $\{0,1\}^n$ whose edges join the pairs at one fixed Hamming distance, in a setting that
covers the constant-weight quantity above; their results give no value at $n = 13$. The
Frankl--Wilson-type inequality stated in the survey \cite{RSM2025} gives
$\alpha(J(13,5,3)) \le 93$ and $\alpha(J(13,6,4)) \le 157$, and the Delsarte linear
programs, solved exactly, give 58 and 78 (\cref{prop:delsarte}).

We call a computational result \emph{certified} if it comes with a certificate, an
output that a separate program can check, and \emph{uncertified} if it rests on a solver
verdict alone. The proof of \cref{thm:main} uses certified results only;
\cref{subsec:trust} states the limits of the tools behind it.

The lower bound $\alpha(J(13,5,3)) \ge 33$ comes from an explicit independent set
(\cref{app:witness33}). For the upper bound, vertex-transitivity and orbital branching
reduce $\alpha \le 33$ to 200 clique subproblems (\cref{sec:graph}), and a certifying
solver refutes each one with a proof log that the proof checker VeriPB accepts
(\cref{sec:j1353}). \Cref{sec:further} gives $\alpha(J(13,6,4)) = 46$, conditional on
uncertified solver verdicts, and shows that, up to isomorphism, $J(13,5,3)$ and
$J(13,6,4)$ are the only generalized Johnson graphs with ground-set size 13 whose
counting bound \eqref{eq:counting} can exceed 33. \Cref{sec:remarks} lists open
questions.


\section{Generalized Johnson graphs and the reduction to clique subproblems}\label{sec:graph}

\begin{definition}\label{def:johnson}
For integers $n \ge k > t \ge 0$, the \emph{generalized Johnson graph} $J(n,k,t)$ has
as vertices the $k$-element subsets of $[n] = \{1, \dots, n\}$, and two vertices $A$ and
$B$ are adjacent if and only if $|A \cap B| = t$.
\end{definition}

The survey \cite{RSM2025} denotes $J(n,k,t)$ by $G(n,k,t)$.

\begin{lemma}\label{lem:embed}
Let $n \ge k > t \ge 0$, and for a $k$-element subset $A$ of $[n]$ let
$\mathbf{1}_A \in \{0,1\}^n$ be its indicator vector. Then the points
$x_A = \mathbf{1}_A/\sqrt{2(k-t)}$ lie in the affine hyperplane
$\{y \in \R^n : \sum_i y_i = k/\sqrt{2(k-t)}\}$. This hyperplane is isometric to
$\R^{n-1}$, and $\|x_A - x_B\| = 1$ whenever $|A \cap B| = t$. Hence every proper
coloring of $\R^{n-1}$ restricts to a proper coloring of $J(n,k,t)$.
\end{lemma}

\begin{proof}
Each $\mathbf{1}_A$ has coordinate sum $k$, and
$\|\mathbf{1}_A - \mathbf{1}_B\|^2 = |A \setminus B| + |B \setminus A| = 2(k - |A \cap B|)$.
\end{proof}

\begin{lemma}\label{lem:counting}
Every finite graph $G$ satisfies $\chi(G) \ge \lceil |V(G)|/\alpha(G) \rceil$. Moreover,
for $n \ge k > t \ge 0$,
\begin{equation}\label{eq:counting}
\chi(\R^{n-1}) \ge \left\lceil \frac{\binom{n}{k}}{\alpha(J(n,k,t))} \right\rceil.
\end{equation}
\end{lemma}

\begin{proof}
Each color class of a proper coloring is an independent set, which gives the first
inequality; the second follows from it and \cref{lem:embed}.
\end{proof}

The graph $J(13,5,3)$ has $\binom{13}{5} = \num{1287}$ vertices and $J(13,6,4)$ has
$\binom{13}{6} = \num{1716}$.

For a finite graph $H$ and an integer $\tau \ge 1$, the \emph{clique subproblem}
$(H, \tau)$ asks whether $H$ contains a clique on $\tau$ vertices; it is \emph{UNSAT} if
the answer is negative and \emph{SAT} otherwise.

\subsection{Fixing one vertex}\label{subsec:fix}

\begin{lemma}\label{lem:vt}
For $n \ge k > t \ge 0$ the graph $J(n,k,t)$ is vertex-transitive.
\end{lemma}

\begin{proof}
Every permutation of $[n]$ preserves intersection sizes and so acts on $J(n,k,t)$ as an
automorphism. The permutations of $[n]$ act transitively on the $k$-element subsets of
$[n]$.
\end{proof}

\begin{proposition}\label{prop:reduction}
Let $n \ge k > t \ge 0$, let $J = J(n,k,t)$ and $v_1 = \{1, \dots, k\}$, let
$\bar N(v_1) = V(J) \setminus (N_J(v_1) \cup \{v_1\})$ be the set of vertices that are
distinct from $v_1$ and not adjacent to it, let $G_0$ be the complement of the induced
subgraph $J[\bar N(v_1)]$, and let $\omega$ denote the clique number. Then
\begin{equation}\label{eq:reduction}
\alpha(J) = 1 + \omega(G_0).
\end{equation}
\end{proposition}

\begin{proof}
If $C$ is a clique of $G_0$, then $C \cup \{v_1\}$ is independent in $J$, so
$\alpha(J) \ge 1 + \omega(G_0)$. Conversely, by \cref{lem:vt} some maximum independent
set $I$ of $J$ contains $v_1$, and $I \setminus \{v_1\} \subseteq \bar N(v_1)$ is then a
clique of $G_0$.
\end{proof}

\subsection{The orbital branching tree}\label{subsec:tree}

\begin{definition}\label{def:node}
Let $G$ be a finite simple graph and $s \ge 1$ an integer. A \emph{node} is a triple
$\nu = (F, X, \tau)$ with $F$ a clique of $G$ (the forced clique), $X \subseteq V(G)$
(the excluded set) and $\tau = s - |F|$ (the local threshold). Its \emph{residual set} is
\[
R(\nu) = \Bigl(\bigcap_{f \in F} N_G(f)\Bigr) \setminus X,
\qquad \text{reading the intersection as } V(G) \text{ when } F = \emptyset,
\]
its \emph{residual graph} is $H(\nu) = G[R(\nu)]$, and its \emph{subproblem} is the
clique subproblem $(H(\nu), \tau)$. The \emph{root} is $(\emptyset, \emptyset, s)$.
\end{definition}

Orbital branching, which originates with \textcite{OLRS2011}, expands a node $\nu$ as
follows. A subgroup $\Gamma$ of the automorphism group of $H(\nu)$ is fixed, a vertex
$r \in R(\nu)$ is chosen, and $O$ denotes the $\Gamma$-orbit of $r$. The node gets two
children: the include child $(F \cup \{r\}, X, \tau - 1)$ with residual set
$R(\nu) \cap N_G(r)$, and the exclude child $(F, X \cup O, \tau)$ with residual set
$R(\nu) \setminus O$. The set $F \cup \{r\}$ is again a clique of $G$, since $r$ lies in
the common neighborhood of $F$. Repeated expansion from the root gives a finite binary
tree, whose leaf subproblems are decided by computation.

\begin{lemma}[orbital branching]\label{lem:cover}
Let $H$ be a finite simple graph, let $\Gamma \le \operatorname{Aut}(H)$ be any
subgroup, let $O \subseteq V(H)$ be a $\Gamma$-orbit, let $r \in O$, and let $\tau$ be
an integer. Then $H$ has a clique of size at least $\tau$ if and only if either $H$ has a
clique of size at least $\tau$ containing $r$ or $H - O$ has a clique of size at least
$\tau$.
\end{lemma}

\begin{proof}
Cliques containing $r$ and cliques of the induced subgraph $H - O$ are cliques of $H$.
Conversely, let $C$ be a clique of $H$ with $|C| \ge \tau$. If $C$ misses $O$, it is a
clique of $H - O$. Otherwise pick $x \in C \cap O$; since $O$ is one orbit, some
$\gamma \in \Gamma$ maps $x$ to $r$, and $\gamma(C)$ is a clique of size $|C|$
containing $r$.
\end{proof}

\begin{proposition}\label{prop:covering}
Let $G$ be a finite simple graph, let $s \ge 1$ be an integer, and let $T$ be a finite
tree obtained from the root $(\emptyset, \emptyset, s)$ by expansions as defined above.
Suppose that the expansion at each internal node $\nu$ of $T$ uses a subgroup
$\Gamma_\nu \le \operatorname{Aut}(H(\nu))$ and the $\Gamma_\nu$-orbit of the chosen
representative. Then $\omega(G) \ge s$ if and only if $\omega(H(\ell)) \ge \tau_\ell$ for
some leaf $\ell$ of $T$, where $\tau_\ell$ is the local threshold of $\ell$.
\end{proposition}

\begin{proof}
Let $\nu$ be an internal node with local threshold $\tau$, representative $r$ and orbit
$O$, and apply \cref{lem:cover} to $H = H(\nu)$ and $\Gamma = \Gamma_\nu$. Deleting $r$
maps the cliques of size at least $\tau$ through $r$ onto the cliques of size at least
$\tau - 1$ in the include child's residual graph, and the cliques of $H(\nu)$ avoiding
$O$ are those of the exclude child's residual graph. So $\omega(H(\nu)) \ge \tau$ if and
only if some child $\mu$ of $\nu$ has $\omega(H(\mu)) \ge \tau_\mu$, where $\tau_\mu$ is
its local threshold. Induction on the height of $T$ gives the claim, since the root has
residual graph $G$ and local threshold $s$.
\end{proof}

Let $G_0$ be the graph of \cref{prop:reduction} for $J = J(n,k,t)$, and let $T$ be a tree
for $G_0$ and $s$ as in \cref{prop:covering}. Since $\alpha(J) \le s$ exactly when
$\omega(G_0) < s$ by \eqref{eq:reduction}, \cref{prop:covering} gives
\begin{equation}\label{eq:finite}
\alpha(J) \le s \iff \omega(H(\ell)) < \tau_\ell \text{ for every leaf } \ell \text{ of } T.
\end{equation}


\section{Certified computation for \texorpdfstring{$J(13,5,3)$}{J(13,5,3)}}\label{sec:j1353}

This section proves \cref{thm:main}. We build an orbital branching tree for the graph
$G_0$ of $J(13,5,3)$ at $s = 33$, certify its 200 leaf subproblems, and check the
decomposition.

\subsection{Construction and decomposition}\label{subsec:algorithm}

All computations on graphs, permutations and witnesses use exact integer arithmetic.
We carry out the following steps for $J(13,5,3)$ at $s = 33$, and
steps~\ref{step:build} to~\ref{step:leaffiles} also for $J(13,6,4)$ at $s = 46$
(\cref{sec:j1364}).
\begin{enumerate}
\item\label{step:build} Build $J(n,k,t)$ from \cref{def:johnson} by two implementations
that share no code, \emph{implementation A} and \emph{implementation B}, and compare
their edge lists edge for edge.
\item\label{step:g0} Build $G_0$, the graph of \cref{prop:reduction}, with a map from its
vertices back to $k$-element subsets. The $k$-element subsets are numbered in
lexicographic order, so that $v_1$ is vertex 1, and $G_0$ numbers its vertices in the
same order.
\item\label{step:branch} Branch. Starting from the root $(\emptyset, \emptyset, s)$, which
is node 1, repeatedly expand the frontier node with the largest residual vertex count
until the tree has 200 leaves; break ties by the smallest node identifier. An expansion
gives its include child and then its exclude child the next two free identifiers. Each
expansion of a node $\nu$ runs four substeps.
\begin{enumerate}
\item Each node carries a partition of $[13]$. The root partition has the blocks
$\{1,\dots,k\}$ and $\{k{+}1,\dots,13\}$, and an include step that forces a vertex $u$ (a
$k$-element subset of $[13]$) splits every block $B$ into $B \cap u$ and $B \setminus u$.
For each block $\{b_1 < \dots < b_m\}$ of the partition of $\nu$, take the transposition
$(b_1\,b_2)$ if $m \ge 2$ and the cycle $(b_1\,b_2\,\cdots\,b_m)$ if $m \ge 3$. These
generate the Young subgroup of the partition; at the root it is
$\operatorname{Sym}(\{1,\dots,k\}) \times \operatorname{Sym}(\{k{+}1,\dots,13\})$, of
order $5!\,8! = \num{4838400}$ for $J(13,5,3)$ and $6!\,7! = \num{3628800}$ for
$J(13,6,4)$. A permutation of $[13]$ that maps $\{1, \dots, k\}$ onto itself fixes $v_1$
and preserves intersection sizes, so it acts as an automorphism of $G_0$. The Young
subgroup of the partition of $\nu$ fixes every forced vertex and lies in the group of
every ancestor of $\nu$; since the excluded set of $\nu$ is a union of orbits of the
groups of its ancestors, the subgroup maps $R(\nu)$ onto itself.
\item Check each generator by three tests, so that the soundness of the expansion does
not depend on the group the generators are meant to generate; any failure aborts the
construction, and no generator failed.
\begin{enumerate}[label=(G\arabic*)]
\item\label{test:g1} The permutation of $[13]$ induces a permutation of $V(G_0)$.
\item The induced permutation maps the edge list of $G_0$ onto itself.
\item\label{test:g3} It maps $R(\nu)$ onto itself and preserves the residual edge list.
\end{enumerate}
\item Compute orbits as forward closures under the checked generators; on a finite set
the forward closure of a vertex is its orbit under the generated group, since the inverse
of each generator is one of its powers. Choose the largest orbit $O$; among orbits of
equal size, choose the one whose least vertex identifier is smallest. Take the vertex
with the smallest identifier in $O$ as the representative $r$, and check one more test.
\begin{enumerate}[label=(G\arabic*), start=4]
\item\label{test:g4} The orbit satisfies $r \in O \subseteq R(\nu)$.
\end{enumerate}
\item Form the include child and the exclude child.
\end{enumerate}
A node is a leaf when it lies at depth 12, when every orbit of its group on $R(\nu)$ is
a single vertex, or when the tree reaches 200 leaves. These rules affect only the shape
of the tree: by \cref{lem:cover}, every choice of orbit and representative gives a sound
expansion. Record the rule, the generators, every leaf's $(F, X, \tau)$ and every
residual vertex count in a \emph{manifest}, written before any leaf subproblem is
decided and not changed afterwards.
\item\label{step:leaffiles} Write each leaf's residual graph, with a vertex map, to its
own file, the \emph{leaf file}, numbering the leaves in increasing order of node
identifier.
\item Certify each leaf subproblem (\cref{subsec:certification}).
\item Check the decomposition (\cref{subsec:checks}).
\end{enumerate}

Call the resulting tree $T_{33}$. Each leaf $\ell$ of $T_{33}$ has forced clique
$F_\ell$, residual set $R_\ell$, residual graph $H_\ell$ and local threshold
$\tau_\ell = 33 - |F_\ell|$. The vertex $v_1$ of $J(13,5,3)$ has
$\binom{5}{3}\binom{8}{2} = 280$ neighbors, so $G_0$ has $1287 - 1 - 280 = \num{1006}$
vertices; it has \num{391135} edges (density 0.774). Of the 200 leaves of $T_{33}$, 66
lie at depth 12, 84 have only single-vertex orbits, and 50 were on the frontier when the
tree reached 200 leaves. The tree uses 21 distinct generators and has no leaf with an empty
residual set. The margin $|R_\ell| - \tau_\ell$ is at least 63 on every leaf, so no
leaf subproblem is UNSAT for lack of vertices. Over the 200 leaves, $|R_\ell|$ runs from
96 to 466 with median $205.5$, and $\tau_\ell$ runs from 29 to 33: it equals 29 on 140
leaves, 30 on 47, 31 on 10, 32 on 2 and 33 on 1.

\subsection{Lower-bound witness}\label{subsec:witnesses}

\begin{proposition}\label{prop:witness33}
The 33 five-element subsets of $[13]$ listed in \cref{app:witness33} are pairwise
non-adjacent in $J(13,5,3)$. Hence $\alpha(J(13,5,3)) \ge 33$.
\end{proposition}

\begin{proof}
Check the 528 pairs; \cref{app:witness33} reduces the check to pairs from different
blocks.
\end{proof}

The set was found by randomized local search.

\subsection{Certified leaves}\label{subsec:certification}

Each leaf subproblem is encoded as a \emph{pseudo-Boolean formula} (a system of linear
inequalities over 0/1 variables). For a leaf $\ell$ with $n_\ell$ residual vertices,
$m_\ell$ residual edges and local threshold $\tau_\ell$, the formula has one variable
$x_w$ for each vertex $w$ of the residual graph and two families of constraints:
\begin{enumerate}
\item[(C)] one cardinality constraint $\sum_w x_w \ge \tau_\ell$;
\item[(N)] one constraint $x_u + x_w \le 1$ for each of the $\binom{n_\ell}{2} - m_\ell$
non-adjacent pairs $\{u, w\}$.
\end{enumerate}
The 0/1 solutions are exactly the indicator vectors of cliques on at least $\tau_\ell$
vertices, so the formula has no solution if and only if the leaf subproblem is UNSAT.

Each leaf was decided in three steps.
\begin{enumerate}
\item The clique solver of the Glasgow Subgraph Solver \cite{McCreeshPT2020}, run in
decision mode at $\tau_\ell$ with the proof logging of \textcite{GMMNPT2020}, wrote its
own pseudo-Boolean formula for the leaf. It refuted the formula and wrote a VeriPB proof
log of the refutation \cite{VeriPBdoc}.
\item A program separate from the solver, the \emph{encoding checker}, rebuilt the
expected formula from the leaf file and from $\tau_\ell = 33 - |F_\ell|$, and required
the solver's formula to equal it (the \emph{encoding check}) up to constraint labels, the
order of constraints and of terms, the rewriting of a negated literal $\bar x$ as
$1 - x$, and division of a constraint by a common factor of its coefficients with the
right-hand side rounded up. None of these changes the 0/1 solutions. The expected formula
has the variables $x_1, \dots, x_{n_\ell}$, one constraint of family (C), which carries
all $n_\ell$ variables with coefficient 1 and has right-hand side $\tau_\ell$, and the
constraints of family (N) for exactly the non-adjacent pairs; it contains nothing else.
The encoding checker shares no code with the solver or with the script that runs the
solver.
\item The proof checker VeriPB checked the proof log against the formula. A proof log is
a sequence of linear inequalities, each derived from the formula and earlier lines by
sound rules and the last a contradiction, so VeriPB's acceptance shows that the formula
has no 0/1 solution.
\end{enumerate}
The procedure was first tested on $J(8,3,1)$, $J(9,3,1)$, $J(10,5,3)$ and $J(11,5,3)$,
whose independence numbers are known. VeriPB accepted the proof logs of all 200 leaves
of $T_{33}$. The leaf verdicts thus rest on the encoding checker and VeriPB alone.
\Cref{tab:proofs} in \cref{app:corroboration} gives proof-log sizes and times for nine
of the leaves.

Five of the leaves (16, 169, 170, 173 and 176) also have a proper coloring of the
residual graph with fewer colors than the local threshold (\cref{tab:fragments}), found
by a randomized DSATUR search \cite{Brelaz1979}. Since the vertices of a clique receive
pairwise different colors, each such coloring certifies its leaf by itself. A program
separate from the search checks every coloring edge by edge and matches it to its leaf
file and local threshold.

\subsection{Checks of the decomposition}\label{subsec:checks}

One program ran the ten steps of \cref{tab:master}, from the construction of
$J(13,5,3)$ to the bound 39, and all ten passed. Steps 1 to 6 run implementation B, three
programs that share no code with implementation A or with each other; they recompute the
graphs, the tree and its residual sets without reading any recorded check result, and
compare them with the stored graph, manifest and leaf files. The rule and generators
recorded in the manifest fix every branching decision of the replay. Steps 7 and 8 read
the VeriPB acceptances and encoding-check results recorded when each leaf was certified.
Implementation A ran tests~\ref{test:g1} to~\ref{test:g4} during construction and
replayed the tree with code separate from its tree construction. As a test of the
generator checks, a generator composed with a transposition of two vertices of equal
degree was rejected.

\begin{table}[htbp]
\centering
\caption{The end-to-end check for $J(13,5,3)$}\label{tab:master}
\small
\begin{tabular}{@{}r>{\raggedright\arraybackslash}p{0.68\textwidth}l@{}}
\toprule
Step & Content & Check \\
\midrule
1 & $J(13,5,3)$ rebuilt from its definition, 1287 vertices, degree 280, edge list matched to the recorded one & recomputed \\
2 & $G_0$ rebuilt on $1287 - 1 - 280 = 1006$ vertices, its file reproduced byte for byte & recomputed \\
3 & 21 generators: permutations of all \num{1006} vertices, edge preserving, each mapping its node's residual set onto itself & recomputed \\
4 & tree replayed from its rule: 200 leaves, 0 dropped, residual sets recomputed & recomputed \\
5 & the 200 leaf files equal $G_0$ induced on the recomputed residual sets & recomputed \\
6 & $\tau_\ell = 33 - |F_\ell|$ on 200 of 200 leaves & recomputed \\
7 & 5 colorings re-verified; proof-log acceptances and encoding-check records read for all 200 leaves & record read \\
8 & $\omega(G_0) \le 32$, from steps 3, 4 and 7 & record read \\
9 & $\alpha(J(13,5,3)) = 1 + \omega(G_0) \le 33$ from step 8; vertex-transitivity recomputed (orbit of vertex 1 under the 12 adjacent transpositions of $[13]$ is all 1287 vertices) & \parbox[t]{5.5em}{\raggedright recomputed; rests on step~8} \\
10 & $\lceil 1287/33 \rceil = 39$; indicator vectors in the hyperplane $x_1 + \dots + x_{13} = 5$, adjacent ones at distance 2, so the points $\mathbf{1}_A/2$ are at distance 1 & recomputed \\
\bottomrule
\end{tabular}
\end{table}

\subsection{Limitations}\label{subsec:trust}

The proof logs were checked with VeriPB, which is not formally verified; the formally
verified checker CakePB \cite{VeriPBdoc}, which checks VeriPB proof logs compiled into a
restricted kernel format, was not run on them because of its expected running time. The encoding checker and the programs
that check the decomposition are not formally verified either.

\subsection{Proof of the main theorem}\label{subsec:proof}

\begin{proposition}\label{prop:leaves}
For every leaf $\ell$ of $T_{33}$, the residual graph $H_\ell$ contains no clique on
$\tau_\ell$ vertices.
\end{proposition}

\begin{proof}
By steps 4 to 6 of \cref{tab:master}, the 200 leaf files hold the residual graphs
$H_\ell$ of the leaves of $T_{33}$, whose local thresholds are
$\tau_\ell = 33 - |F_\ell|$. By step 7, for each leaf VeriPB accepted a proof log
refuting a formula that the encoding check matched to the leaf file and to $\tau_\ell$
(\cref{subsec:certification}), and the 0/1 solutions of that formula are the indicator
vectors of the cliques of $H_\ell$ on at least $\tau_\ell$ vertices.
\end{proof}

\begin{proof}[Proof of \cref{thm:main}]
Tests~\ref{test:g1} to~\ref{test:g4} of step~\ref{step:branch} show that $T_{33}$
satisfies the hypotheses of \cref{prop:covering}, and by \cref{prop:leaves} no leaf
residual graph $H_\ell$ has a clique on $\tau_\ell$ vertices. Hence
$\alpha(J(13,5,3)) \le 33$ by \eqref{eq:finite}, and \cref{prop:witness33} gives
equality. Since $33 \cdot 39 = 1287$, \cref{lem:counting} gives $\chi(\R^{12}) \ge 39$.
\end{proof}

\begin{corollary}\label{cor:fractional}
The fractional chromatic number of $J(13,5,3)$ is $\chi_f(J(13,5,3)) = 39$.
\end{corollary}

\begin{proof}
Since $J(13,5,3)$ is vertex-transitive (\cref{lem:vt}), Proposition~3.1.1 of
\cite{SU1997} gives
\[
\chi_f(J(13,5,3)) = \frac{1287}{\alpha(J(13,5,3))}.
\]
\Cref{thm:main} gives $\alpha(J(13,5,3)) = 33$, so $\chi_f(J(13,5,3)) = 1287/33 = 39$.
\end{proof}


\section{Further computations}\label{sec:further}

This section reports what \cref{thm:main} does not use: the uncertified MaxCliqueDyn
search with its reruns, the computation for $J(13,6,4)$, and the other parameter pairs
with ground-set size 13.

\subsection{The MaxCliqueDyn search and reruns}\label{subsec:production}

The MaxCliqueDyn search used a build of the branch-and-bound solver MaxCliqueDyn
\cite{KJ2007} modified to solve the decision problem at a fixed threshold, with its search
logic unchanged (\cref{tab:software}). It returned UNSAT on all 200 leaves of each tree at
their local thresholds. Both implementations checked that each leaf has exactly one such
verdict, matched to its leaf file; implementation B also matched each verdict to its
solver transcript.

The solvers MoMC \cite{LJM2017} and cliquer \cite{NO2003} share no code with
MaxCliqueDyn, were written by other authors, and use different bounding rules. MoMC reran
every leaf of $T_{33}$ and returned UNSAT on all 200, so three solvers agree on all 200
leaves of $T_{33}$: MaxCliqueDyn, MoMC and the certifying solver of
\cref{subsec:certification}. On the tree for $J(13,6,4)$, MoMC and cliquer reran a sample
of 14 of the 200 leaves, fixed before the reruns: the three leaves other than leaf 1 with
the longest MaxCliqueDyn times and, in each of the 11 nonempty classes defined by local
threshold and tercile of MaxCliqueDyn time, the lowest-numbered of the remaining leaves.
MoMC returned UNSAT on 13 of the 14 leaves; cliquer, run on the 8 with MaxCliqueDyn times
up to \qty{600}{\second}, returned UNSAT on 6. The other three runs, one of MoMC and two of
cliquer, reached their time cap of \qty{600}{\second}. Each of the 14 leaves was returned
UNSAT by at least one of the two solvers, and no rerun verdict contradicted MaxCliqueDyn.
Leaf 1 of that tree, the largest, with 761 residual vertices and a MaxCliqueDyn time of
\qty{20.6}{\hour}, was left out of the sample for its projected cost. Every solver read the
same leaf files, so the reruns check neither the construction of the leaves nor the
coverage of the tree.

\subsection{The independence number of \texorpdfstring{$J(13,6,4)$}{J(13,6,4)}}\label{sec:j1364}

The computation for $J(13,6,4)$ followed steps~\ref{step:build} to~\ref{step:leaffiles}
of \cref{subsec:algorithm} at $s = 46$, and the generator, tree and leaf-file checks of
\cref{subsec:checks} were applied to it as well. Let $G_0'$ be the graph of \cref{prop:reduction} for $J(13,6,4)$
and $T_{46}$ its tree, with $F_\ell$, $R_\ell$ and $H_\ell$ as for $T_{33}$ and
$\tau_\ell = 46 - |F_\ell|$. The vertex $v_1$ of $J(13,6,4)$ has
$\binom{6}{4}\binom{7}{2} = 315$ neighbors, so $G_0'$ has $1716 - 1 - 315 = \num{1400}$
vertices; it has \num{793135} edges (density 0.810). Like $T_{33}$, the tree $T_{46}$ has
200 leaves and uses 21 distinct generators. On every leaf the margin
$|R_\ell| - \tau_\ell$ is at least 129; over the 200 leaves, $|R_\ell|$ runs from 175 to
761 with median 394, and $\tau_\ell$ runs from 42 to 46 with median 42.

\begin{proposition}\label{prop:witness46}
The 46 six-element subsets of $[13]$ listed in \cref{app:witness46} are pairwise
non-adjacent in $J(13,6,4)$. Hence $\alpha(J(13,6,4)) \ge 46$.
\end{proposition}

\begin{proof}
Check the \num{1035} pairs (\cref{app:witness46}).
\end{proof}

The set was found by randomized local search.

\begin{claim}\label{clm:j1364}
For every leaf $\ell$ of $T_{46}$, the residual graph $H_\ell$ contains no clique on
$\tau_\ell$ vertices.
\end{claim}

Leaves 11 and 170 are certified by colorings with fewer colors than their local
thresholds (\cref{tab:fragments}); a DSATUR search like that of
\cref{subsec:certification}, run earlier on 15 leaves of $T_{46}$, found the two colorings.
The other 198 leaves rest on MaxCliqueDyn verdicts, and 12 of them were rerun
(\cref{subsec:production}). No proof logging was attempted for $J(13,6,4)$. On its leaves
other than leaf 1, the MaxCliqueDyn search visited about 120 times as many nodes as on all
200 leaves of $T_{33}$. Its verdict records name the same solver version as those of
$J(13,5,3)$ but predate the recording of the binary's SHA-256 digest, which was linked to
them after the run.

\begin{proposition}\label{prop:j1364}
If \cref{clm:j1364} holds, then $\alpha(J(13,6,4)) = 46$.
\end{proposition}

\begin{proof}
The argument for $\alpha(J(13,5,3)) = 33$ in the proof of \cref{thm:main} applies with
$G_0'$, $s = 46$, $T_{46}$, \cref{clm:j1364} and \cref{prop:witness46} in place of $G_0$,
$s = 33$, $T_{33}$, \cref{prop:leaves} and \cref{prop:witness33}.
\end{proof}

Under \cref{clm:j1364}, \cref{lem:counting} gives
$\chi(\R^{12}) \ge \lceil 1716/46 \rceil = 38$, which \cref{thm:main} supersedes.

\textcite{EI2014} report $\alpha(J(13,6,4)) = 46$: ``both mcqd and our specialized
program were able to determine that the independence number is 46'' (mcqd is
MaxCliqueDyn \cite{KJ2007}). They give the resulting bound as
$\lceil 1716/46 \rceil = 36$. The ceiling is 38, since
$46 \cdot 37 = 1702 < 1716 \le 1748 = 46 \cdot 38$, so their stated bound
$\chi(\R^{12}) \ge 36$ is valid and two below what their value gives. The introduction of
\cite{CKR2018} lists $\chi(\R^{12}) \ge 36$ as an announced improvement.

The present computation reproduces the value 46, uncertified, with its own reduction,
decomposition and leaf files. Its verdicts come from MaxCliqueDyn, which \textcite{EI2014}
also ran; their second program repeated the full search, while MoMC and cliquer reran 14
of the 200 leaves here. The present work adds the decomposition proof, implementation B
and the two certified leaves.

\subsection{Other generalized Johnson graphs with ground-set size 13}\label{sec:exclusion}

Up to isomorphism, $J(13,5,3)$ and $J(13,6,4)$ are the only generalized Johnson graphs
with ground-set size 13 whose counting bound \eqref{eq:counting} can exceed 33. The pairs
$(8,6)$ and $(7,5)$ excluded below give their complements $J(13,8,6) \cong J(13,5,3)$ and
$J(13,7,5) \cong J(13,6,4)$.

\begin{proposition}\label{prop:exclusion}
Let $(k,t)$ range over the 91 pairs with $1 \le k \le 13$ and $0 \le t < k$. For each of
the 87 pairs outside $\{(5,3), (8,6), (6,4), (7,5)\}$ there is an independent set of size
$a$ in $J(13,k,t)$ with $\lceil \binom{13}{k}/a \rceil \le 33$; hence the counting bound
\eqref{eq:counting} for these graphs is at most 33.
\end{proposition}

\begin{proof}
Two $k$-element subsets of $[13]$ share at least $2k - 13$ elements, so the 49 graphs with
$t < 2k - 13$ are edgeless; for them $a = \binom{13}{k}$ and the ceiling is 1. The graphs
$J(13,1,0)$ and $J(13,12,11)$ are complete on 13 vertices, so $a = 1$ and the ceiling is
13. \Cref{tab:exclusion} gives $a$ and the ceiling for the 18 pairs with
$2 \le k \le 6$. For $t = 0$ the witness is the set of $k$-element subsets containing the
element 1, of size $\binom{12}{k-1}$, a maximum independent set by the
Erd\H{o}s--Ko--Rado theorem \cite{EKR1961} since $13 \ge 2k$. The other 13 witnesses were
found by randomized local search and give lower bounds only. All pairs of sets in each
witness were checked by machine. The remaining 18 pairs have $k \ge 7$ and follow through
the isomorphism $A \mapsto [13] \setminus A$ from $J(13,k,t)$ onto
$J(13,13-k,13-2k+t)$. The largest ceiling, 33, occurs at $J(13,4,2)$ and $J(13,9,7)$.
\end{proof}

\begin{table}[htbp]
\centering
\caption{Witness size $a$ and ceiling $\lceil \binom{13}{k}/a \rceil$, written $a$ (ceiling), for the 18 pairs $(k,t)$ of \cref{prop:exclusion} with $2 \le k \le 6$; the excluded pairs $(5,3)$ and $(6,4)$ are blank}\label{tab:exclusion}
\small
\begin{tabular}{@{}rrllllll@{}}
\toprule
$k$ & $\binom{13}{k}$ & $t = 0$ & $t = 1$ & $t = 2$ & $t = 3$ & $t = 4$ & $t = 5$ \\
\midrule
2 & 78 & 12 (7) & 6 (13) \\
3 & 286 & 66 (5) & 12 (24) & 26 (11) \\
4 & 715 & 220 (4) & 55 (13) & 22 (33) & 65 (11) \\
5 & 1287 & 495 (3) & 165 (8) & 62 (21) &  & 122 (11) \\
6 & 1716 & 792 (3) & 372 (5) & 148 (12) & 86 (20) &  & 156 (11) \\
\bottomrule
\end{tabular}
\end{table}

The proposition bounds only the right-hand side of \eqref{eq:counting}. Up to
isomorphism, the independence and chromatic numbers of the 87 graphs are determined here
only for the edgeless graphs, for $J(13,1,0)$, and for the Kneser graphs $J(13,k,0)$ with
$2 \le k \le 6$, where $13 \ge 2k$, so that the Erd\H{o}s--Ko--Rado theorem gives
$\alpha = \binom{12}{k-1}$ and Lov\'asz's theorem \cite{Lovasz1978} gives
$\chi = 15 - 2k$.

\section{Open questions}\label{sec:remarks}

\begin{question}\label{q:forty}
Is $\chi(J(13,5,3)) = 39$? The fractional chromatic number is 39 (\cref{cor:fractional}),
and since $\alpha(J(13,5,3)) = 33$ and $39 \cdot 33 = 1287$, a 39-coloring would partition
the vertices into 39 maximum independent sets. A negative answer would give
$\chi(\R^{12}) \ge 40$ from the same graph.
\end{question}

\begin{question}\label{q:maxsets}
Are all maximum independent sets of $J(13,5,3)$ equivalent under $\operatorname{Sym}(13)$?
\end{question}

\begin{question}\label{q:larger}
Does some $J(n,k,t)$ with $n \in \{14, 15\}$ give, through \eqref{eq:counting}, a bound
above 46 on $\chi(\R^{13})$ or above 52 on $\chi(\R^{14})$?
\end{question}


\section*{Use of AI tools}

I directed the work, ran the computations, and reviewed the manuscript, the code and the
reported computations. I used Claude Code (Anthropic) with the Claude Fable 5, Fable 5.1,
Fable 5.2 and Opus 5.5 models to plan, draft, revise and review this paper and to write
its code, including the programs for the computation and the verification programs. I
used OpenAI Codex with the GPT-5.6 Sol model to evaluate plans and, on some occasions, to
review drafts of the paper.

\section*{Data availability}

The following are on Zenodo, \mbox{\url{https://doi.org/10.5281/zenodo.24145863}}, each with its SHA-256 digest:
the programs (the verification programs, the MaxCliqueDyn patch with its tests, the
pinned solver revisions and the MaxCliqueDyn binary); the certificates and proof logs (the
lower-bound witnesses, the Delsarte and coloring certificates, and the 200 proof logs for
$J(13,5,3)$ with their pseudo-Boolean formulas and checker transcripts); and the run
records (the run manifests, the 400 leaf files, the per-leaf verdict records, the result
records and the records of the checks, the per-leaf rerun table, the coloring attempts and the 91-pair
parameter table of \cref{sec:exclusion}). The proof logs are compressed with the PPMd
method of 7-Zip 26.04; the archives total \qty{40.6}{\giga\byte}.

\printbibliography

\appendix
\crefalias{section}{appendix}

% The heading, the block note, the listing and the sentence reporting the check of the
% listing take up about 27 baselineskips; reserve them together so the listing is never
% separated from the other three.
\needspace{27\baselineskip}
\section{The 33-vertex witness for \texorpdfstring{$J(13,5,3)$}{J(13,5,3)}}\label{app:witness33}

The 33 sets of \cref{prop:witness33} fall into five blocks. Each of the first three blocks
consists of the six 5-element subsets of one 6-element set; the three 6-element sets are
$\{1,\dots,6\}$, $\{3,6,9,10,12,13\}$ and $\{4,5,7,8,9,10\}$. The fourth block consists of
the six sets $\{1,7,11,12,x\}$ with $x \in \{3,4,5,6,9,10\}$, and the fifth of the nine
sets $\{2,8,11,13,x\}$ with $x \in \{1,3,4,5,6,7,9,10,12\}$. Two sets in the same block
meet in exactly 4 elements, so only pairs from different blocks need checking. Block by
block, the 33 sets are:
\begin{center}
\small
$\begin{array}{@{}lll@{}}
\{1,2,3,4,5\} & \{1,2,3,4,6\} & \{1,2,3,5,6\} \\
\{1,2,4,5,6\} & \{1,3,4,5,6\} & \{2,3,4,5,6\} \\[2pt]
\{3,6,9,10,12\} & \{3,6,9,10,13\} & \{3,6,9,12,13\} \\
\{3,6,10,12,13\} & \{3,9,10,12,13\} & \{6,9,10,12,13\} \\[2pt]
\{4,5,7,8,9\} & \{4,5,7,8,10\} & \{4,5,7,9,10\} \\
\{4,5,8,9,10\} & \{4,7,8,9,10\} & \{5,7,8,9,10\} \\[2pt]
\{1,3,7,11,12\} & \{1,4,7,11,12\} & \{1,5,7,11,12\} \\
\{1,6,7,11,12\} & \{1,7,9,11,12\} & \{1,7,10,11,12\} \\[2pt]
\{1,2,8,11,13\} & \{2,3,8,11,13\} & \{2,4,8,11,13\} \\
\{2,5,8,11,13\} & \{2,6,8,11,13\} & \{2,7,8,11,13\} \\
\{2,8,9,11,13\} & \{2,8,10,11,13\} & \{2,8,11,12,13\} \\
\end{array}$
\end{center}
No two of the 33 subsets intersect in exactly 3 elements (all $\binom{33}{2} = 528$
pairs checked by implementations A and B), so the set is independent in $J(13,5,3)$.

% The heading, the listing and the sentence reporting the check of the listing take up
% about 16 baselineskips; reserve them together so the listing is never separated from
% the other two.
\needspace{16\baselineskip}
\section{The 46-vertex witness for \texorpdfstring{$J(13,6,4)$}{J(13,6,4)}}\label{app:witness46}

As 6-element subsets of $\{1,\dots,13\}$, the 46 sets of \cref{prop:witness46} are:
\begin{center}
\small
$\begin{array}{@{}llll@{}}
\{1,2,3,4,5,6\} & \{1,2,3,4,5,7\} & \{1,2,3,4,6,7\} & \{1,2,3,5,6,7\} \\
\{1,2,3,8,9,10\} & \{1,2,4,5,6,7\} & \{1,2,4,8,9,10\} & \{1,2,5,8,12,13\} \\
\{1,2,6,10,11,12\} & \{1,2,7,9,11,13\} & \{1,3,4,5,6,7\} & \{1,3,4,8,9,10\} \\
\{1,3,5,8,12,13\} & \{1,3,6,10,11,12\} & \{1,3,7,9,11,13\} & \{1,4,5,10,11,13\} \\
\{1,4,6,9,12,13\} & \{1,4,7,8,11,12\} & \{1,5,6,8,9,11\} & \{1,5,7,9,10,12\} \\
\{1,6,7,8,10,13\} & \{2,3,4,5,6,7\} & \{2,3,4,8,9,10\} & \{2,3,5,8,12,13\} \\
\{2,3,6,10,11,12\} & \{2,3,7,9,11,13\} & \{2,4,5,10,11,13\} & \{2,4,6,9,12,13\} \\
\{2,4,7,8,11,12\} & \{2,5,6,8,9,11\} & \{2,5,7,9,10,12\} & \{2,6,7,8,10,13\} \\
\{3,4,5,10,11,13\} & \{3,4,6,9,12,13\} & \{3,4,7,8,11,12\} & \{3,5,6,8,9,11\} \\
\{3,5,7,9,10,12\} & \{3,6,7,8,10,13\} & \{4,5,6,8,9,11\} & \{4,5,7,10,11,13\} \\
\{4,6,7,9,12,13\} & \{4,6,9,10,12,13\} & \{5,6,7,8,9,11\} & \{5,6,8,9,10,11\} \\
\{5,6,8,9,11,12\} & \{5,6,8,9,11,13\} \\
\end{array}$
\end{center}
No two of the 46 subsets intersect in exactly 4 elements (all $\binom{46}{2} =
\num{1035}$ pairs checked by implementations A and B), so the set is independent in
$J(13,6,4)$.

\section{Software and run data}\label{app:corroboration}

\begin{table}[htbp]
\centering
\caption{Software that produced or checked a computational result}\label{tab:software}
\small
\begin{tabular}{@{}>{\raggedright\arraybackslash}p{0.27\textwidth}>{\raggedright\arraybackslash}p{0.33\textwidth}>{\raggedright\arraybackslash}p{0.32\textwidth}@{}}
\toprule
Tool & Version & Role \\
\midrule
modified MaxCliqueDyn \cite{KJ2007} & upstream revision of 2016-09-01; \texttt{clang++ -O3}, as reported by the binary & uncertified search \\
MoMC \cite{LJM2017} & 2019 revision of the 2016 source & reruns \\
cliquer \cite{NO2003} & 1.21 & reruns \\
Glasgow Subgraph Solver \cite{McCreeshPT2020,GMMNPT2020} & upstream revision of 2026-06-19; Apple clang 21.0.0 & certifying search \\
VeriPB \cite{BGMN2023} & 3.0.2 & proof checker \\
R \cite{RCore2026} & 4.6.1, package \texttt{gmp} 0.7.5.1 & implementation A (construction, decomposition), Delsarte linear programs \\
DSATUR coloring heuristic \cite{Brelaz1979} & randomized, in R & coloring certificates \\
Python & 3.14.8 and 3.15.0 & implementation B and checking programs \\
\bottomrule
\end{tabular}
\end{table}

The MaxCliqueDyn searches and the certification ran on the same Apple M1 machine, on
which the solver passed all 30 tests of its own proof test suite. The
reruns ran on a Linux machine. No build log was recorded for the MaxCliqueDyn binary.

\begin{table}[htbp]
\centering
\caption{The seven colorings that certify leaves, sorted by residual vertex count within
each computation}\label{tab:fragments}
\small
\setlength{\tabcolsep}{4pt}
\begin{tabular}{@{}llrrrr@{}}
\toprule
Computation & Leaf & Residual vertices & Residual edges & Local threshold $\tau_\ell$ & Colors used \\
\midrule
$J(13,5,3)$ & 16 & 96 & \num{3160} & 33 & 17 \\
$J(13,5,3)$ & 170 & 113 & \num{4524} & 32 & 26 \\
$J(13,5,3)$ & 169 & 124 & \num{5861} & 31 & 30 \\
$J(13,5,3)$ & 176 & 125 & \num{5769} & 31 & 30 \\
$J(13,5,3)$ & 173 & 128 & \num{6230} & 30 & 29 \\
$J(13,6,4)$ & 11 & 175 & \num{10185} & 46 & 36 \\
$J(13,6,4)$ & 170 & 216 & \num{16962} & 45 & 42 \\
\bottomrule
\end{tabular}
\end{table}

\begin{table}[htbp]
\centering
\caption{Proof-log statistics for nine of the 200 $J(13,5,3)$ leaves, among them the
smallest and the largest, sorted by residual vertex count $n_\ell$}\label{tab:proofs}
\small
\begin{tabular}{@{}lrrrrrrr@{}}
\toprule
Leaf & $n_\ell$ & Family (N) & $\tau_\ell$ & Search nodes & Proof-log size & Solve (\unit{\second}) & Check (\unit{\second}) \\
\midrule
16 & 96 & \num{1400} & 33 & 1 & \qty{4.71}{\kilo\byte} & $< 0.1$ & $< 0.1$ \\
170 & 113 & \num{1804} & 32 & 1 & \qty{4.33}{\kilo\byte} & $< 0.1$ & 0.1 \\
169 & 124 & \num{1765} & 31 & 3 & \qty{9.54}{\kilo\byte} & $< 0.1$ & $< 0.1$ \\
176 & 125 & \num{1981} & 31 & 5 & \qty{14.2}{\kilo\byte} & $< 0.1$ & $< 0.1$ \\
77 & 208 & \num{5372} & 29 & \num{5916} & \qty{12.3}{\mega\byte} & 0.5 & 0.3 \\
78 & 286 & \num{10449} & 30 & \num{303030} & \qty{604}{\mega\byte} & 10.1 & 16.1 \\
25 & 348 & \num{15914} & 29 & \num{5655159} & \qty{9.87}{\giga\byte} & 166.2 & 281.2 \\
1 & 404 & \num{21940} & 29 & \num{23208561} & \qty{42.2}{\giga\byte} & 664.5 & 1360.1 \\
10 & 466 & \num{28184} & 30 & \num{140108190} & \qty{274}{\giga\byte} & 4382.6 & 9062.6 \\
\bottomrule
\end{tabular}
\end{table}

Each coloring in \cref{tab:fragments} was re-verified as a proper coloring of the leaf's
residual graph with fewer colors than its local threshold. In \cref{tab:proofs},
family~(N) counts the at-most-one constraints of the leaf's formula, search nodes are
those of the Glasgow solver, and the solve and check columns give wall-clock times of the
solver and of VeriPB on the certification machine, rounded to \qty{0.1}{\second}.

\section{Delsarte bounds}\label{app:delsarte}

\begin{proposition}\label{prop:delsarte}
The independence numbers of the two graphs satisfy
\[
\alpha(J(13,5,3)) \le 58 \quad \text{and} \quad \alpha(J(13,6,4)) \le 78.
\]
\end{proposition}

\begin{proof}
Class $i$ of the Johnson scheme on the $k$-element subsets of $[13]$ holds the ordered
pairs of subsets that share $k - i$ elements. Adjacency in $J(13,k,t)$ is therefore class
$k - t$, and $k - t = 2$ for both graphs here. Let $v = \binom{13}{k}$, and let $P$ be
the first eigenmatrix of the scheme, with rows indexed by eigenspaces and columns indexed
by classes. Its entry in row $i$ and column $j$,
\[
P_j(i) = \sum_{h} (-1)^h \binom{i}{h} \binom{k-i}{j-h} \binom{13-k-i}{j-h},
\]
is the eigenvalue of class $j$ on the $i$-th eigenspace. The entries of the second
eigenmatrix are $Q_m(i) = \mu_m P_i(m)/v_i$, where $v_i = \binom{k}{i}\binom{13-k}{i}$ is
the valency of class $i$ and, since $2k \le 13$, $\mu_m = \binom{13}{m} - \binom{13}{m-1}$
is the dimension of the $m$-th eigenspace \cite{Delsarte1973}. For an independent set $S$
of $J(13,k,t)$, the numbers
$a_i = |\{(A,B) \in S^2 : (A,B) \text{ in class } i\}|/|S|$ satisfy $a_0 = 1$,
$a_{k-t} = 0$, $a_i \ge 0$ and $\sum_i a_i = |S|$. They also satisfy Delsarte's
inequalities $\sum_i a_i Q_m(i) \ge 0$ for $m = 0, \dots, k$ \cite{Delsarte1973}.
Maximizing $\sum_i a_i$ under these constraints is the Delsarte linear program. A dual
certificate is a vector $u = (u_1, \dots, u_k)$ with $u_m \ge 0$ and
\[
\sum_{m=1}^{k} u_m Q_m(i) \le -v \qquad \text{for every class } i \notin \{0, k-t\}.
\]
Multiplying the $m$-th Delsarte inequality by $u_m$ and summing over $m \ge 1$ gives
$0 \le \sum_m u_m \mu_m - v(|S| - 1)$, so
\[
\alpha(J(13,k,t)) \le 1 + \frac{1}{v} \sum_{m=1}^{k} u_m \mu_m .
\]

For $J(13,5,3)$ the certificate is $u = (9945/16, 117/2, 0, 0, 1755/16)$, and
\cref{tab:delsarte} lists the entries $Q_m(i)$ with $u_m \ne 0$.

\begin{table}[htbp]
\centering
\caption{The dual certificate $u$ for $J(13,5,3)$ and the entries $Q_m(i)$ of the
second eigenmatrix of the Johnson scheme on the 5-element subsets of $[13]$, for the
indices $m$ with $u_m \ne 0$; the adjacency class $i = 2$ is omitted, since
$a_2 = 0$}\label{tab:delsarte}
\small
\begin{tabular}{@{}rrrrrrr@{}}
\toprule
$m$ & $u_m$ & $Q_m(0) = \mu_m$ & $Q_m(1)$ & $Q_m(3)$ & $Q_m(4)$ & $Q_m(5)$ \\
\midrule
1 & $9945/16$ & 12 & $81/10$ & $3/10$ & $-18/5$ & $-15/2$ \\
2 & $117/2$ & 65 & $26$ & $-169/28$ & $13/14$ & $325/14$ \\
5 & $1755/16$ & 572 & $-143/2$ & $-143/14$ & $286/35$ & $-143/14$ \\
\bottomrule
\end{tabular}
\end{table}

The four constraint sums are $-1287$ at $i = 1, 3, 4$ and $-\num{70785}/16$ at $i = 5$, all at
most $-1287$, and
\[
1 + \tfrac{1}{1287}\bigl(12 \cdot \tfrac{9945}{16} + 65 \cdot \tfrac{117}{2}
+ 572 \cdot \tfrac{1755}{16}\bigr) = 1 + \tfrac{1}{1287} \cdot \tfrac{\num{148005}}{2}
= 1 + \tfrac{115}{2} = \tfrac{117}{2},
\]
so $\alpha(J(13,5,3)) \le 58$, since $\alpha$ is an integer. For $J(13,6,4)$ the
certificate is
\[
u = (702, 936/5, 0, 0, 78, 156);
\]
all five constraint sums equal $-1716$, and $1 + \num{132132}/1716 = 78$, so
$\alpha(J(13,6,4)) \le 78$ with no rounding step. A separate program checked both
certificates in exact rational arithmetic.
\end{proof}

The Delsarte linear programs, solved exactly, have the optima $117/2$ and 78, so they give no bound
below 58 and 78. Stronger relaxations, such as the semidefinite bound of
\textcite{Schrijver2005}, were not computed.

\end{document}