\documentclass[11pt]{amsart}
\pdfsuppressptexinfo=-1
\usepackage{amssymb,amsmath,mathtools}
\usepackage[margin=1.15in]{geometry}
\usepackage{booktabs}
\usepackage[hidelinks]{hyperref}

\newtheorem{theorem}{Theorem}[section]
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}

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

\hypersetup{pdftitle={The kissing numbers in dimensions five and seven are at most 43 and 132},pdfauthor={Tejasvi Singh Tomar}}

\title{The kissing numbers in dimensions five and seven are at most $43$ and $132$}
\author{Tejasvi Singh Tomar}
\date{}

\begin{document}
\begin{abstract}
The kissing number $\tau_n$ is the largest number of non-overlapping unit balls in $\R^n$ that can touch a common unit ball. The best bounds so far were $40\le\tau_5\le44$ and $126\le\tau_7\le134$; both upper bounds come from high-precision floating-point computations of the three-point bound by Mittelmann and Vallentin. We prove $\tau_5\le 43$ and $\tau_7\le132$. Each proof is an exact rational solution of the second level of the Lasserre hierarchy for spherical codes at degrees $(d_1,d_2,\delta)=(14,20,20)$. We use the formulation of de~Laat, Leijenhorst and de~Muinck Keizer and check the solutions with their verification program. Each certificate is obtained by rounding a convex combination of two dual iterates of the interior-point method, one on each side of the target value. Exact certificates for the same hierarchy also give $A(4,\arccos\frac13)\le14$, $A(5,\arccos\frac13)\le22$ and $A(6,\arccos\frac13)\le34$ for spherical codes, improving the previous bounds $15$, $23$ and $35$; with a known code, $A(4,\arccos\frac13)=14$. The largest number of points at angle $\pi/3$ from a point of a kissing configuration in $\R^n$ equals $A(n-1,\arccos\frac13)$, so in $\R^5$ this number is $14$. We also prove the five bounds in the Lean proof assistant, assuming only the positivity of the zonal kernels given by the zonal polynomial files: once by checking the exact certificates with compiled code, and once, with every computation done by Lean's kernel, from the certificates rounded to $30$ decimal places.
\end{abstract}
\maketitle

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

A kissing configuration in $\R^n$ is a set $C\subset S^{n-1}$ with $\langle x,y\rangle\le\frac12$ for all distinct $x,y\in C$, and the kissing number $\tau_n$ is the largest size of such a set. The values $\tau_1=2$ and $\tau_2=6$ are elementary, $\tau_3=12$ is due to Sch\"utte and van der Waerden~\cite{SvdW}, $\tau_4=24$ to Musin~\cite{Mus}, and $\tau_8=240$ and $\tau_{24}=196560$ to Odlyzko and Sloane~\cite{OS} and, independently, Levenshtein~\cite{Lev}.
In dimension five the root system $D_5$ (Korkine and Zolotareff~\cite{KZ}) gives $\tau_5\ge40$, and three further non-isometric $40$-point kissing configurations are known, found by Leech~\cite{Leech}, Sz\"oll\H{o}si~\cite{Sz} and Cohn and Rajagopal~\cite{CR}.
The linear programming bound gives $\tau_5\le46$~\cite{OS}, and the three-point semidefinite programming bound of Bachoc and Vallentin~\cite{BV} gives $\tau_5\le45$. Mittelmann and Vallentin~\cite{MV} computed the three-point bound in high-precision floating-point arithmetic and obtained $44.99899685\ldots$, so $\tau_5\le44$; three-point computations at higher degrees have since reached $44.981067$~\cite{MOF} and $44.970252$~\cite{LdL}.
In dimension seven the root system $E_7$ gives $\tau_7\ge126$. The three-point bound gives $\tau_7\le135$~\cite{BV}, and the computation of~\cite{MV} gives $134.4488169\ldots$, so $\tau_7\le134$.
De~Laat, Leijenhorst and de~Muinck Keizer~\cite{LLM} computed the second level of the Lasserre hierarchy at degrees $(14,16,16)$ in dimensions $5$, $6$, $7$, $10$, $12$ and $16$; it improved the known bounds only in dimension six, where it gives $\tau_6\le77$. See~\cite{Val} for a recent survey.

\begin{theorem}\label{thm:main}
$\tau_5\le 43$ and $\tau_7\le132$.
\end{theorem}

More generally, a spherical code with minimal angle $\theta$ is a finite set $C\subset S^{n-1}$ with $\langle x,y\rangle\le\cos\theta$ for all distinct $x,y\in C$, and $A(n,\theta)$ denotes the largest size of such a code; thus $\tau_n=A(n,\pi/3)$. Upper bounds for $A(n,\theta)$ come from linear programming (Delsarte, Goethals and Seidel~\cite{DGS}, Kabatiansky and Levenshtein~\cite{KL}) and from semidefinite programming. Bachoc and Vallentin~\cite{BV} tabulated the three-point bound for several dimensions and angles. For $\cos\theta=\frac13$ their table improved the upper bounds for $A(5,\theta)$ and $A(6,\theta)$ from $24$ and $37$ to $23$ and $35$ and matched the bound $A(4,\theta)\le15$; the bounds $15$ and $24$ are due to Boyvalenkov and Kazakov~\cite{BK}. The best known codes have $14$, $21$ and $32$ points (Section~\ref{sec:lower}). (The table of~\cite{BV} lists $20$ for $n=5$.) Before this work the known bounds were therefore
\[
14\le A(4,\theta)\le 15,\qquad 21\le A(5,\theta)\le 23,\qquad 32\le A(6,\theta)\le 35 .
\]
Cohn, de~Laat and Leijenhorst~\cite[Table~6.1]{CdLL} list the $32$-point code in $\R^6$ among the codes conjectured to be optimal.

\begin{theorem}\label{thm:cos13}
Let $\theta=\arccos\frac13$. Then $A(4,\theta)=14$, $A(5,\theta)\le22$ and $A(6,\theta)\le34$.
\end{theorem}

Together with the codes of Section~\ref{sec:lower}, Theorem~\ref{thm:cos13} gives $A(5,\theta)\in\{21,22\}$ and $32\le A(6,\theta)\le 34$.

For a kissing configuration $C\subset S^{n-1}$ and $x\in C$, call the points $y\in C$ with $\langle x,y\rangle=\frac12$ the contacts of~$x$. In the arrangement of unit balls centred at $0$ and at $2y$ for $y\in C$, the contacts of $x$ correspond to the outer balls that touch the ball centred at~$2x$. Let $c_n$ be the largest number of contacts of a point in a kissing configuration in~$\R^n$.

\begin{corollary}\label{cor:contact}
For every $n\ge2$ we have $c_n=A(n-1,\arccos\frac13)$. Hence $c_5=14$, $c_6\in\{21,22\}$ and $32\le c_7\le 34$.
\end{corollary}

The angle $\arccos\frac13$ enters through the tangent space at $x$: the normalised projections of two contacts of $x$ to $x^\perp$ have inner product at most $\frac13$, and conversely (Section~\ref{sec:contact}). This correspondence is classical; see for example~\cite[Section~4.1]{DdLM}. With the bounds of~\cite{BV} it gives $c_5\le15$, $c_6\le23$ and $c_7\le35$. Theorem~\ref{thm:cos13} and Corollary~\ref{cor:contact} were first published in~\cite{cos13}; they are included here because they come from the same method.

All upper bounds in this paper come from the second level of the Lasserre hierarchy for spherical codes, which de~Laat and Vallentin~\cite{dLV} defined and de~Laat, Leijenhorst and de~Muinck Keizer~\cite{LLM} reduced by symmetry. In each case we computed a numerical solution of their semidefinite program, rounded it to an exact rational solution and checked that solution with their verification program. Section~\ref{sec:method} recalls what a certificate consists of. Sections~\ref{sec:values}--\ref{sec:verify} treat $\tau_5$ and $\tau_7$: the floating-point values at increasing degrees, how the certificates were obtained, and how they were checked. Section~\ref{sec:certificates} lists the certificates for $\cos\theta=\frac13$, Section~\ref{sec:lower} recalls the lower bounds, Section~\ref{sec:contact} proves Corollary~\ref{cor:contact}, and Section~\ref{sec:lean} describes Lean proofs of the upper bounds in Theorems~\ref{thm:main} and~\ref{thm:cos13}, which assume that the zonal kernels are positive semidefinite. The first version of this paper, titled ``The kissing number in dimension five is at most $43$'', did not contain the bound for~$\tau_7$.

\section{The second level of the Lasserre hierarchy}\label{sec:method}

We use the second level of the Lasserre hierarchy for spherical codes~\cite{dLV} in the symmetry-reduced form of~\cite[Section~4]{LLM}, and refer there for details. Fix $n$ and $t=\cos\theta$. Call a set of points of $S^{n-1}$ admissible if their pairwise inner products lie in $[-1,t]$. The dual program asks for a positive semidefinite kernel $K$ on the admissible sets of at most two points, invariant under the orthogonal group. After the symmetry reduction, $K$ is given by positive semidefinite matrices $F_\lambda$, one for each partition $\lambda=(\lambda_1,\lambda_2)$ with $|\lambda|\le d_1$ that occurs, combined with the zonal matrices of~\cite{LLM}. For $k=1,2,3,4$ and every admissible set $S$ of $k$ points, the sum of $K(J_1,J_2)$ over all $J_1,J_2$ with $J_1\cup J_2=S$ must be at most $-1$ if $k=1$ and at most $0$ otherwise. These inequalities are imposed as polynomial identities in the inner products of $S$: the difference between the two sides is a sum of terms $c\,g\,r$, where $g$ runs through $1$ and the symmetrised polynomials that cut out the admissible Gram matrices, $c\ge0$ is a constant, $r$ is a sum of squares, and each term has degree at most~$\delta$. We call the requirement on the multipliers $c\,g$ the multiplier conditions. Every code $C$ with minimal angle $\theta$ then has at most $K(\emptyset,\emptyset)$ points: since $K$ is positive semidefinite, the sum of $K(J_1,J_2)$ over all subsets $J_1,J_2$ of $C$ with at most two points is nonnegative, and grouping its terms by $S=J_1\cup J_2$ bounds it by $K(\emptyset,\emptyset)-|C|$. The kernel $K$ is positive semidefinite because the matrices $F_\lambda$ are and the zonal matrices of~\cite{LLM} are Gram matrices. The value $K(\emptyset,\emptyset)$ is one entry of the matrix for the trivial representation. The degrees $d_1\le d_2$ determine the partitions $\lambda$ and the sizes of the matrices $F_\lambda$, and the even number $\delta\ge d_2$ bounds the degrees in the sums of squares.

A certificate consists of rational matrices $F_\lambda$ and rational Gram matrices for the sums of squares, in fixed polynomial bases, such that all of them are positive semidefinite and all identities hold exactly. The verification program of~\cite{LLM}, available with the data of that paper~\cite{LLMdata} and written in Julia~\cite{Julia} with Nemo~\cite{Nemo}, reads a certificate from files, checks that every matrix is positive definite by a Cholesky factorisation in ball arithmetic~\cite{Arb}, recomputes the four families of identities in exact rational arithmetic, and compares $K(\emptyset,\emptyset)$ with the claimed bound.

\section{Floating-point values}\label{sec:values}

Table~\ref{tab:values} lists numerical values of the relaxation for $\tau_5$ and $\tau_7$ ($t=\frac12$) at increasing degrees. They are not part of the proof. We computed them in $128$- or $256$-bit floating-point arithmetic with a version of the interior-point solver of~\cite{LdL} that we had modified for speed. Raising $d_1$ from $14$ to $16$ at $\delta=16$ lowers the value for $\tau_5$ by only $0.0037$. At $d_1=14$, the steps of $\delta$ from $14$ to $16$, from $16$ to $18$ and from $18$ to $20$ lower it by $0.70$, $0.32$ and $0.22$ for $\tau_5$ and by $3.00$, $2.17$ and $1.22$ for $\tau_7$. The value for $\tau_7$ at $\delta=16$ is still above the three-point value $134.45$, in line with~\cite{LLM}.

\begin{table}[ht]
\centering
\begin{tabular}{ccc}
\toprule
$(d_1,d_2,\delta)$ & $n=5$ & $n=7$ \\
\midrule
$(10,10,10)$ & $46.3376$ & \\
$(12,12,12)$ & $46.3052$ & $140.1624$ \\
$(14,14,14)$ & $45.0529$ & $138.6072$ \\
$(14,16,16)$ & $44.3547$ & $135.6085$ \\
$(16,16,16)$ & $44.3511$ & \\
$(14,18,18)$ & $44.0314$ & $133.4419$ \\
$(14,20,20)$ & $43.8154$ & $132.2202$ \\
\bottomrule
\end{tabular}
\medskip
\caption{Dual objective at the end of the interior-point runs for the second level of the Lasserre hierarchy for $\tau_5$ and $\tau_7$, rounded to four decimals. Empty entries were not computed.}\label{tab:values}
\end{table}

\section{The certificates for \texorpdfstring{$\tau_5$}{tau5} and \texorpdfstring{$\tau_7$}{tau7}}\label{sec:cert}

As in~\cite[Section~5.2]{LLM}, where $\tau_6\le77$ was obtained by fixing the objective at $77.85$, just above the numerical optimum, we fix a target value: $N=\frac{4399}{100}$ for $\tau_5$ and $N=\frac{13299}{100}$ for $\tau_7$. An exact rational solution of the relaxation with all matrices positive semidefinite and $K(\emptyset,\emptyset)=N$ proves $\tau_n\le\lfloor N\rfloor$. We obtained one in each case by rounding a numerical solution.

For $\tau_5$ a direct interior-point solve of this feasibility problem stalled, and for both bounds we used two iterates of the optimization run instead. Since $K(\emptyset,\emptyset)$ is a linear function of the matrices, the convex combination
\[
W=(1-\gamma)\,Y_A+\gamma\,Y_B,\qquad \gamma=\frac{b_A-N}{b_A-b_B},
\]
of two dual iterates $Y_A,Y_B$ with values $b_A>N>b_B$ satisfies all identities up to the residuals of $Y_A$ and $Y_B$, has $K(\emptyset,\emptyset)=N$, and is positive definite because $Y_A$ and $Y_B$ are. We obtained $Y_A$ and $Y_B$ from two iterates of the run by one further step each in $256$-bit arithmetic, which reduces the dual residuals further. Table~\ref{tab:certs} lists the iterates and their dual residuals, the values $b_A$ and $b_B$, and the smallest eigenvalue of $W$ after each block is scaled to unit diagonal. In both cases $1-\gamma$ is tiny, and $W$ is essentially $Y_B$ with its value raised to~$N$. For $\tau_5$ the extra step lowered the dual objective from the value $43.8154$ in Table~\ref{tab:values} to $b_B$.

\begin{table}[ht]
\centering
\begin{tabular}{lcc}
\toprule
 & $\tau_5$ & $\tau_7$ \\
\midrule
target $N$ & $4399/100$ & $13299/100$ \\
iterates giving $Y_A$ and $Y_B$ & $96$, $117$ & $99$, $132$ \\
their dual residuals & $1\cdot10^{-17}$, $1\cdot10^{-18}$ & $2\cdot10^{-17}$, $3\cdot10^{-18}$ \\
$b_A$ & $3.09\cdot10^{5}$ & $3.06\cdot10^{9}$ \\
$b_B$ & $43.8128$ & $132.2202$ \\
$1-\gamma$ & $5.7\cdot10^{-7}$ & $2.5\cdot10^{-10}$ \\
smallest scaled eigenvalue of $W$ & $8\cdot10^{-11}$ & $1\cdot10^{-10}$ \\
successful rounding run (of which exact correction) & 8 h (5 h) & 7 h (5 h) \\
size of the certificate files & 2.3 GB & 2.1 GB \\
\midrule
check: positive definiteness & 1 min & 1 min \\
check: transformation to the bases of the identities & 3 h & 5 h \\
check: identities for $k\le3$ & 28 min & 14 min \\
check: identity for $k=4$ & 23 h & 37 h \\
check: peak memory & 410 GB & 720 GB \\
\bottomrule
\end{tabular}
\medskip
\caption{The certificates for $\tau_5$ and $\tau_7$. Times are approximate wall-clock times. The times and the memory of the check are those of the run described in Section~\ref{sec:verify}.}\label{tab:certs}
\end{table}

We rounded $W$ with the procedure of Cohn, de~Laat and Leijenhorst~\cite{CdLL}: the entries are approximated by rationals, and a subset of the entries is corrected by an exact linear solve so that all identities hold exactly. In both cases the identities amount to $11172$ linear equations in the $2666855$ entries on and above the diagonals of the matrices. For $\tau_5$ we allowed $255452$ entries to change: all entries of the matrices $F_\lambda$ and of the Gram matrices for $k\le3$, the diagonal and superdiagonal of the Gram matrices for $k=4$, and further entries chosen at random. For $\tau_7$ this rule gave a system without a solution modulo two random primes for every number of random entries we tried, up to $300140$ entries in total. We then added entries in batches of $100000$ until the system had a solution modulo a random prime: first the entries that the rule always keeps, together with $45644$ entries of the Gram matrices for $k=4$ whose two basis polynomials have the largest degree sum, $20$, and then random entries of the Gram matrices for $k=4$. Two batches were needed. In both cases the correction is the minimum-norm solution on $11731$ of the allowed entries. All matrices stayed positive definite, so no change of basis was needed.

\section{Verification of the certificates}\label{sec:verify}

All runs in this section use the package~\cite{LLMdata} without modification unless stated otherwise. On the certificate for $\tau_5$ the verification program of~\cite{LLM}, run on the files in~\cite{supp5}, reports that every spherical code in dimension $5$ with pairwise cosine at most $\frac12$ has at most $\frac{4399}{100}$ points, and on the certificate for $\tau_7$ it reports the same for dimension $7$ with the bound $\frac{13299}{100}$.\footnote{The output is ``Verified that any spherical code with pairwise cosine at most 1//2 in dimension 5 contains at most 4399//100 points.'', and the same with $7$ and 13299//100. The program uses auxiliary files (about $130$~GB) to make missing zonal polynomial files and does not read them when, as here, all the zonal polynomial files are present. For the runs above we reused them from an earlier run. A copy of the package changed only to skip computing them gave the same result on each certificate.} The checks read the zonal polynomial files of the supplement~\cite{supp5}, which we computed with the same package. For $n=5$ and for $n=7$ we also recomputed the $490$ files that each check reads, starting from an empty cache, and obtained identical files. Since $\tau_5$ and $\tau_7$ are integers, this proves Theorem~\ref{thm:main}.

Table~\ref{tab:certs} lists the time of each part of the check and its memory use. Section~\ref{sec:lean} describes a second check of the certificates in Lean.

\section{The certificates for \texorpdfstring{$\cos\theta=\frac13$}{cos theta = 1/3}}\label{sec:certificates}

Table~\ref{tab:cert} lists the three certificates for Theorem~\ref{thm:cos13}. For each case we solved the semidefinite program numerically in multiple-precision arithmetic, with the modified solver of Section~\ref{sec:values}. The objective was replaced by the constraint $K(\emptyset,\emptyset)=N$ for the value $N$ in the table, which lies above the numerical optimum. This feasibility problem then has solutions with positive definite matrices, and the interior-point method returns one. We rounded it with the procedure of~\cite{CdLL}. Here too all matrices stayed positive definite.

\begin{table}[ht]
\centering
\begin{tabular}{ccccccc}
\toprule
$n$ & previous bound & $(d_1,d_2,\delta)$ & level-2 value & certificate $N$ & conclusion \\
\midrule
$4$ & $15$ & $(12,12,12)$ & $14.9213$ & $1499/100$ & $A(4,\theta)\le14$\\
$5$ & $23$ & $(12,12,12)$ & $22.9177$ & $459/20$ & $A(5,\theta)\le22$\\
$6$ & $35$ & $(14,16,16)$ & $34.2444$ & $349/10$ & $A(6,\theta)\le34$\\
\bottomrule
\end{tabular}
\medskip
\caption{Certificates for $\cos\theta=\frac13$. The level-2 value is the floating-point optimum of the semidefinite program at the given degrees. Each certificate was checked by the verification program of~\cite{LLM}, which reports that every code with these parameters has at most $N$ points.}\label{tab:cert}
\end{table}

Since $A(n,\theta)$ is an integer, the certificates give the upper bounds of Theorem~\ref{thm:cos13}.

\begin{remark}
We also computed the three-point bound of~\cite{BV} for $n=4$ in floating-point arithmetic. It is $14.9903$ at degree $12$ and $14.9825$ at degree~$14$, so at these degrees the three-point bound also points to $A(4,\theta)\le14$. What we add in this case is an exact certificate. For $n=5$ the second level at the degrees $(14,16,16)$ gives $22.4748$, so these degrees give no further improvement.
\end{remark}

\section{Lower bounds}\label{sec:lower}

Codes of size $14$ in $\R^4$ and of size $21$ in $\R^5$ with minimal angle larger than $\arccos\frac13$ are listed in~\cite{Sl}, and the $32$ unit vectors along $16$ equiangular lines in $\R^6$ with angle $\arccos\frac13$~\cite{vLS} form a code of minimal angle $\arccos\frac13$. For completeness the supplement~\cite{supp13} contains a $14$-point code in $S^3$ and a $21$-point code in $S^4$ with rational coordinates, obtained by inverse stereographic projection of rational points. Their largest pairwise inner products are $0.32094\ldots$ and $0.31622\ldots$, both less than $\frac13$; we checked this in exact arithmetic. Together with the certificate for $n=4$ this proves $A(4,\theta)=14$.

\section{Contact numbers}\label{sec:contact}

\begin{proof}[Proof of Corollary~\ref{cor:contact}]
Let $C\subset S^{n-1}$ be a kissing configuration and $x\in C$. Every contact $y$ of $x$ can be written as $y=\frac12x+\frac{\sqrt3}{2}y'$ with $y'\in S^{n-1}$ orthogonal to~$x$. For two distinct contacts $y,z$ we get
\[
\langle y,z\rangle=\tfrac14+\tfrac34\langle y',z'\rangle\le\tfrac12 ,
\]
so $\langle y',z'\rangle\le\frac13$. Hence the points $y'$ form a code with minimal angle $\arccos\frac13$ in the unit sphere of $x^\perp\cong\R^{n-1}$, and $x$ has at most $A(n-1,\arccos\frac13)$ contacts. Conversely, let $x\in S^{n-1}$ and let $D$ be a code with minimal angle $\arccos\frac13$ in the unit sphere of~$x^\perp$. The same computation shows that $\{x\}\cup\{\frac12x+\frac{\sqrt3}{2}y':y'\in D\}$ is a kissing configuration in which $x$ has $|D|$ contacts. So $c_n=A(n-1,\arccos\frac13)$, and Theorem~\ref{thm:cos13} together with the lower bounds of Section~\ref{sec:lower} gives the values for $n=5,6,7$.
\end{proof}

\section{Lean proofs}\label{sec:lean}

We also checked the two certificates of Section~\ref{sec:cert} and the three certificates of Table~\ref{tab:cert} in the Lean~4 proof assistant with the Mathlib library. For $(n,t,N)=(5,\frac12,43)$, $(7,\frac12,132)$, $(4,\frac13,14)$, $(5,\frac13,22)$ and $(6,\frac13,34)$ the Lean theorem states: if $\mathrm{ZonalPSD}(n,d_1,d_2)$ holds, then every finite set of unit vectors in $\R^n$ with pairwise inner products at most $t$ has at most $N$ elements. Here $d_1$ and $d_2$ are the degrees of the certificate, and $\mathrm{ZonalPSD}(n,d_1,d_2)$ says that for every partition $\lambda$ with $|\lambda|\le d_1$ that occurs, the matrix kernel $(J,J')\mapsto\hat Z_\lambda(J,J')$ built from the zonal polynomial files computed with the program of~\cite{LLMdata} is positive semidefinite on every finite family of ordered lists of at most two points of $S^{n-1}$, in which points may repeat (a one-point list $(y)$ is evaluated as the pair $(y,y)$, as in the verification program). In~\cite{LLM} the zonal matrices are Gram matrices, $Z_\lambda(J_1,J_2)_{\ell_1,\ell_2}=\langle\psi_{\lambda,\ell_1}(J_1),\psi_{\lambda,\ell_2}(J_2)\rangle$, so $\mathrm{ZonalPSD}(n,d_1,d_2)$ holds if the zonal files express these matrices correctly. This property of the zonal files is not formalized. Weak duality for the second level of the hierarchy, the nonnegativity of the weights on Gram matrices of codes, and the bookkeeping that turns sums over pairs $J_1,J_2$ into the identities checked by the verification program are proved in Lean.

There are two versions of the finite checks on a certificate (positive semidefiniteness of every matrix, the multiplier conditions, the four identities, and a symmetry of the zonal data). In the first, they are decided on the exact certificates by compiled code through Lean's \texttt{native\_decide}, so the Lean compiler is part of the trusted base. This version builds in about four hours of wall time. In the second, every check is done by the Lean kernel, and the five theorems depend only on Lean's standard axioms. To keep the kernel computations small, this version uses the certificate matrices rounded to $30$ decimal places. Lean checks that they are still positive semidefinite, through a diagonally dominant decomposition, but they satisfy the identities only up to explicit residual polynomials $r_k$ (stored in Lean as integer polynomials $L_kr_k$). A version of weak duality with residuals, also proved in Lean, gives $|C|\le K(\emptyset,\emptyset)+\sum_{k=1}^4\binom{|C|}{k}\|r_k\|_1$ for every code $C$, where $\|r\|_1$ is the sum of the absolute values of the coefficients of $r$. The bound on the residual terms uses only that the inner products of unit vectors lie in $[-1,1]$. If a code had more than $M$ points, the inequality applied to $M+1$ of them would give $M+1\le K(\emptyset,\emptyset)+\sum_k\binom{M+1}{k}\|r_k\|_1$. For the certificates of Theorem~\ref{thm:main}, with $M=43$ and $M=132$, the right-hand side is less than $M+1$: the residual terms are about $2\cdot10^{-9}$ and $9\cdot10^{-9}$, and $K(\emptyset,\emptyset)$ is $\frac{4399}{100}$ and $\frac{13299}{100}$. The kernel checks pack vectors of integers into single natural numbers, so that most of the work is done by the kernel's built-in arithmetic on large numbers, and they are split into pieces that fit in memory. For the certificates of Theorem~\ref{thm:main} they take about $78$ and $76$ hours, summed over the single-threaded checks. The largest single check, positive semidefiniteness of the largest block (of size $1040$), takes about $7$ hours and $330$~GB of memory for each of the two certificates. %

As a numerical check of $\mathrm{ZonalPSD}(n,d_1,d_2)$ we evaluated the kernels on random families of subsets of $S^{n-1}$ (in total $1840$, $1104$ and $960$ block matrices for the three certificates with $\cos\theta=\frac13$, and $960$ for each of $n=5$ and $n=7$ with $d_1=14$); the smallest eigenvalue relative to $\max(1,\lambda_{\max})$ was never below $-10^{-13}$, while in control runs on further families, multiplying a single zonal coefficient by $-3$ produced clearly negative eigenvalues in every family.

\section*{Data availability}
The certificates for Theorem~\ref{thm:main} (in the file format of the verification program of~\cite{LLMdata}), the zonal polynomial files they use, the code that produced them and the Lean files of Section~\ref{sec:lean} are in~\cite{supp5}. The certificates for Theorem~\ref{thm:cos13}, the codes of Section~\ref{sec:lower} and a script that checks them in exact arithmetic are in~\cite{supp13}.

\section*{Acknowledgements}
Generative AI tools were used to write code, run analyses and draft text; the author directed the work and takes full responsibility for its content.

\begin{thebibliography}{99}
\bibitem{BV} C.~Bachoc and F.~Vallentin, \emph{New upper bounds for kissing numbers from semidefinite programming}, J. Amer. Math. Soc. \textbf{21} (2008), 909--924.
\bibitem{Julia} J.~Bezanson, A.~Edelman, S.~Karpinski and V.~B.~Shah, \emph{Julia: a fresh approach to numerical computing}, SIAM Rev. \textbf{59} (2017), 65--98.
\bibitem{BK} P.~Boyvalenkov and P.~Kazakov, \emph{New upper bounds for some spherical codes}, Serdica Math. J. \textbf{21} (1995), 231--238.
\bibitem{CdLL} H.~Cohn, D.~de~Laat and N.~Leijenhorst, \emph{Optimality of spherical codes via exact semidefinite programming bounds}, arXiv:2403.16874 (2024).
\bibitem{CR} H.~Cohn and I.~Rajagopal, \emph{Variations on five-dimensional sphere packings}, Discrete Comput. Geom. \textbf{76} (2026), 1660--1678.
\bibitem{DGS} P.~Delsarte, J.~M.~Goethals and J.~J.~Seidel, \emph{Spherical codes and designs}, Geom. Dedicata \textbf{6} (1977), 363--388.
\bibitem{DdLM} M.~Dostert, D.~de~Laat and P.~Moustrou, \emph{Exact semidefinite programming bounds for packing problems}, SIAM J. Optim. \textbf{31} (2021), 1433--1458.
\bibitem{Nemo} C.~Fieker, W.~Hart, T.~Hofmann and F.~Johansson, \emph{Nemo/Hecke: computer algebra and number theory packages for the Julia programming language}, in: Proc. ISSAC 2017, ACM, 2017, 157--164.
\bibitem{Arb} F.~Johansson, \emph{Arb: efficient arbitrary-precision midpoint-radius interval arithmetic}, IEEE Trans. Comput. \textbf{66} (2017), 1281--1292.
\bibitem{KL} G.~A.~Kabatiansky and V.~I.~Levenshtein, \emph{On bounds for packings on a sphere and in space}, Problems Inform. Transmission \textbf{14} (1978), 1--17.
\bibitem{KZ} A.~Korkine and G.~Zolotareff, \emph{Sur les formes quadratiques}, Math. Ann. \textbf{6} (1873), 366--389.
\bibitem{dLV} D.~de~Laat and F.~Vallentin, \emph{A semidefinite programming hierarchy for packing problems in discrete geometry}, Math. Program. \textbf{151} (2015), 529--553.
\bibitem{LLM} D.~de~Laat, N.~Leijenhorst and W.~H.~H.~de~Muinck Keizer, \emph{Optimality and uniqueness of the $D_4$ root system}, arXiv:2404.18794 (2024).
\bibitem{LLMdata} D.~de~Laat, N.~Leijenhorst and W.~H.~H.~de~Muinck Keizer, \emph{Data for ``Optimality and uniqueness of the $D_4$ root system''}, 4TU.ResearchData (2024), \href{https://doi.org/10.4121/74ce1c25-6fca-4680-8a36-e9c18e7e9594.v1}{doi:10.4121/74ce1c25-6fca-4680-8a36-e9c18e7e9594.v1}.
\bibitem{Leech} J.~Leech, \emph{Five dimensional non-lattice sphere packings}, Canad. Math. Bull. \textbf{10} (1967), 387--393.
\bibitem{LdL} N.~Leijenhorst and D.~de~Laat, \emph{Solving clustered low-rank semidefinite programs arising from polynomial optimization}, Math. Program. Comput. \textbf{16} (2024), 503--534.
\bibitem{Lev} V.~I.~Levenshtein, \emph{On bounds for packings in $n$-dimensional Euclidean space}, Dokl. Akad. Nauk SSSR \textbf{245} (1979), 1299--1303; English transl., Soviet Math. Dokl. \textbf{20} (1979), 417--421.
\bibitem{MOF} F.~C.~Machado and F.~M.~de~Oliveira Filho, \emph{Improving the semidefinite programming bound for the kissing number by exploiting polynomial symmetry}, Experiment. Math. \textbf{27} (2018), 362--369.
\bibitem{MV} H.~D.~Mittelmann and F.~Vallentin, \emph{High accuracy semidefinite programming bounds for kissing numbers}, Experiment. Math. \textbf{19} (2010), 175--179.
\bibitem{Mus} O.~R.~Musin, \emph{The kissing number in four dimensions}, Ann. of Math. \textbf{168} (2008), 1--32.
\bibitem{OS} A.~M.~Odlyzko and N.~J.~A.~Sloane, \emph{New bounds on the number of unit spheres that can touch a unit sphere in $n$ dimensions}, J. Combin. Theory Ser. A \textbf{26} (1979), 210--214.
\bibitem{SvdW} K.~Sch\"utte and B.~L.~van der Waerden, \emph{Das Problem der dreizehn Kugeln}, Math. Ann. \textbf{125} (1953), 325--334.
\bibitem{Sl} N.~J.~A.~Sloane, with the collaboration of R.~H.~Hardin, W.~D.~Smith and others, \emph{Tables of spherical codes}, \url{http://neilsloane.com/packings/}.
\bibitem{Sz} F.~Sz\"oll\H{o}si, \emph{A note on five dimensional kissing arrangements}, Math. Res. Lett. \textbf{30} (2023), 1609--1615.
\bibitem{cos13} T.~S.~Tomar, \emph{Spherical codes with minimal angle $\arccos(1/3)$ in dimensions four, five and six}, Zenodo (2026), \href{https://doi.org/10.5281/zenodo.23603435}{doi:10.5281/zenodo.23603435}.
\bibitem{supp5} T.~S.~Tomar, \emph{Supplementary files for ``The kissing numbers in dimensions five and seven are at most $43$ and $132$''}, Zenodo (2026), \href{https://doi.org/10.5281/zenodo.23992399}{doi:10.5281/zenodo.23992399}.
\bibitem{supp13} T.~S.~Tomar, \emph{Supplementary files for ``Spherical codes with minimal angle $\arccos(1/3)$ in dimensions four, five and six''}, Zenodo (2026), \href{https://doi.org/10.5281/zenodo.23603429}{doi:10.5281/zenodo.23603429}.
\bibitem{Val} F.~Vallentin, \emph{Conic optimization for extremal geometry}, in: Proceedings of the International Congress of Mathematicians 2026, Vol.~7, SIAM, 2026, 229--248.
\bibitem{vLS} J.~H.~van Lint and J.~J.~Seidel, \emph{Equilateral point sets in elliptic geometry}, Indag. Math. \textbf{28} (1966), 335--348.
\end{thebibliography}

\end{document}