\documentclass[11pt]{amsart}
\pdfsuppressptexinfo=-1
\usepackage{amssymb,amsmath,mathtools}
\usepackage[margin=1.15in]{geometry}
\usepackage{booktabs,array}
\newcolumntype{L}[1]{>{\raggedright\arraybackslash}p{#1}}
\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}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}

\newcommand{\R}{\mathbb{R}}
\newcommand{\vol}{\operatorname{vol}}
\newcommand{\Tt}{T_3}
\newcommand{\Hs}{\mathcal H}
\newcommand{\conv}{\operatorname{conv}}

% DOI of the version of the supplement cited as [supp]
\newcommand{\suppdoi}{10.5281/zenodo.23720965}

\hypersetup{pdftitle={The 24-cell conjecture in the all-contact case and near D4},pdfauthor={Tejasvi Singh Tomar}}

\title{The 24-cell conjecture in the all-contact case and near $D_4$}
\author{Tejasvi Singh Tomar}
\date{}
\subjclass[2020]{Primary 52C17; Secondary 52B11, 90C22, 11H31, 68V20}
\keywords{24-cell conjecture, sphere packing, Voronoi cell, kissing configuration, Lasserre hierarchy, formal verification}



\begin{document}
\begin{abstract}
The 24-cell conjecture states that every Voronoi cell of a packing of unit balls in $\R^4$ has volume at least~$8$, the volume of the regular 24-cell. It implies that no packing of equal balls in $\R^4$ is denser than the lattice packing $D_4$. We prove the conjecture for two classes of cells; in each class, equality holds only for the $D_4$ root configuration. The first consists of the cells whose ball touches every ball centred at distance less than $2\sqrt2$ from its centre, and its proof uses a certificate at the second level of the Lasserre hierarchy. The second consists of the cells whose $24$ nearest centres lie in an explicit neighbourhood of the $D_4$ configuration, whatever the other centres are. For them the volume is at least $8$ plus a fixed multiple of the total outward displacement of the $24$ centres, which we prove by a quantitative rigidity estimate and a second-order expansion of the volume about $D_4$. Our proofs for both classes are computer-assisted and partly formalised in Lean.
\end{abstract}
\maketitle

\section{Introduction}

Let $\mathcal P\subset\R^4$ be the set of centres of a packing of unit balls, so that distinct centres are at distance at least~$2$. The Voronoi cell of $c\in\mathcal P$ is
\[
V_c=\{x\in\R^4:\ |x-c|\le |x-y| \text{ for all } y\in\mathcal P\}.
\]
For the lattice $D_4$, scaled to minimal distance~$2$, every Voronoi cell is a regular 24-cell with inradius~$1$ and volume~$8$. The \emph{24-cell conjecture} states that $\vol(V_c)\ge 8$ for every packing and every centre.

The conjecture implies that the density of a packing of equal balls in $\R^4$ is at most $\pi^2/16$, the density of $D_4$, so that $D_4$ would be the densest packing in $\R^4$~\cite{Mus18}. Among lattice packings this was proved by Korkine and Zolotareff~\cite{KZ}, while for general packings the best proved upper bound on the density is $0.63611$, from the three-point bounds of Cohn, de~Laat and Salmon~\cite{CdLS}. In dimension three the analogous volume statement for the densest lattice packing is false: by the dodecahedral theorem of Hales and McLaughlin~\cite{HM}, the smallest Voronoi cell of a packing of unit balls is the regular dodecahedron of inradius~$1$, not the cell of the face-centred cubic lattice~\cite{Mus18}. A proof of the full conjecture has been announced by Bhattacharjee, Bhattacharya, Mandal and Bhattacharya~\cite{BBMB}. The subsection at the end of this section relates our results to it and to their later draft~\cite{BBMBd}.

The centres that touch a given ball form a kissing configuration. In dimension~$4$ the kissing number is $24$, the number of contacts in $D_4$, by Musin's theorem~\cite{Mus}, and the configuration of $24$ contact points is unique up to isometry~\cite{LLdMK}. Musin~\cite{Mus18} proposed to approach the conjecture itself by semidefinite bounds for the centres around a given one, extending those for spherical codes, together with isoperimetric inequalities for polyhedra. Our proof of Theorem~\ref{thm:main} below combines the two kissing theorems with the semidefinite part of this proposal.

The conjecture is sharp at $D_4$, where the $24$ nearest centres touch the central ball and every other centre is at distance at least $2\sqrt2$. Our first result treats the cells in which, as in $D_4$, every centre at distance less than $2\sqrt2$ touches the central ball.

\begin{theorem}\label{thm:main}
Let $c\in\mathcal P$, and suppose that every centre $y\in\mathcal P$ with $0<|y-c|<2\sqrt2$ satisfies $|y-c|=2$. Then $\vol(V_c)\ge 8$, with equality if and only if the centres at distance~$2$ from $c$ form a translate of a $D_4$ root system scaled by~$\sqrt2$.
\end{theorem}

The proof bounds $\vol(V_c)$ from below by a quantity $\Tt$, obtained from the caps that the neighbouring centres cut from the ball $B=B(c,\sqrt2)$ by inclusion--exclusion truncated at the third order. For contact configurations, $\Tt$ depends only on the kissing configuration $C\subset S^3$ of contact directions. An exact certificate for the second level of the Lasserre hierarchy, in the form developed by de~Laat, Leijenhorst and de~Muinck Keizer~\cite{LLdMK}, together with interval bounds for the polynomial approximations it uses, shows $\Tt(C)>8$ whenever $|C|\le23$. The two kissing theorems recalled above dispose of $|C|\ge24$. We also show that, for every packing, no point of $B$ lies in five caps (Proposition~\ref{prop:four}), which identifies the loss in this bound exactly.

Our second result concerns configurations close to that of $D_4$. Let $u_1,\dots,u_{24}$ be the vectors of the $D_4$ root system scaled to unit length. For unit vectors $W=(w_1,\dots,w_{24})$ put
\[
d(W)=\min_{R\in O(4)}\ \min_{\pi}\ \Bigl(\sum_{i=1}^{24}|w_{\pi(i)}-Ru_i|^2\Bigr)^{1/2},
\]
the minimum over orthogonal maps $R$ and permutations $\pi$ of $\{1,\dots,24\}$.

\begin{theorem}\label{thm:local}
Let $c\in\mathcal P$, and let $y_1,\dots,y_{24}\in\mathcal P\setminus\{c\}$ be distinct. Put $\delta_i=|y_i-c|-2$ and $w_i=(y_i-c)/|y_i-c|$, and suppose that
\[
d(W)\le\tfrac25\qquad\text{and}\qquad\sum_{i=1}^{24}\delta_i\le\tfrac3{100} .
\]
Then
\[
\vol(V_c)\ \ge\ 8+0.2437\cdot\frac12\sum_{i=1}^{24}\delta_i .
\]
In particular $\vol(V_c)\ge8$, with equality if and only if $\{y_1-c,\dots,y_{24}-c\}=2R\{u_1,\dots,u_{24}\}$ for some $R\in O(4)$. In that case $V_c$ is the regular 24-cell cut out by these $24$ centres.
\end{theorem}

The packing condition gives $\delta_i\ge0$, and nothing is assumed about the other centres of $\mathcal P$. The bound $d(W)\le\frac25$ only starts the rigidity argument, which then confines $d(W)$ below $0.022$; in particular, $y_1,\dots,y_{24}$ are the $24$ centres nearest to $c$ (Remark~\ref{rem:effective}). The proof shows that the first-order gain from the outward displacement outweighs all losses (Section~\ref{sec:local} begins with an outline).

We develop the truncated bound in Section~\ref{sec:trunc}, give the certificate in Section~\ref{sec:cert}, control its polynomial approximations in Section~\ref{sec:approx} and complete the proof of Theorem~\ref{thm:main} in Section~\ref{sec:proof}. Section~\ref{sec:remarks} contains remarks on the relaxation, and we prove Theorem~\ref{thm:local} in Section~\ref{sec:local}. Results marked \emph{computer-assisted} rest on finite computations, which Section~\ref{sec:lean} describes together with the parts of both proofs that are formalised in Lean. Appendix~\ref{app:proofs} contains the longer proofs of Section~\ref{sec:local}.

\subsection*{\texorpdfstring{Relation to~\cite{BBMB} and~\cite{BBMBd}}{Relation to [2] and [3]}}
The proof of the full conjecture announced in~\cite{BBMB} treats cells according to their number of contacts, using a covering estimate, a semidefinite certificate and the uniqueness of the $D_4$ root system. The later public draft~\cite{BBMBd} states the bound for every cell except those with $24$ to $27$ other centres within distance~$\sqrt6$ of the centre, not all at distance~$2$. For part of this excluded class it has further results, among them a local result near $D_4$ and the bound for the $24$ centres of the root configuration pushed outwards along their own directions.

The statement of~\cite{BBMBd} covers the cells of Theorem~\ref{thm:main}, for which we give an independent proof, based on an exact certificate for the second level of the Lasserre hierarchy. The configurations of Theorem~\ref{thm:local} with $\sum_i\delta_i>0$ lie in the excluded class (Remark~\ref{rem:effective}). Theorem~\ref{thm:local} contains the local result of~\cite{BBMBd}, allows a total outward displacement $7.5$ times larger and gives an explicit linear bound.

From~\cite{BBMB} we take the truncated inclusion--exclusion bound and its value at $D_4$, which we reprove in Section~\ref{sec:trunc}; the distance $d(W)$; and the rigidity operator of the $D_4$ contact graph with its constant stress (Lemma~\ref{lem:Lambda}) and its spectrum, which we recheck. From~\cite{BBMBd} we take the inversion hull (Lemma~\ref{lem:hull}) and the rigidity argument with slack (Lemma~\ref{lem:rigid}).

\section{The truncated cell}\label{sec:trunc}

Fix a packing and translate so that $c=0$. Let $B=\{x:|x|<\sqrt2\}$. For a centre $y\ne0$ put
\[
H_y=\{x:\ \langle x,y\rangle>|y|^2/2\}=\{x:\ |x-y|<|x|\},\qquad K_y=H_y\cap B .
\]
Since $V_0$ is closed and each $H_y$ is open, $V_0=\R^4\setminus\bigcup_y H_y$, so $V_0\cap B=B\setminus\bigcup_y K_y$. If $|y|\ge 2\sqrt2$, then every $x\in H_y$ has $|x|\ge\langle x,y\rangle/|y|>|y|/2\ge\sqrt2$, so $K_y=\emptyset$. Write $Y$ for the finite set of centres with $0<|y|<2\sqrt2$, and let $S_k$ be the sum, over all $k$-element subsets of $Y$, of the volumes of the intersections of the corresponding caps.

\begin{proposition}\label{prop:four}
No point of $B$ lies in five of the sets $K_y$. Consequently
\[
\vol(V_0\cap B)=2\pi^2-S_1+S_2-S_3+S_4 .
\]
\end{proposition}

\begin{proof}
Let $x\in B$ lie in $K_{y_1},\dots,K_{y_m}$, and put $p_0=0$ and $p_i=y_i$. Each $p_i$ satisfies $|p_i-x|\le |x|$, and $|p_i-p_j|\ge2$ for $i\ne j$. Hence
\[
\langle p_i-x,\,p_j-x\rangle=\tfrac12\bigl(|p_i-x|^2+|p_j-x|^2-|p_i-p_j|^2\bigr)\le |x|^2-2<0 .
\]
The $m+1$ vectors $p_i-x$ are nonzero and have pairwise negative inner products. In $\R^4$ there are at most five such vectors, so $m\le4$. Inclusion--exclusion over the caps covering a point therefore ends at order four, and $\vol(B)=2\pi^2$.
\end{proof}

Put
\[
\Tt(Y)=2\pi^2-S_1+S_2-S_3 .
\]
Since at most four caps meet, $S_4$ is the volume of the set of points of $B$ that lie in four caps.

\begin{corollary}\label{cor:loss}
$\vol(V_0)\ \ge\ \vol(V_0\cap B)\ =\ \Tt(Y)+S_4\ \ge\ \Tt(Y)$.
\end{corollary}

The inequality $\vol(V_0\cap B)\ge \Tt(Y)$ is~\cite[Lemma~7.32]{BBMB}, stated there for contact configurations together with its equality case. Corollary~\ref{cor:loss} shows that, in every packing, its loss is exactly $S_4$.

\begin{proposition}\label{prop:mono}
If a centre moves radially outward, or is removed, then $\Tt(Y)$ does not decrease. Moving a centre of $Y$ radially inward strictly decreases it.
\end{proposition}

\begin{proof}
For $x\in B$ let $k(x)$ be the number of caps containing $x$. Then $\Tt(Y)=\int_B b(k(x))\,dx$ with $b(k)=1-k+\binom k2-\binom k3$, and $b(k)-b(k-1)=-(k-2)(k-3)/2\le0$ for $k\ge1$. Moving $y$ outward along its ray shrinks $H_y$, and removing $y$ removes it, so $k(x)$ does not increase anywhere. For an inward move of $y\in Y$ the gained region contains points near $y/2$. This point lies in no other half-space $H_{y'}$, because the packing condition gives $|y/2-y'|^2-|y/2|^2=\frac12\bigl(|y'|^2+|y-y'|^2-|y|^2\bigr)\ge(8-|y|^2)/2>0$. There $k$ goes from $0$ to $1$ and $b$ from $1$ to $0$.
\end{proof}

\subsection*{Contact configurations}
Suppose now that every $y\in Y$ has $|y|=2$. Then $y=2w$ with $w\in S^3$, and $|y-y'|\ge2$ means $\langle w,w'\rangle\le\frac12$. The directions form a \emph{kissing configuration} $C\subset S^3$: a finite set of unit vectors with pairwise inner products in $[-1,\frac12]$. All caps are cut off by hyperplanes at distance~$1$. Let $\omega_1$ be the volume of one such cap of $B$, let $\omega_2(u)$ be the volume of the intersection of two caps whose normals have inner product~$u$, and let $\omega_3(u,v,t)$ be the analogous volume for three caps. Then
\[
\Tt(C)=2\pi^2-\omega_1|C|+\sum_{\{w,w'\}\subset C}\omega_2(\langle w,w'\rangle)-\sum_{\{w,w',w''\}\subset C}\omega_3(\langle w,w'\rangle,\langle w,w''\rangle,\langle w',w''\rangle).
\]

\begin{lemma}\label{lem:positive}
If $k$ caps of a contact configuration share a point of $B$, then their normals have pairwise positive inner products. In particular $\omega_2(u)=0$ for $u\le0$. For three of the normals, with Gram matrix $G$ and pairwise inner products $u,v,t\le\frac12$, we have $\omega_3(u,v,t)>0$ if and only if
\[
q(u,v,t)=4uvt-(u+v+t-1)^2=2\det G-\mathbf 1^{\top}\operatorname{adj}(G)\,\mathbf 1>0 .
\]
\end{lemma}

\begin{proof}
If $x\in B$ satisfies $\langle x,w_i\rangle>1$, then the angle between $x$ and $w_i$ has cosine greater than $1/|x|>1/\sqrt2$. Any two of the $w_i$ are therefore at angle less than $\pi/2$. Now let three caps meet in $B$. By the first part their inner products $u,v,t$ lie in $(0,\frac12]$, so $\det G=1+2uvt-u^2-v^2-t^2\ge\frac14$. The entries of $\operatorname{adj}(G)\mathbf 1$ are $(1-t)(1+t-u-v)$ and its cyclic analogues, all positive. Let $x_0\in\operatorname{span}\{w_1,w_2,w_3\}$ satisfy $\langle x_0,w_i\rangle=1$ for each $i$. Then $x_0=\sum_i\lambda_iw_i$ with $\lambda=G^{-1}\mathbf 1>0$, and $|x_0|^2=\mathbf 1^{\top}G^{-1}\mathbf 1$. Every $x$ in the intersection of the three closed half-spaces satisfies
\[
|x|^2\ \ge\ |x_0|^2+2\langle x-x_0,x_0\rangle\ =\ |x_0|^2+2\sum_i\lambda_i\bigl(\langle x,w_i\rangle-1\bigr)\ \ge\ |x_0|^2 ,
\]
so $\mathbf 1^{\top}G^{-1}\mathbf 1<2$. Since $\operatorname{adj}G=(\det G)\,G^{-1}$, we get $q=\det G\,(2-\mathbf 1^{\top}G^{-1}\mathbf 1)>0$. Conversely, let $q>0$. If $\det G=0$, then $\operatorname{adj}G$ is positive semidefinite and $q=-\mathbf 1^{\top}\operatorname{adj}(G)\mathbf 1\le0$. Hence $\det G>0$ and $|x_0|^2=\mathbf 1^{\top}G^{-1}\mathbf 1<2$, and for small $\varepsilon>0$ the point $(1+\varepsilon)x_0$ lies in all three caps. The identity for $q$ is a direct expansion.
\end{proof}

\begin{lemma}[{\cite[Prop.~7.34]{BBMB}}]\label{lem:D4}
For the $D_4$ root system, normalised to unit vectors, $\Tt=8$.
\end{lemma}

\begin{proof}
The Voronoi cell of $\sqrt2D_4$ is the regular 24-cell with inradius $1$, circumradius $\sqrt2$ and volume~$8$, so $\vol(V_0\cap B)=8$. The lattice $\sqrt2D_4$ has no vectors of length strictly between $2$ and $2\sqrt2$, so $Y$ consists of the $24$ contacts. The inner products of distinct roots lie in $\{-1,-\frac12,0,\frac12\}$. The eight roots at inner product $\frac12$ with a fixed root form the vertices of a cube, two of them being at inner product $\frac12$ exactly when they are adjacent. A cube has no triangles, so no four roots have all six inner products equal to $\frac12$. By Lemma~\ref{lem:positive} no point of $B$ lies in four caps, so $S_4=0$, and Corollary~\ref{cor:loss} gives $\Tt=8$.
\end{proof}

Numerically,
\[
\omega_1\approx0.7460119958,\qquad \omega_2(\tfrac12)\approx0.0760762771,\qquad \omega_3(\tfrac12,\tfrac12,\tfrac12)\approx0.0118567031,
\]
and Lemma~\ref{lem:D4} reads $2\pi^2-24\omega_1+96\,\omega_2(\tfrac12)-96\,\omega_3(\tfrac12,\tfrac12,\tfrac12)=8$.

\section{A level-two certificate}\label{sec:cert}

We use the second level of the Lasserre hierarchy for spherical codes in the form of~\cite{LLdMK}, which built on~\cite{dLV}. The dual objects are a kernel $K$ on $\mathcal I_2$, the subsets of $S^3$ of size at most two, invariant under the orthogonal group and positive semidefinite in the sense of~\cite{LLdMK}. For a finite set $S$ of at most four points put
\[
A_2K(S)=\sum_{\substack{J,J'\in\mathcal I_2\\ J\cup J'=S}}K(J,J').
\]
Positive semidefiniteness of $K$, applied to the indicator vector of the subsets of a finite code $C$, gives
\begin{equation}\label{eq:psd}
0\ \le\ \sum_{J,J'\subseteq C,\ |J|,|J'|\le2}K(J,J')\ =\ K(\emptyset,\emptyset)+\sum_{\emptyset\ne S\subseteq C,\ |S|\le4}A_2K(S).
\end{equation}
In the symmetry-reduced form of~\cite{LLdMK}, $A_2K(S)$ is an $S_{|S|}$-invariant polynomial in the pairwise inner products of $S$. We use the degree parameters $(d_1,\delta)=(14,16)$ of~\cite{LLdMK}, and with these every such polynomial has degree at most $16$.

The objective is encoded by right-hand sides on pieces of the configuration spaces. Write $D=[-1,\frac12]$, and call a finite set of points \emph{admissible} if its pairwise inner products lie in $D$ and its Gram matrix is positive semidefinite. Let $p_2$ be a polynomial of degree at most $16$ in one variable, and let $p_3$ be an $S_3$-invariant polynomial of degree at most $16$ in three variables. The pieces are:
\begin{itemize}
\item singletons, with right-hand side $-\omega_1^+$, where $\omega_1^+$ is a rational number with $\omega_1\le\omega_1^+$;
\item pairs with $u\in[-1,0]$, right-hand side $0$, and pairs with $u\in[0,\frac12]$, right-hand side $p_2(u)$;
\item admissible triples with $q\le0$, right-hand side $0$, and admissible triples with $q\ge0$, right-hand side $-p_3$;
\item admissible quadruples, right-hand side~$0$.
\end{itemize}
On each piece we require an identity $A_2K(S)+\Sigma(S)=c(S)$, where $\Sigma$ is a sum of terms $g\cdot h$ with $h$ a sum of squares and $g$ a polynomial that is nonnegative on the piece. Put $s(x)=(x+1)(\frac12-x)$. For pairs on $[a,b]$ the polynomials $g$ are $1$ and $(u-a)(b-u)$. For triples they are $1$, the elementary symmetric functions of $s(u),s(v),s(t)$, the Gram determinant, and $-q$ or $q$ on the two triple pieces. For quadruples they are $1$, the elementary symmetric functions of the values of $s$ at the six inner products, the Gram determinant, and the elementary symmetric functions of the four $3\times3$ principal minors of the Gram matrix. In the singleton identity we add a variable $\mu\ge0$, giving $A_2K(\{x\})+r-\mu=-\omega_1^+$ with a constant $r\ge0$.

\begin{proposition}\label{prop:duality}
Suppose the identities hold, with $\mu\ge0$ and $K(\emptyset,\emptyset)+23\mu=\kappa$. Then every kissing configuration $C$ with $|C|\le23$ satisfies
\[
F(C):=2\pi^2-\omega_1^+|C|+\sum_{\substack{\{w,w'\}\subset C\\ u\ge0}}p_2(u)-\sum_{\substack{\text{triples}\\ q\ge0}}p_3\ \ \ge\ 2\pi^2-\kappa .
\]
\end{proposition}

\begin{proof}
Assign each pair with $u\ge0$ to the second pair piece and every other pair to the first. Assign each triple with $q\ge0$ to the second triple piece and every other triple to the first. Quadruples form a single piece. On the assigned piece $\Sigma\ge0$, so $A_2K(S)\le c(S)$. For singletons, $A_2K(\{x\})\le\mu-\omega_1^+$. Substituting into~\eqref{eq:psd} gives $0\le K(\emptyset,\emptyset)+|C|(\mu-\omega_1^+)+\sum p_2-\sum p_3$. Since $|C|\mu\le23\mu$, this becomes $F(C)\ge2\pi^2-K(\emptyset,\emptyset)-23\mu=2\pi^2-\kappa$.
\end{proof}

\begin{theorem}[computer-assisted]\label{thm:cert}
There is a solution of the identities above in exact rational arithmetic with $\mu>0$ and $\kappa=1828197/156250$. Hence $F(C)\ge 2\pi^2-1828197/156250=8.0387480021787\ldots$ for every kissing configuration with at most $23$ points.
\end{theorem}

The certificate, computed with the clustered low-rank solver of~\cite{LdL} and rounded to exact rationals, is in the supplement~\cite{supp}. Each zonal matrix entry, indexed as in~\cite{LLdMK} by a signature $\lambda=(\lambda_1,\lambda_2)$, was checked to have degree $|\lambda|=\lambda_1+\lambda_2$, and the sum-of-squares terms have degree at most $16$ by construction. So both sides of each identity are polynomials of degree at most~$16$, and exact equality at the pair samples and on the principal lattices of Table~\ref{tab:verif}, which are unisolvent for all such polynomials~\cite{Nic,CY}, proves the identities.

\section{The polynomial approximations}\label{sec:approx}

The function $F$ uses $\omega_1^+$, $p_2$ and $p_3$ in place of $\omega_1$, $\omega_2$ and $\omega_3$. Lemma~\ref{lem:approx} below bounds the errors (Table~\ref{tab:verif}). The volume $\omega_2$ has a closed form. For $\omega_3$ the partial derivative $\partial\omega_3/\partial u$ has a closed form in terms of a one-dimensional integral, and $\omega_3$ is enclosed by certified one-dimensional integration~\cite{Arb}. The same formula bounds the derivatives of $\omega_3-p_3$ over each box of a cover of the triple piece.

\begin{lemma}[computer-assisted]\label{lem:approx}
Let $\varepsilon_2=2.8111\cdot10^{-12}$ and $\varepsilon_3=10^{-6}$. Then
\begin{enumerate}
\item $\omega_1\le\omega_1^+$;
\item $p_2(u)\le\omega_2(u)+\varepsilon_2$ for $u\in[0,\frac12]$;
\item $p_3(u,v,t)\ge\omega_3(u,v,t)-\varepsilon_3$ for every admissible triple with $q(u,v,t)\ge0$.
\end{enumerate}
\end{lemma}

By Lemma~\ref{lem:positive}, $\omega_2=0$ on $[-1,0]$ and $\omega_3=0$ on admissible triples with $q\le0$. The right-hand side $0$ on those pieces is therefore exact.

\section{Proof of \texorpdfstring{Theorem~\ref{thm:main}}{Theorem 1.1}}\label{sec:proof}

By Corollary~\ref{cor:loss} it suffices to show $\Tt(C)\ge8$ for every kissing configuration $C\subset S^3$, with equality only for $D_4$. By~\cite{Mus} we have $|C|\le24$, and by~\cite{LLdMK} a configuration with $|C|=24$ is a $D_4$ root system, for which $\Tt=8$ by Lemma~\ref{lem:D4}.

Let $|C|\le23$. Then $C$ has at most $253$ pairs and $1771$ triples. Lemmas~\ref{lem:positive} and~\ref{lem:approx} give
\[
\Tt(C)\ \ge\ F(C)-253\,\varepsilon_2-1771\,\varepsilon_3 ,
\]
since the singleton term only improves, the pair and triple terms on the pieces with right-hand side $0$ are exact, and each remaining term loses at most $\varepsilon_2$ or $\varepsilon_3$. Theorem~\ref{thm:cert} then gives
\[
\Tt(C)\ \ge\ 2\pi^2-\frac{1828197}{156250}-253\,\varepsilon_2-1771\,\varepsilon_3=8.0369770014675\ldots>8 .
\]

If $\vol(V_0)=8$, then $\Tt(C)\le8$ by Corollary~\ref{cor:loss}, so $C$ is a $D_4$ root system and $V_0$ is the regular 24-cell. Conversely, if the contacts form $\sqrt2$ times a $D_4$ root system, their half-spaces cut out a regular 24-cell of circumradius $\sqrt2$. Every other centre $y$ has $|y|\ge2\sqrt2$, so $H_y$ lies in $\{|x|>\sqrt2\}$ and misses the cell. Hence $V_0$ is this 24-cell and $\vol(V_0)=8$. \qed

\section{Remarks on the relaxation}\label{sec:remarks}

\begin{remark}[The bound on the number of points]\label{rem:cap}
The values in this remark are floating-point solutions of the semidefinite programs. Without the constraint $|C|\le23$, the relaxation gives only $\Tt\ge7.9617$ at degrees $(14,16)$ and $7.9932$ at degrees $(16,18)$; at $(14,16)$ the numbers of pairs, triples and quadruples of its optimal moment vector are close to those of a mixture of a $23$-point and a $24$-point configuration, which the bound on $|C|$ excludes. The bound $|C|\le23.5$, which is equivalent for integer sizes, gives $7.9807$. For the exact truncated volume $\Tt+S_4$ of Corollary~\ref{cor:loss} the values are $7.9953$ without a bound and $8.0239$ with $|C|\le23.5$. Whether the relaxation for $\Tt+S_4$ reaches $8$ without a bound on $|C|$ at some degree is open.
\end{remark}

\begin{remark}[The packing constraint is needed]\label{rem:poly}
The bound concerns cells whose facets come from a kissing configuration. Without the angular constraint it fails. The polytope $\{x:\langle x,q_i\rangle\le1,\ i=1,\dots,24\}$ for the rational vectors $q_i$ listed in the supplement contains the unit ball and has $24$ facets, yet its volume is $7.9655697\ldots<8$. This was computed exactly, by two independent methods~\cite{supp}. Its normals have minimal angle about $54.6^\circ$. A volume below $8$ in this setting was observed numerically in the code accompanying~\cite{BBMB}. So no argument about facet directions alone, in the manner of Fejes T\'oth's bound for polyhedra with twelve faces containing a ball~\cite{FT}, can give the conjecture. Any proof must use the $60^\circ$ separation.
\end{remark}

\begin{remark}[Beyond contacts]\label{rem:beyond}
For a general cell, the centres at distance between $2$ and $2\sqrt2$ cut smaller caps from $B$, and Proposition~\ref{prop:four} still applies. The natural extension of Theorem~\ref{thm:cert} is a level-two relaxation in which each point carries its distance as a label. By Proposition~\ref{prop:mono}, rounding labels down is valid, but near $D_4$ the bound grows only linearly in the displacement, so such a relaxation must keep the labels continuous there. Theorem~\ref{thm:local} treats the configurations near $D_4$ by a local argument instead.
\end{remark}

\section{A neighbourhood of \texorpdfstring{$D_4$}{D4}}\label{sec:local}

This section proves Theorem~\ref{thm:local}. We translate so that $c=0$ and write $\rho$ and $\sigma$ for the two bounds in the hypothesis, so that $d(W)\le\rho$ and $\sum_i\delta_i\le\sigma$. Put
\[
h_i=\tfrac12|y_i|,\qquad \eta_i=h_i-1=\tfrac12\delta_i,\qquad s=\sum_{i=1}^{24}\eta_i,\qquad w_i=\frac{y_i}{|y_i|} .
\]
The packing condition gives $\eta_i\ge0$, and the hypothesis gives $\eta_i\le\bar\eta:=\sigma/2$ and $s\le\sigma/2$, so that $|\eta|^2\le\bar\eta s$. Since $H_{y_i}=\{x:\langle x,w_i\rangle>h_i\}$, the cell lies in the polytope
\[
P=\{x:\ \langle x,w_i\rangle\le h_i,\ i=1,\dots,24\},
\]
and we put $\mathcal F=\vol(P\cap B)$, with $B=\{|x|<\sqrt2\}$ as in Section~\ref{sec:trunc}. The argument works for any $(\rho,\sigma)$ satisfying the conditions collected in Section~\ref{ssec:assembly}, and it gives $\vol(V_0)\ge8+\Gamma s$ with an explicit constant $\Gamma=\Gamma(\rho,\sigma)>0$. The values in Theorem~\ref{thm:local} are one certified instance, the row $(\rho,\sigma)=(\tfrac25,\tfrac3{100})$ of Table~\ref{tab:pairs}, which we call the \emph{main row}.

The proof compares the first-order gain with the losses. By Lemma~\ref{lem:hull}, the cell contains $P\cap J$, where $J$ is the inversion hull of Section~\ref{ssec:hull}, so $\vol(V_0)$ is at least $\mathcal F$ minus the \emph{hull deficit} $\vol((P\cap B)\setminus J)$. In Section~\ref{ssec:decomp} we write $\mathcal F$ as an inclusion--exclusion sum $\Phi$, the analogue of $\Tt$, up to a small term from squares of caps, and in Section~\ref{ssec:smooth} we expand $\Phi$ about $D_4$: to first order it grows by $\frac43s$, the quadratic part is controlled by exact matrices, and the third-order remainder is explicit. In Section~\ref{ssec:deficit} we bound the hull deficit by quadratic terms. All these losses are quadratic in the tilt $\tau$ and the pushes $\eta$. The rigidity estimate of Section~\ref{ssec:rigid} bounds $|\tau|$ by a multiple of $s$, and $|\eta|^2\le\bar\eta s$, so in the region of Theorem~\ref{thm:local} the losses add up to less than $\frac43s$, and the first-order gain dominates them. The budget and the assembly of the bound are in Section~\ref{ssec:assembly}.

\subsection{The root system}\label{ssec:roots}

The roots of $D_4$ are the $24$ vectors $\pm e_p\pm e_q$ with $p<q$, and $u_i$ is the $i$th root divided by $\sqrt2$. Two distinct $u_i,u_j$ have inner product $\frac12$ on a set $T$ of $96$ pairs, $0$ on a set $O$ of $72$ pairs, $-\frac12$ on $96$ pairs and $-1$ on $12$. The pairs in $T$ are the \emph{contact pairs}. Each $u_i$ lies in eight of them, and its eight contact neighbours sum to $4u_i$. A \emph{contact triangle} is a set of three roots any two of which form a contact pair. There are $96$ contact triangles, each contact pair lies in exactly three of them and each root in twelve, and no four roots are pairwise in contact (proof of Lemma~\ref{lem:D4}).

The $24$ \emph{vertex directions} $v_1,\dots,v_{24}$ are the unit vectors $\pm e_p$ and $\frac12(\pm1,\pm1,\pm1,\pm1)$. Each inner product $\langle u_i,v_k\rangle$ is $0$ or $\pm1/\sqrt2$. For each $k$ the set
$N(k)=\{i:\langle u_i,v_k\rangle=1/\sqrt2\}$ has six elements. It consists of three orthogonal pairs $\{a_{kj},a'_{kj}\}$, $j=1,2,3$, and its other twelve pairs are contact pairs. With $f_{kj}=(u_{a_{kj}}-u_{a'_{kj}})/\sqrt2$, the vectors $v_k,f_{k1},f_{k2},f_{k3}$ are orthonormal, and the six roots in $N(k)$ are $(v_k\pm f_{kj})/\sqrt2$. In particular $u_{a_{kj}}+u_{a'_{kj}}=\sqrt2\,v_k$. Each orthogonal pair lies in exactly one set $N(k)$, each contact pair in exactly three and each root in exactly six. A \emph{square} is the union of two orthogonal pairs of the same $N(k)$; there are $72$ squares. The polytope
\[
J_0=\conv\{2u_1,\dots,2u_{24}\}=\{x:\ \langle x,v_k\rangle\le\sqrt2\ \text{for all }k\}
\]
is a 24-cell with inradius $\sqrt2$. Its facet with normal $v_k$ is the octahedron $\conv\{2u_b:b\in N(k)\}$, which touches the sphere $|x|=\sqrt2$ at $\sqrt2\,v_k$.

For each $i$ fix a $4\times3$ matrix $B_i$ whose columns form an orthonormal basis of $u_i^\perp$. A \emph{tilt} is a vector $\tau=(\tau_1,\dots,\tau_{24})\in(\R^3)^{24}=\R^{72}$, and we write $t_i=B_i\tau_i\in u_i^\perp$, so that $|\tau|^2=\sum_i|t_i|^2$. The \emph{rigidity operator} $\Lambda:\R^{72}\to\R^T$ and its analogue $\Lambda_O:\R^{72}\to\R^O$ on orthogonal pairs are
\[
(\Lambda\tau)_{ij}=\langle t_i,u_j\rangle+\langle u_i,t_j\rangle\quad(\{i,j\}\in T),\qquad
(\Lambda_O\tau)_{ij}=\langle t_i,u_j\rangle+\langle u_i,t_j\rangle\quad(\{i,j\}\in O).
\]
The vector $\Lambda\tau$ is the first-order change of the contact inner products when each $u_i$ moves to $u_i+t_i$.

The exact computations in~\cite{supp} use other coordinates: $t_i=B_i^{\rm s}\tau_i^{\rm s}$, where $\sqrt2\,B_i^{\rm s}$ is an integer $4\times3$ matrix whose columns are orthogonal, lie in $u_i^\perp$ and have lengths $\sqrt2,1,1$. So the columns of $B_i^{\rm s}$ have Gram matrix $\mathrm{diag}(1,\frac12,\frac12)$. In the coordinates $\tau^{\rm s}$, the matrices of $\Lambda$ and $\Lambda_O$ are rational, and so are the matrices of the quadratic forms given by $N_0$ in Lemma~\ref{lem:rigid} and by $\Hs$ in Lemma~\ref{lem:deriv}. Positive semidefiniteness, eigenvalues, Schur complements and norms refer to the Euclidean inner product and do not depend on the coordinates. In~\cite{supp} they are computed exactly in the coordinates $\tau^{\rm s}$, with this Gram matrix.

\begin{lemma}\label{lem:Lambda}
\begin{enumerate}
\item The eigenvalues of $\Lambda^{\top}\Lambda$ are $0,1,\frac52,3,4$, with multiplicities $6,29,8,21,8$, and $\ker\Lambda=\{(B_i^{\top}Au_i)_i:\ A\in\mathfrak{so}(4)\}$. Hence $|\Lambda\tau|\ge|\tau|$ for $\tau\perp\ker\Lambda$, and $\|\Lambda\|=2$.
\item $\sum_{\{i,j\}\in T}(\Lambda\tau)_{ij}=0$ for every $\tau$.
\item $\|\Lambda_O\|\le2$.
\end{enumerate}
\end{lemma}

\begin{proof}
Part (1) is~\cite[Lemma~7.50]{BBMB}, where it is stated for the singular values of $\Lambda$. The vectors $(B_i^{\top}Au_i)_i$ lie in the kernel because $\langle Au_i,u_j\rangle+\langle u_i,Au_j\rangle=0$, and they form a $6$-dimensional space because the $u_i$ span $\R^4$; since $\ker\Lambda$ has dimension $6$, they form all of it. For (2), $\sum_T(\Lambda\tau)_{ij}=\sum_i\langle t_i,\sum_{j}u_j\rangle$, where $j$ runs over the contact neighbours of $i$. This equals $\sum_i\langle t_i,4u_i\rangle=0$, which is the constant stress of~\cite[Cor.~7.49]{BBMB}. For (3), the six roots orthogonal to $u_i$ are $\pm$ an orthonormal basis of $u_i^\perp$, so $\sum_{j\perp i}\langle t_i,u_j\rangle^2=2|t_i|^2$, and $\sum_O(\Lambda_O\tau)_{ij}^2\le2\sum_i\sum_{j\perp i}\langle t_i,u_j\rangle^2=4|\tau|^2$.
\end{proof}

By (1) and (2), a tilt with $\Lambda\tau\le0$ satisfies $\Lambda\tau=0$ and is an infinitesimal rotation: the normalised root system is infinitesimally jammed, as shown in~\cite[Prop.~3.3]{CJKT}. Lemma~\ref{lem:rigid} below is a quantitative form of this statement.

\subsection{The other centres}\label{ssec:hull}

Put $q_i=4y_i/|y_i|^2=2w_i/h_i$, the image of $y_i$ under inversion in the sphere of radius~$2$, and let
\[
J=\conv\{0,q_1,\dots,q_{24}\}
\]
be the \emph{inversion hull}.

\begin{lemma}[Inversion hull~\cite{BBMBd}]\label{lem:hull}
For centres $y\ne z$, both different from $0$, and $q_y=4y/|y|^2$,
\[
\frac{|z|^2}2-\langle q_y,z\rangle=\frac{(|z|^2-4)(|y|^2-4)+4(|y-z|^2-4)}{2|y|^2}\ \ge\ 0 .
\]
Consequently $V_0\supseteq P\cap J$ and
\[
\vol(V_0)\ \ge\ \mathcal F-\vol\bigl((P\cap B)\setminus J\bigr).
\]
\end{lemma}

\begin{proof}
Since $2\langle y,z\rangle=|y|^2+|z|^2-|y-z|^2$,
\[
2|y|^2\Bigl(\frac{|z|^2}2-\langle q_y,z\rangle\Bigr)=|y|^2|z|^2-4\bigl(|y|^2+|z|^2-|y-z|^2\bigr)=(|z|^2-4)(|y|^2-4)+4(|y-z|^2-4),
\]
and the three brackets are nonnegative by the packing condition. Hence, for every centre $z\notin\{0,y_1,\dots,y_{24}\}$, the closed half-space $\{x:\langle x,z\rangle\le|z|^2/2\}$ contains $0$ and every $q_i$, and therefore contains $J$. The cell $V_0$ is the intersection of $P$ with these half-spaces, so $V_0\supseteq P\cap J$ and $\vol(V_0)\ge\vol(P\cap J\cap B)=\mathcal F-\vol((P\cap B)\setminus J)$.
\end{proof}

\subsection{Gauge and rigidity}\label{ssec:rigid}

Choose, as in~\cite[Theorem~7.51]{BBMB}, a labelling and an $R\in O(4)$ that attain $d(W)$. Applying $R^{-1}$ to the packing changes neither the hypotheses nor the volume, so we may assume $R=I$. Then the identity minimises $R'\mapsto\sum_i|w_i-R'u_i|^2$ over $O(4)$. Put
\[
d_i=w_i-u_i,\qquad \|d\|=\Bigl(\sum_i|d_i|^2\Bigr)^{1/2}=d(W)\le\rho,\qquad n_i=\langle d_i,u_i\rangle,\qquad t_i=d_i-n_iu_i,
\]
let $\tau\in\R^{72}$ be the tilt with $B_i\tau_i=t_i$, and write $\xi=(\tau,\eta)\in\R^{72}\times\R^{24}$. For $\{i,j\}\in T\cup O$ put $u_{ij}=\langle w_i,w_j\rangle$, and for $\{i,j\}\in T$ put $\Delta u_{ij}=u_{ij}-\frac12$. Let $\bar d$ be a number with $\max_i|d_i|\le\|d\|\le\bar d<1$. At first $\bar d=\rho$, and Corollary~\ref{cor:boot} below replaces it by a much smaller value. Put
\[
\chi=\frac{2}{1+(1-\bar d^2)^{1/2}},\qquad \varphi=2\arcsin\frac{\bar d}2,\qquad \bar u=\tfrac12-\cos\bigl(\tfrac\pi3+2\varphi\bigr),\qquad \bar u_\perp=\sin2\varphi .
\]

\begin{lemma}\label{lem:gauge}
\begin{enumerate}
\item $\tau\perp\ker\Lambda$.
\item $n_i=-\frac12|d_i|^2$ and $|t_i|^2\le|d_i|^2\le\chi|t_i|^2$. Hence $|\tau|\le\|d\|\le\chi^{1/2}|\tau|$.
\item For $\{i,j\}\in T$ we have $\Delta u_{ij}=(\Lambda\tau)_{ij}+c_{ij}$ with $c_{ij}=\langle d_i,d_j\rangle-\frac14(|d_i|^2+|d_j|^2)$. For $\{i,j\}\in O$ we have $u_{ij}=(\Lambda_O\tau)_{ij}+\langle d_i,d_j\rangle$. Moreover
\[
\sum_{\{i,j\}\in T}\Delta u_{ij}=Q_d:=\sum_{\{i,j\}\in T}\langle d_i,d_j\rangle-2\|d\|^2 .
\]
\item $|c_{ij}|\le\frac34(|d_i|^2+|d_j|^2)$ and $(\sum_Tc_{ij}^2)^{1/2}\le3\bar d\|d\|$. With $Q_t(\tau)=\sum_T\langle t_i,t_j\rangle-2|\tau|^2$,
\[
|Q_d-Q_t(\tau)|\le\bigl(2\sqrt3\,\chi\bar d+\chi^2\bar d^2\bigr)|\tau|^2 .
\]
\item For $\{i,j\}\in T$,
\[
u_{ij}\ \le\ a(h_i,h_j)\ \le\ \tfrac12+\tfrac12(\eta_i+\eta_j),\qquad a(h,h')=\frac{h^2+h'^2-1}{2hh'} .
\]
\item If $2\varphi<\pi/6$, then $u_{ij}\ge\frac12-\bar u$ for $\{i,j\}\in T$, $|u_{ij}|\le\bar u_\perp$ for $\{i,j\}\in O$, and $u_{ij}<0$ for all other pairs.
\end{enumerate}
\end{lemma}

\begin{proof}
(1) For $A\in\mathfrak{so}(4)$ the derivative of $s\mapsto\sum_i|w_i-e^{sA}u_i|^2$ at $s=0$ is $-2\sum_i\langle u_i+d_i,Au_i\rangle=-2\sum_i\langle t_i,Au_i\rangle$, because $\langle u_i,Au_i\rangle=0$ and $d_i-t_i$ is a multiple of $u_i$. Minimality makes it vanish, so $\tau$ is orthogonal to every $(B_i^{\top}Au_i)_i$, and these span $\ker\Lambda$ by Lemma~\ref{lem:Lambda}.

(2) Expanding $|u_i+d_i|^2=1$ gives $|d_i|^2=-2n_i$. Hence $n_i^2+2n_i+|t_i|^2=0$, and since $\langle w_i,u_i\rangle=1+n_i=1-\frac12|d_i|^2>0$ (as $|d_i|\le\bar d<1$) we get $n_i=(1-|t_i|^2)^{1/2}-1$. So $|d_i|^2=2|t_i|^2/(1+(1-|t_i|^2)^{1/2})\le\chi|t_i|^2$, while $|d_i|^2=|t_i|^2+n_i^2\ge|t_i|^2$.

(3) For $\{i,j\}\in T$ we have $\langle u_i,d_j\rangle=\langle u_i,t_j\rangle+\frac12n_j=\langle u_i,t_j\rangle-\frac14|d_j|^2$, and expanding $\langle u_i+d_i,u_j+d_j\rangle$ gives the first identity. The second is the same expansion with $\langle u_i,u_j\rangle=0$. For the sum, the contact neighbours of $u_i$ sum to $4u_i$, so $\sum_T(\langle u_i,d_j\rangle+\langle d_i,u_j\rangle)=\sum_i\langle d_i,4u_i\rangle=4\sum_in_i=-2\|d\|^2$.

(4) The bound on $c_{ij}$ follows from $|\langle d_i,d_j\rangle|\le\frac12(|d_i|^2+|d_j|^2)$. Since each root lies in eight contact pairs, $\sum_Tc_{ij}^2\le\frac9{16}\sum_T(|d_i|^2+|d_j|^2)^2\le\frac98\sum_T(|d_i|^4+|d_j|^4)=9\sum_i|d_i|^4\le9\bar d^2\|d\|^2$. For the last bound write $d_i=t_i+n_iu_i$. For $\{i,j\}\in T$ this gives $\langle d_i,d_j\rangle=\langle t_i,t_j\rangle+n_j\langle t_i,u_j\rangle+n_i\langle u_i,t_j\rangle+\frac12n_in_j$, and $\|d\|^2=|\tau|^2+\sum_in_i^2$, so
\[
Q_d-Q_t(\tau)=\sum_T\bigl(n_j\langle t_i,u_j\rangle+n_i\langle u_i,t_j\rangle+\tfrac12n_in_j\bigr)-2\sum_in_i^2 .
\]
Here $|\langle t_i,u_j\rangle|=|\langle t_i,u_j-\frac12u_i\rangle|\le\frac{\sqrt3}2|t_i|$, $|n_i|\le\frac\chi2|t_i|^2$ and $|t_i|\le\bar d$. The cubic terms are therefore at most $\frac{\sqrt3\chi}4\bar d\sum_T(|t_i|^2+|t_j|^2)=2\sqrt3\chi\bar d|\tau|^2$. The quartic terms are at most $\frac{\chi^2}{16}\bar d^2\sum_T(|t_i|^2+|t_j|^2)+\frac{\chi^2}2\bar d^2|\tau|^2=\chi^2\bar d^2|\tau|^2$.

(5) The packing condition $|y_i-y_j|^2=4h_i^2+4h_j^2-8h_ih_ju_{ij}\ge4$ is $u_{ij}\le a(h_i,h_j)$. With $h=1+\eta$ a direct expansion gives
\[
\tfrac12(\eta_i+\eta_j)-\bigl(a(h_i,h_j)-\tfrac12\bigr)=\frac{\eta_i\eta_j(3+\eta_i+\eta_j)}{2(1+\eta_i)(1+\eta_j)}\ \ge\ 0 .
\]

(6) The angle between $w_i$ and $u_i$ is $2\arcsin(|d_i|/2)\le\varphi$. Angles between points of $S^3$ satisfy the triangle inequality, so the angle between $w_i$ and $w_j$ differs by at most $2\varphi$ from the angle between $u_i$ and $u_j$. This angle is $\pi/3$ on $T$, $\pi/2$ on $O$ and at least $2\pi/3$ otherwise. Since $2\varphi<\pi/6$, this gives the three bounds.
\end{proof}

The next lemma is the rigidity argument of~\cite[Theorem~7.51]{BBMB}, carried out with slack as in~\cite{BBMBd}: the contact inner products may exceed $\frac12$ by the pushes.

\begin{lemma}[computer-assisted]\label{lem:rigid}
Let $C_r$ be the supremum of $|\tau'|$ over all $\tau'\perp\ker\Lambda$ and $\eta'\in\R^{24}$ such that $\eta'\ge0$, $\sum_i\eta'_i=1$, and $(\Lambda\tau')_{ij}\le\frac12(\eta'_i+\eta'_j)$ for all $\{i,j\}\in T$. Then $C_r$ is finite, and $C_r^2\le\frac{191}{100}$. In the setting of Lemma~\ref{lem:gauge},
\[
|\tau|\ \le\ C_r\bigl(s+\tfrac32\|d\|^2\bigr).
\]
If moreover $|\tau|\le\bar t$ and $\beta:=\frac32C_r\chi\bar t<1$, then $|\tau|\le C_rs/(1-\beta)$.
\end{lemma}

\begin{proof}
First, $C_r\le8$. Let $(\tau',\eta')$ be admissible. Since each root lies in eight contact pairs, $\sum_T(\Lambda\tau')^+_{ij}\le\frac12\sum_T(\eta'_i+\eta'_j)=4$. By Lemma~\ref{lem:Lambda}(2) the entries of $\Lambda\tau'$ sum to $0$, so $\|\Lambda\tau'\|_1=2\sum_T(\Lambda\tau')^+_{ij}\le8$. By Lemma~\ref{lem:Lambda}(1), $|\tau'|\le|\Lambda\tau'|\le\|\Lambda\tau'\|_1\le8$.

The bound $C_r^2\le\frac{191}{100}$ comes from an identity
\[
\tfrac{191}{100}\Bigl(\sum_i\eta'_i\Bigr)^2-|\tau'_\perp|^2=\xi'^{\top}N_0\xi'+\sum_{k,l}(M_0)_{kl}\,\ell_k(\xi')\,\ell_l(\xi')\qquad\text{for all }\xi'=(\tau',\eta'),
\]
where $\tau'_\perp$ is the component of $\tau'$ orthogonal to $\ker\Lambda$ and $\ell_1,\dots,\ell_{120}$ are the linear forms $\eta'_i$ and $\frac12(\eta'_i+\eta'_j)-(\Lambda\tau')_{ij}$ for $\{i,j\}\in T$. The matrix $M_0$ is symmetric with nonnegative rational entries, and $N_0$ is positive semidefinite (Table~\ref{tab:verif}). On admissible $(\tau',\eta')$ every $\ell_k$ is nonnegative, so $|\tau'|^2\le\frac{191}{100}$.

By Lemma~\ref{lem:gauge}(3)--(5), $(\Lambda\tau)_{ij}=\Delta u_{ij}-c_{ij}\le\frac12(\eta_i+\eta_j)+\frac34(|d_i|^2+|d_j|^2)$ on $T$. So $\eta'_i:=\eta_i+\frac32|d_i|^2\ge0$ satisfies $(\Lambda\tau)_{ij}\le\frac12(\eta'_i+\eta'_j)$, and $\tau\perp\ker\Lambda$ by Lemma~\ref{lem:gauge}(1). If $\sum_i\eta'_i>0$, scaling gives $|\tau|\le C_r\sum_i\eta'_i=C_r(s+\frac32\|d\|^2)$. If $\sum_i\eta'_i=0$, then $\Lambda\tau\le0$ with entries summing to $0$, so $\Lambda\tau=0$ and $\tau=0$. Finally $\|d\|^2\le\chi|\tau|^2\le\chi\bar t|\tau|$, so $|\tau|\le C_rs+\beta|\tau|$.
\end{proof}

Iterating Lemma~\ref{lem:rigid} improves the bound $\bar d$.

\begin{corollary}\label{cor:boot}
Let $D_0=\rho$, and for $n\ge0$ let $\chi_n=2/(1+(1-D_n^2)^{1/2})$, $\beta_n=\frac32C_r\chi_nD_n$ and
\[
D_{n+1}=\min\Bigl(D_n,\ \chi_n^{1/2}\,\frac{C_r\,\sigma/2}{1-\beta_n}\Bigr).
\]
If $\beta_0<1$, then for every $n$ we have $\|d\|\le D_n$, hence $\max_i|d_i|\le D_n$, and
\[
|\tau|\ \le\ C_r''\,s\ \le\ \tau_{\max}:=C_r''\,\sigma/2,\qquad C_r''=\frac{C_r}{1-\beta_n} .
\]
\end{corollary}

\begin{proof}
By induction on $n$. If $\|d\|\le D_n$, then $|\tau|\le\|d\|\le D_n$, so Lemma~\ref{lem:rigid} applies with $\bar d=\bar t=D_n$ and $\beta=\beta_n\le\beta_0<1$. It gives $|\tau|\le C_rs/(1-\beta_n)\le C_r(\sigma/2)/(1-\beta_n)$, and then $\|d\|\le\chi_n^{1/2}|\tau|\le D_{n+1}$ by Lemma~\ref{lem:gauge}(2).
\end{proof}

We write $D_{\rm eff}$ for the value of $D_n$ used below (the computation of Section~\ref{ssec:assembly} takes $D_{\rm eff}=D_{12}$). From now on $\bar d=D_{\rm eff}$, the quantities $\chi,\varphi,\bar u,\bar u_\perp$ are computed from it, and we assume $2\varphi<\pi/6$, so that Lemma~\ref{lem:gauge}(6) applies. At $\rho=\tfrac25$ the first step has $\beta_0=0.8653\ldots$, and at the main row the iteration gives the value $D_{\rm eff}$ of Table~\ref{tab:pairs}.

\subsection{The truncated volume of \texorpdfstring{$P$}{P}}\label{ssec:decomp}

For heights $h_1,\dots,h_m\ge1$ and unit vectors $w_1,\dots,w_m$ with Gram entries $u_{ab}$, the volume of
\[
\{x:\ |x|<\sqrt2,\ \langle x,w_a\rangle>h_a\ \text{for } a=1,\dots,m\}
\]
depends only on the $h_a$ and the $u_{ab}$. For $m=1,2,3$ we denote it by $S(h_1)$, $\Pi(h_1,h_2;u_{12})$ and $\Theta(h_1,h_2,h_3;u_{12},u_{13},u_{23})$. Thus $S(h_i)=\vol(K_{y_i})$, and at $h=1$ these are the functions $\omega_1,\omega_2,\omega_3$ of Section~\ref{sec:trunc}. Define
\[
\Phi(h,u_T)=2\pi^2-\sum_iS(h_i)+\sum_{\{i,j\}\in T}\Pi(h_i,h_j;u_{ij})-\sum_{\{a,b,c\}}\Theta(h_a,h_b,h_c;u_{ab},u_{ac},u_{bc}),
\]
the last sum over the $96$ contact triangles. This is a function of the $24$ heights and the $96$ contact inner products. At $\zeta_0=(h=1,\ u_T=\frac12)$ it equals $\Tt(D_4)=8$, by Lemma~\ref{lem:D4}.

The next lemma describes two half-spaces in a frame adapted to them.

\begin{lemma}\label{lem:pair}
Let $w,w'$ be unit vectors with $u=\langle w,w'\rangle\in(-1,1)$, and let $h,h'\ge1$. Put $\alpha=((1+u)/2)^{1/2}$, $\alpha'=((1-u)/2)^{1/2}$, $p=(w+w')/(2\alpha)$, $n=(w-w')/(2\alpha')$, $\hat h=\frac12(h+h')$, $\check h=(h-h')/(2\alpha')$, $\hat c=\hat h/\alpha$ and $\hat g=\sqrt2-\hat c$. Then $p,n$ are orthonormal, and $\langle x,w\rangle>h$ and $\langle x,w'\rangle>h'$ hold if and only if $\alpha\langle x,p\rangle>\hat h+\alpha'|\langle x,n\rangle-\check h|$. If some $x$ with $|x|<\sqrt2$ satisfies both, then $\hat g>0$, $u>0$ and $\hat g\le u/\sqrt2$, and every such $x$ satisfies
\[
\hat c<\langle x,p\rangle<\sqrt2,\qquad |\langle x,n\rangle-\check h|<\frac{\alpha}{\alpha'}\bigl(\langle x,p\rangle-\hat c\bigr),\qquad |x-\sqrt2p|^2<(2-\hat c^2)+\hat g^2 .
\]
\end{lemma}

\begin{proof}
We have $w=\alpha p+\alpha'n$ and $w'=\alpha p-\alpha'n$. The two inequalities read $\alpha\langle x,p\rangle>h-\alpha'\langle x,n\rangle$ and $\alpha\langle x,p\rangle>h'+\alpha'\langle x,n\rangle$, and the larger right-hand side is $\hat h+\alpha'|\langle x,n\rangle-\check h|$. This gives $\langle x,p\rangle>\hat c$ and the bound on $\langle x,n\rangle-\check h$, and $\langle x,p\rangle\le|x|<\sqrt2$. Next, $|x-\sqrt2p|^2=(|x|^2-\langle x,p\rangle^2)+(\sqrt2-\langle x,p\rangle)^2<(2-\hat c^2)+\hat g^2$. Since $h,h'\ge1$ we have $\hat c\ge1/\alpha=(2/(1+u))^{1/2}$, so $\hat c<\sqrt2$ forces $u>0$, and $\hat g\le\sqrt2(1-(1+u)^{-1/2})\le u/\sqrt2$.
\end{proof}

For $x\in B$ let $A(x)=\{i:\ x\in K_{y_i}\}$, and put
\[
c_0=\Bigl(\frac{2}{1+\bar u_\perp}\Bigr)^{1/2},\qquad \zeta_O=\bigl((2-c_0^2)+(\sqrt2-c_0)^2\bigr)^{1/2}+4\bar d .
\]

\begin{lemma}\label{lem:activity}
Suppose $\zeta_O\le1-\sqrt2\,\bar d$, and let $x\in B$. Either any two elements of $A(x)$ form a contact pair, and then $A(x)$ has at most three elements, or $A(x)\subseteq N(k)$ for some $k$.
\end{lemma}

\begin{proof}
Let $x\in K_{y_i}\cap K_{y_j}$ with $\{i,j\}\notin T$. By Lemma~\ref{lem:pair}, $u_{ij}>0$, so $\{i,j\}\in O$ by Lemma~\ref{lem:gauge}(6). Let $k$ be the vertex with $\{i,j\}\subseteq N(k)$, so that $u_i+u_j=\sqrt2\,v_k$. Lemma~\ref{lem:pair} gives $|x-\sqrt2p|<((2-\hat c^2)+\hat g^2)^{1/2}$, and $\hat c\ge(2/(1+u_{ij}))^{1/2}\ge c_0$. The right-hand side decreases in $\hat c$, so it is at most $((2-c_0^2)+(\sqrt2-c_0)^2)^{1/2}$. Since $|(w_i+w_j)-(u_i+u_j)|\le2\bar d$ and $|u_i+u_j|=\sqrt2$, and $|a/|a|-b/|b||\le2|a-b|/|b|$ for nonzero vectors, we get $|p-v_k|\le2\sqrt2\,\bar d$. Hence $|x-\sqrt2v_k|<\zeta_O$. If also $x\in K_{y_l}$, then
\[
1\le h_l<\langle x,w_l\rangle\le\sqrt2\langle v_k,w_l\rangle+\zeta_O\le\sqrt2\langle v_k,u_l\rangle+\sqrt2\,\bar d+\zeta_O ,
\]
so $\langle v_k,u_l\rangle>0$. Hence $\langle v_k,u_l\rangle=1/\sqrt2$, that is, $l\in N(k)$. So $A(x)\subseteq N(k)$ as soon as $A(x)$ contains a pair outside $T$. Otherwise its elements are pairwise in contact, and there are at most three of them.
\end{proof}

\begin{lemma}\label{lem:decomp}
Suppose $\zeta_O\le1-\sqrt2\,\bar d$ and $64\bar d^2<1$. Then $\mathcal F=\Phi(h,u_T)+\mathcal N$, where
\[
\mathcal N=\int_B\nu(A(x))\,dx,\qquad \nu(A)=[A=\emptyset]-1+|A|-e_T(A)+t_T(A),
\]
and $e_T(A)$, $t_T(A)$ are the numbers of contact pairs and contact triangles contained in $A$. The function $\nu(A(x))$ takes values in $\{-1,0,1\}$, and it equals $-1$ exactly when $A(x)$ is a square. Moreover
\[
\mathcal N\ \ge\ -\sum_{Q}\vol\Bigl(\bigcap_{a\in Q}K_{y_a}\Bigr)\ \ge\ -A_{\rm sq}|\tau|^2,
\]
the sum over the $72$ squares $Q$, where $A_{\rm sq}=\frac12k_{\rm sq}\,\bar g^{3/2}(2+\sqrt3\,\bar d\chi^{1/2})^2$ with
\[
k_{\rm sq}=\frac{32}{15}\,2^{3/4}\,\frac{1+\bar u_\perp}{1-\bar u_\perp}\,(1-64\bar d^2)^{-1/2},\qquad \bar g=\bar u_\perp/\sqrt2 .
\]
\end{lemma}

\begin{proof}
Up to a null set, $P\cap B=\{x\in B:A(x)=\emptyset\}$. The numbers $S(h_i)$, $\Pi(h_i,h_j;u_{ij})$ and $\Theta(\dots)$ are the volumes of the caps $K_{y_i}$ and of their intersections, so $\sum_iS(h_i)=\int_B|A(x)|\,dx$, $\sum_T\Pi=\int_Be_T(A(x))\,dx$ and $\sum\Theta=\int_Bt_T(A(x))\,dx$. With $\vol(B)=2\pi^2$ this gives $\mathcal F-\Phi=\mathcal N$. By Lemma~\ref{lem:activity}, $A(x)$ is a set of at most three pairwise contacts, where $\nu=0$, or lies in some $N(k)$. In $N(k)$ the contact pairs are the twelve edges of an octahedron, the orthogonal pairs its three diagonals and the contact triangles its eight faces. A subset without a diagonal lies in a face, where $\nu=0$. For subsets containing a diagonal we have $\nu=1$ for $|A|=2$ and $\nu=0$ for $|A|=3$. For $|A|=4$, $\nu=-1$ for two diagonals, which is a square, and $\nu=0$ for one diagonal together with one vertex of each other diagonal. Finally $\nu=0$ for $|A|=5$ and $\nu=1$ for $|A|=6$. This proves the statement about $\nu$, and with it the first inequality. The second is proved in Appendix~\ref{app:square}.
\end{proof}

\subsection{The smooth part}\label{ssec:smooth}

By the symmetry of $D_4$, the first partial derivatives of $\Phi$ at $\zeta_0$ are $g_h=\partial\Phi/\partial h_i$ and $g_u=\partial\Phi/\partial u_{ij}$, the same for all $i$ and all $\{i,j\}\in T$. Write $\Phi_{hh},\Phi_{hu},\Phi_{uu}$ for the blocks of the Hessian $D^2\Phi(\zeta_0)$, and define the quadratic form
\[
\widetilde\Hs(\xi,\xi)=2g_u\,Q_t(\tau)+D^2\Phi(\zeta_0)\bigl[(\eta,\Lambda\tau)\bigr]^2,\qquad \xi=(\tau,\eta)\in\R^{72}\times\R^{24},
\]
with $Q_t$ as in Lemma~\ref{lem:gauge}(4). By Lemma~\ref{lem:gauge}(3), $\frac12\widetilde\Hs(\xi,\xi)$ is the second-order part of $\xi\mapsto\Phi(h,u_T)$. Let $M_\sigma$ be the $24\times72$ matrix with $(M_\sigma\tau)_k=\sigma_k(\tau):=\sum_{j=1}^3(\Lambda_O\tau)_{a_{kj}a'_{kj}}$, the sum of the first-order changes of the three orthogonal inner products at the vertex $v_k$. Let $E$ be the $24\times24$ matrix with $E_{kb}=1$ if $b\in N(k)$ and $E_{kb}=0$ otherwise.

\begin{lemma}[computer-assisted]\label{lem:deriv}
\begin{enumerate}
\item $|g_h-\frac43|\le10^{-22}$ and $|g_u-\frac14|\le10^{-22}$. The entries of $\Phi_{hh}$, $\Phi_{hu}$ and $\Phi_{uu}$ differ by at most $10^{-22}$ from those of the rational matrices $\Phi_{hh}^0$, $\Phi_{hu}^0$ and $\Phi_{uu}^0$ given by $(\Phi_{hh}^0)_{kk}=-4$, $(\Phi_{hh}^0)_{kl}=1$ if $\{k,l\}\in T$ and $0$ for the other $k\ne l$, $(\Phi_{hu}^0)_{k,ij}=-1$ if $k\in\{i,j\}$, $\frac13$ if $\{i,j,k\}$ is a contact triangle and $0$ otherwise, and $(\Phi_{uu}^0)_{ee}=1$, $(\Phi_{uu}^0)_{ef}=-\frac16$ if the distinct contact pairs $e,f$ lie in a common contact triangle and $0$ otherwise. Moreover $\|\Phi_{hu}^0\|=4$ and $0\preceq\Phi_{uu}^0\preceq\frac32I$.
\item Let $D^2\Phi^0$ be the symmetric matrix with blocks $\Phi_{hh}^0,\Phi_{hu}^0,\Phi_{uu}^0$, and define the quadratic form $\Hs(\xi,\xi)=\frac12Q_t(\tau)+D^2\Phi^0\bigl[(\eta,\Lambda\tau)\bigr]^2$. Then $\|\widetilde\Hs-\Hs\|\le1.3\cdot10^{-20}$, and the blocks of $\Hs$ satisfy:
\begin{enumerate}
\item $0\preceq\Hs_{\tau\tau}$, with largest eigenvalue $\frac53$;
\item $\Hs_{\eta\tau}$ vanishes on $\ker\Hs_{\tau\tau}$; hence $L:=\Hs_{\tau\tau}^+\Hs_{\tau\eta}$ satisfies $\Hs_{\tau\tau}L=\Hs_{\tau\eta}$, and $\|L\|^2=12$;
\item the Schur complement $Z=\Hs_{\eta\eta}-\Hs_{\tau\eta}^{\top}L$ satisfies $Z\succeq-8I$;
\item $9\,\Hs_{\tau\tau}-M_\sigma^{\top}M_\sigma\succeq0$ and $\|E+M_\sigma L\|=6$.
\end{enumerate}
\end{enumerate}
\end{lemma}

The blocks of $\Hs$, the pseudo-inverse in (2)(b) and the matrices $M_\sigma$, $L$ are taken in the orthonormal coordinates $\tau\in\R^{72}$, $\eta\in\R^{24}$ (cf.\ Section~\ref{ssec:roots}). The form $\Hs$ is the Hessian at $\xi=0$ of the volume of $P$ (Table~\ref{tab:verif}). The draft~\cite{BBMBd} also computes this Hessian at the 24-cell. Part (2)(b) gives, for $\tau'=\tau+L\eta$,
\begin{equation}\label{eq:schur}
\Hs(\xi,\xi)=\tau'^{\top}\Hs_{\tau\tau}\tau'+\eta^{\top}Z\eta\ \ge\ \tau'^{\top}\Hs_{\tau\tau}\tau'-8|\eta|^2 .
\end{equation}
So the quadratic part of the expansion is bounded below by $-4|\eta|^2\ge-4\bar\eta s$. The tilts do not enter at first order: the first-order term in $u_T$ is $g_u\sum_T\Delta u_{ij}=g_uQ_d$, which is of second order by Lemma~\ref{lem:gauge}(3); this is where the constant stress enters.

Let $\varepsilon_0=10^{-20}$. For $b_e,b_u>0$ let $\mathbf B(b_e,b_u)$ be the box of heights $h_a\in[1,1+b_e]$ and inner products $u_{ab}\in[\frac12-b_u,\frac12+b_e]$.

\begin{lemma}[computer-assisted]\label{lem:remainder}
Suppose that $\bar\eta\le b_e$ and $\bar u\le b_u$ for one of the boxes $\mathbf B_m=\mathbf B(m/100,m/50)$, $m=1,\dots,5$. Then
\[
\Phi(h,u_T)-8-\bigl(\tfrac43-\varepsilon_0\bigr)s-\tfrac12\Hs(\xi,\xi)\ \ge\ -A_e^{(3)}|\eta|^2-A_t^{(3)}|\tau|^2 ,
\]
with the constants $A_e^{(3)},A_t^{(3)}$ of Appendix~\ref{app:remainder}, which depend on $\bar\eta$, $\bar d$, a weight $\kappa_1>0$ and bounds for the third partial derivatives of $\Pi$ and $\Theta$ on the box.
\end{lemma}

The proof is in Appendix~\ref{app:remainder}, which also describes how the bounds on the third derivatives are obtained. The certification of Theorem~\ref{thm:local} leaves some room in these inputs: it still succeeds if all bounds on third derivatives are multiplied by $4.09$, or if only $C_r\le1.444$ is used in place of $C_r^2\le\frac{191}{100}$.

\subsection{The hull deficit}\label{ssec:deficit}

The cell can lose volume only near the $24$ points $\sqrt2\,v_k$, where $J_0$ touches the sphere $|x|=\sqrt2$. There the hull $J$ is close to the facet $\conv\{2u_b:b\in N(k)\}$ of $J_0$. Put $e_{kj}=\eta_{a_{kj}}+\eta_{a'_{kj}}$. To first order, the part of $(P\cap B)\setminus J$ near $\sqrt2\,v_k$ is empty unless $e_{kj}>u_{a_{kj}a'_{kj}}$ for $j=1,2,3$, and its depth and its widths in the directions $f_{kj}$ are bounded by these excesses. So its volume is of fourth order~\cite{BBMBd}.

\begin{lemma}\label{lem:deficit}
Let $\kappa_2,\kappa_3>0$, and suppose that the region condition~\eqref{eq:region} of Appendix~\ref{app:hull} holds at every step of the iteration described there. Then, with $\tau'=\tau+L\eta$,
\[
\vol\bigl((P\cap B)\setminus J\bigr)\ \le\ A_\sigma\sum_{k=1}^{24}\sigma_k(\tau')^2+A_e^{\rm h}|\eta|^2+A_t^{\rm h}|\tau|^2 ,
\]
where $A_\sigma,A_e^{\rm h},A_t^{\rm h}$ are given by~\eqref{eq:hullconst} in terms of $\bar\eta$, $\bar d$, $\kappa_2$ and $\kappa_3$.
\end{lemma}

The proof is in Appendix~\ref{app:hull}. By Lemma~\ref{lem:deriv}(2)(d), $\sum_k\sigma_k(\tau')^2=|M_\sigma\tau'|^2\le9\,\tau'^{\top}\Hs_{\tau\tau}\tau'$. So the first term is absorbed by the nonnegative term in~\eqref{eq:schur} when $9A_\sigma\le\frac12$.

\subsection{Proof of \texorpdfstring{Theorem~\ref{thm:local}}{Theorem 1.2}}\label{ssec:assembly}

Let $\kappa_1,\kappa_2,\kappa_3,\kappa_4>0$ be weights. We use the following conditions on $(\rho,\sigma)$, with $\bar d=D_{\rm eff}$:
\begin{enumerate}
\item[(C1)] $\beta_0<1$ in Corollary~\ref{cor:boot};
\item[(C2)] $2\varphi<\pi/6$;
\item[(C3)] $\zeta_O\le1-\sqrt2\,\bar d$, $64\bar d^2<1$, and $\varepsilon_q<\sqrt2$, where $\varepsilon_q=2\bar\eta/(1+\bar\eta)+2\bar d$;
\item[(C4)] $\bar\eta\le b_e$ and $\bar u\le b_u$ for one of the boxes $\mathbf B_m$;
\item[(C5)] the region condition~\eqref{eq:region} at every step of the iteration of Appendix~\ref{app:hull};
\item[(C6)] $\Gamma>0$, where $\Gamma$ is defined in~\eqref{eq:Gamma} below.
\end{enumerate}

By Lemma~\ref{lem:hull}, $\vol(V_0)\ge\mathcal F-\vol((P\cap B)\setminus J)$. By Lemma~\ref{lem:decomp}, $\mathcal F\ge\Phi-A_{\rm sq}|\tau|^2$. Lemma~\ref{lem:remainder}, inequality~\eqref{eq:schur} and Lemma~\ref{lem:deficit} then give
\[
\vol(V_0)-8\ \ge\ \bigl(\tfrac43-\varepsilon_0\bigr)s+\bigl(\tfrac12-9A_\sigma\bigr)\tau'^{\top}\Hs_{\tau\tau}\tau'-(4+A_e)|\eta|^2-A_t|\tau|^2 ,
\]
with $A_e=A_e^{(3)}+A_e^{\rm h}$ and $A_t=A_t^{(3)}+A_{\rm sq}+A_t^{\rm h}$. If $9A_\sigma\le\frac12$, the middle term is nonnegative and we drop it. Otherwise we use $\Hs_{\tau\tau}\preceq\frac53I$ and $|\tau'|^2\le(1+\kappa_4)|\tau|^2+(1+\kappa_4^{-1})\|L\|^2|\eta|^2$ with $\|L\|^2=12$, and add $(9A_\sigma-\frac12)\frac53(1+\kappa_4)$ to $A_t$ and $(9A_\sigma-\frac12)\frac53(1+\kappa_4^{-1})\cdot12$ to $A_e$. Finally $|\eta|^2\le\bar\eta s$, and $|\tau|^2\le\tau_{\max}C_r''s$ by Corollary~\ref{cor:boot}. Hence
\begin{equation}\label{eq:Gamma}
\vol(V_0)-8\ \ge\ \Gamma s,\qquad \Gamma=\tfrac43-\varepsilon_0-(4+A_e)\,\bar\eta-A_t\,\tau_{\max}C_r'' .
\end{equation}

All quantities in (C1)--(C6) are explicit. They were evaluated, together with the choice between the two cases for $9A_\sigma$, using $C_r=(191/100)^{1/2}$, the third-derivative bounds of Lemma~\ref{lem:remainder} and $300$ steps of the iteration of Appendix~\ref{app:hull} (Table~\ref{tab:verif}). At the main row the computation gives $\Gamma\ge0.2437$ (Table~\ref{tab:mainrow}), which proves the inequality of Theorem~\ref{thm:local}. Every row of Table~\ref{tab:pairs} gives a theorem of the same form; for instance, $d(W)\le\frac9{20}$ and $\sum_i\delta_i\le\frac1{125}$ imply $\vol(V_0)\ge8+1.3111\,s$. At the main row the depth bound $\hat\Delta$ of Appendix~\ref{app:hull} keeps its starting value $\varepsilon_q$; the iteration there improves only $\bar Y$ and $\tilde Y$.

\begin{table}[ht]
\caption{Certified pairs $(\rho,\sigma)$: with the weights and box listed, conditions (C1)--(C6) hold, and $\vol(V_0)\ge8+\Gamma s$ whenever $d(W)\le\rho$ and $\sum_i\delta_i\le\sigma$. The column $\Gamma$ gives the certified lower bound rounded down to four decimals, and the column $D_{\rm eff}$ the certified upper bound rounded up to six decimals.}\label{tab:pairs}
\small
\begin{tabular}{llllll}
\toprule
$\rho$ & $\sigma$ & $\Gamma\ge$ & $D_{\rm eff}$ & $(\kappa_1,\kappa_2,\kappa_3,\kappa_4)$ & box\\
\midrule
$2/5$ & $1/125$ & $1.3111$ & $0.005593$ & $(1,8,1,\frac12)$ & $\mathbf B_1$\\
$9/20$ & $1/125$ & $1.3111$ & $0.005593$ & $(1,8,1,\frac12)$ & $\mathbf B_1$\\
$2/5$ & $1/50$ & $1.1951$ & $0.014242$ & $(\frac12,4,4,\frac12)$ & $\mathbf B_2$\\
$2/5$ & $1/40$ & $0.9535$ & $0.017944$ & $(\frac12,2,4,\frac12)$ & $\mathbf B_2$\\
$2/5$ & $3/100$ & $0.2437$ & $0.021709$ & $(\frac12,2,4,2)$ & $\mathbf B_2$\\
$2/5$ & $31/1000$ & $0.0026$ & $0.022470$ & $(\frac12,2,4,2)$ & $\mathbf B_2$\\
\bottomrule
\end{tabular}
\end{table}

\begin{table}[ht]
\caption{The budget of~\eqref{eq:Gamma} at the main row of Table~\ref{tab:pairs}, with the weights $(\frac12,2,4,2)$ and the box $\mathbf B_2$, per unit of $s$. The losses are rounded as shown, and $\Gamma$ is rounded down. They follow, as in Section~\ref{ssec:assembly}, from the constants recorded for the main row in the supplement~\cite{supp}.}\label{tab:mainrow}
\small
\begin{tabular}{L{10.4cm}l}
\toprule
term & per unit of $s$\\
\midrule
first-order gain (Lemma~\ref{lem:remainder}) & $\frac43-\varepsilon_0$\\
hull deficit (Lemma~\ref{lem:deficit}), including the term added because $9A_\sigma>\frac12$ & $-0.94$\\
other losses: third-order remainder (Lemma~\ref{lem:remainder}), quadratic part~\eqref{eq:schur}, square overlaps (Lemma~\ref{lem:decomp}) & $-0.15$\\
total loss, using $|\tau|^2\le\tau_{\max}C_r''s$ (Corollary~\ref{cor:boot}) & $-1.0896$\\
$\Gamma$ & $0.243742$\\
\bottomrule
\end{tabular}
\end{table}

\emph{Equality.} If $s>0$, then $\vol(V_0)-8\ge\Gamma s>0$. If $s=0$, Corollary~\ref{cor:boot} gives $|\tau|\le C_r''s=0$, so $t_i=0$, $d_i=0$ and $y_i=2u_i$ for all $i$, in the labelling and frame fixed in Section~\ref{ssec:rigid}. Then $q_i=2u_i$ and $J=J_0$, and $P=\{x:\langle x,u_i\rangle\le1\}$ is the regular 24-cell with vertices $\sqrt2\,v_k$. These satisfy $\langle\sqrt2v_k,v_{k'}\rangle\le\sqrt2$, so $P\subseteq J_0$. By Lemma~\ref{lem:hull}, $V_0\supseteq P\cap J=P$, and $V_0\subseteq P$, so $V_0=P$ and $\vol(V_0)=8$. The same argument shows that $\vol(V_0)=8$ whenever $\{y_1,\dots,y_{24}\}=2R\{u_1,\dots,u_{24}\}$ for some $R\in O(4)$. This completes the proof of Theorem~\ref{thm:local}. \qed

\begin{remark}[Effective size and nearest centres]\label{rem:effective}
We prove the claims made after Theorem~\ref{thm:local}. Corollary~\ref{cor:boot} gives $d(W)=\|d\|\le D_{\rm eff}<0.021709$, so no $24$ centres of a packing containing $0$ with $d(W)$ between this value and $\frac25$ have $\sum_i\delta_i\le\tfrac3{100}$. The hypothesis $d(W)\le\frac25$ gives the starting value $D_0=\frac25$ of the iteration of Corollary~\ref{cor:boot}, for which condition (C1) is checked.

Next, every centre $z\notin\{0,y_1,\dots,y_{24}\}$ satisfies $|z|>2.72$. Indeed, the 24-cell $\{x:\langle x,u_i\rangle\le1\}$ has circumradius $\sqrt2$, so $\langle z,u_i\rangle\ge|z|/\sqrt2$ for some $i$, and then $|z-2u_i|^2\le|z|^2-2\sqrt2|z|+4=(|z|-\sqrt2)^2+2$. In the frame of Section~\ref{ssec:rigid}, $|y_i-2u_i|\le2\eta_i+2|d_i|<0.0735$, so $|z-2u_i|>2-0.0735$ by the packing condition. Since $|z|\ge2$, this gives $(|z|-\sqrt2)^2>1.9265^2-2>1.7114$ and $|z|>2.72$. So $y_1,\dots,y_{24}$ are the $24$ centres nearest to $0$, and the only centres within distance $\sqrt6$.
\end{remark}

\begin{remark}[Sharpness]\label{rem:sharp}
The coefficient $\frac43$ is $g_h$, and it cannot be improved. Let the packing consist of $0$ and the centres $2u_i$, except that $y_1=2(1+\eta)u_1$ with $0<\eta<1$; this is a packing, and $d(W)=0$. The cell is the 24-cell with one facet moved from $\langle x,u_1\rangle=1$ to $\langle x,u_1\rangle=1+\eta$. The hyperplanes of the eight neighbouring facets pass through $2u_1$, and the pyramid over the facet with apex $2u_1$ has height $1$, like the pyramid with apex $0$, so its volume is $8/24=\frac13$. The cell gains the part of this pyramid at height at most $\eta$, so $\vol(V_0)=8+\frac13(1-(1-\eta)^4)$, and $(\vol(V_0)-8)/s=(1-(1-\eta)^4)/(3\eta)<\frac43$ (this example is also in~\cite{BBMBd}). For the largest push allowed by Theorem~\ref{thm:local}, $\eta=\tfrac3{200}$, the ratio equals $1.3036\ldots$, slightly less than $\frac43$. Numerically, configurations with exact rational coordinates sampled at the corner of the region of Theorem~\ref{thm:local}, including extreme tilts and further centres, never give a smaller exact ratio than this single push~\cite{supp}. The certified constant is far below these values.
\end{remark}

\begin{remark}[Limits of the method]\label{rem:limits}
In $\sigma$, the method is limited by the second-order terms of the hull deficit: at $\rho=\frac25$ the certified constant falls to $0.0026$ at $\sigma=\frac{31}{1000}$, and with the weights $(\frac12,2,8,2)$ the computation gives a negative lower bound for $\Gamma$ at $\sigma=\frac1{25}$. In $\rho$, the method is limited by the first step of the rigidity iteration: (C1) fails at $(\frac{23}{50},\frac1{125})$, and at $(\frac9{20},\frac1{50})$ the iteration of Corollary~\ref{cor:boot} does not reduce $D_n$ below $\frac9{20}$, so (C2) fails.
\end{remark}

\section{Verification}\label{sec:lean}

Table~\ref{tab:verif} lists, for the results behind Theorems~\ref{thm:main} and~\ref{thm:local}, how each is checked and what is formalised in Lean. The computations are done by the programs of the supplement~\cite{supp}. Unless ball or interval arithmetic~\cite{Arb} is stated, they are exact, in rational or in modular arithmetic. A comparison made in ball or interval arithmetic holds for every point of the balls or intervals involved.

Parts of Sections~\ref{sec:trunc}--\ref{sec:proof} and of Section~\ref{sec:local} are formalised in Lean~4 with Mathlib. A theorem is \emph{kernel-checked} if its only axioms are the three standard ones of Lean, so that every step has been checked by Lean's kernel. It is \emph{native} if some finite computations are evaluated by compiled code, which adds the Lean compiler, its runtime and the compiled libraries to the trusted base. In the formal statements, space is $\R^4$ with Lebesgue measure, half-spaces and the ball $B$ are open as in Section~\ref{sec:trunc}, and a packing is any set of points, possibly infinite, at mutual distance at least~$2$. For the arithmetic of the certificate, the kernel works on a copy of the certificate in Lean, whose agreement with the deposited certificate is verified by independent programs outside Lean. For Theorem~\ref{thm:cert}, native evaluation shows that each row of the certificate is the value at its sample point of a row function built by a Lean reimplementation of the zonal assembly of~\cite{LLdMK}, and that the triple row functions are invariant under relabelling, as the invariant sample sets require. The versions of Theorems~\ref{thm:cert} and~\ref{thm:main} specialised to the certificate make two assumptions on the certificate:
\begin{enumerate}
\item[(H1)] inequality~\eqref{eq:psd} holds, for every kissing configuration, for the kernel that the $60$ kernel blocks of the certificate define through the zonal functions of the reimplementation;
\item[(H2)] the row function of the quadruple piece, an explicit polynomial in the six inner products, is invariant under the relabellings of the four points.
\end{enumerate}
Hypothesis (H1) contains the positivity theorem of~\cite{LLdMK}, the faithfulness of the reimplementation to the construction there, and the correctness of the zonal entries, which agree with those computed by the code of~\cite{LLdMK}. The formal proof of Theorem~\ref{thm:local} assumes, for every packing and centres $y_1,\dots,y_{24}$ as in the theorem with $c=0$, and in (h1)--(h4) for every labelling and $R$ as in (h0), with certified upper bounds for the constants of the main row:
\begin{enumerate}
\item[(h0)] a labelling and an $R\in O(4)$ attaining $d(W)$ exist, which follows from the compactness of $O(4)$;
\item[(h1)] the bound of Lemma~\ref{lem:decomp} holds;
\item[(h2)] the inequality of Lemma~\ref{lem:deficit} holds;
\item[(h3)] the bounds on $|\tau|$ of Corollary~\ref{cor:boot} hold;
\item[(h4)] the inequality of Lemma~\ref{lem:remainder} holds.
\end{enumerate}
The supplement~\cite{supp} gives these constants exactly, states the hypotheses in full and documents the formal proofs.

\begin{table}[tbp]
\caption{Verification. ``Kernel'' means kernel-checked, and ``native'' that some finite computations are evaluated by compiled code.}\label{tab:verif}
\footnotesize
\setlength{\tabcolsep}{4pt}
\begin{tabular}{L{2.7cm}L{6.1cm}L{5.9cm}}
\toprule
result & how it is checked & in Lean\\
\midrule
the results of Section~\ref{sec:trunc} and Proposition~\ref{prop:duality} & proofs in the text & kernel; Lemma~\ref{lem:D4} via the covolume of $\sqrt2D_4$, without identifying $V_0$ as the 24-cell\\
the certificate of Theorem~\ref{thm:cert} & identities at the sample points and the identity fixing $\kappa$, right-hand sides $-\omega_1^+$, $p_2$, $-p_3$, $0$: exact\newline blocks positive definite: Cholesky, ball arithmetic\newline unisolvence of the sample sets ($17$ points for pairs; $204$ and $3679$, the dimensions of the $S_3$- and $S_4$-invariant polynomials of degree $\le16$): full rank modulo a prime\newline triple and quadruple identities on the principal lattices $\{a/16:\ a\in\mathbb Z_{\ge0}^m,\ |a|\le16\}$, $m=3,6$, without invariance assumptions: exact & polynomials $g$ of Section~\ref{sec:cert} nonnegative on their pieces: kernel\newline these facts, except those on the principal lattices, and $K(\emptyset,\emptyset)+23\mu=1828197/156250$ with $\mu>0$: kernel\newline Theorem~\ref{thm:cert} for the certificate: native, under (H1) and (H2)\\
Lemma~\ref{lem:approx} & interval arithmetic (Section~\ref{sec:approx}) & (1): kernel, with $\omega_1^+$ read natively from the certificate\newline (2): closed form of $\omega_2$ kernel, inequality native\newline (3): not formalised\\
Theorem~\ref{thm:main} & proof in Section~\ref{sec:proof} & kernel, from the bound of Theorem~\ref{thm:cert}, Lemma~\ref{lem:approx}, \cite{Mus} and~\cite{LLdMK}\newline for the certificate: native, under (H1), (H2), Lemma~\ref{lem:approx}(3), \cite{Mus} and~\cite{LLdMK}\\
facts on $D_4$ and $J_0$ (Section~\ref{ssec:roots}) & exact, with $J_0$ by vertex enumeration & counts of roots, contact pairs and contact triangles: kernel\\
Lemma~\ref{lem:Lambda} & spectrum of $\Lambda^{\top}\Lambda$: exact, in two coordinate systems & $\ker\Lambda$, $|\Lambda\tau|\ge|\tau|$ for $\tau\perp\ker\Lambda$, $\|\Lambda\|=2$ and the constant stress: kernel\newline the rest of the spectrum: not formalised\\
$C_r^2\le191/100$ (Lemma~\ref{lem:rigid}) & exact identity; $M_0\ge0$ entrywise, $N_0\succeq0$ of rank $90$ by $LDL^{\top}$ & the certificate: kernel; it enters only through (h3)\\
$\Hs$ (Lemma~\ref{lem:deriv}(2)) & exact $LDL^{\top}$ and spectra\newline eigenvalues of $\Hs_{\tau\tau}$: $0,1/6,2/3,1,4/3,5/3$, multiplicities $15,16,12,12,9,8$\newline characteristic polynomial of $Z$: $(x+8)^{14}(x+20/3)^9(x-4)$\newline in the coordinates $\tau^{\rm s}$, equal to the Hessian of the volume of $P$ computed in~\cite{supp} & parts (a)--(d), with the eigenvalue $5/3$ and $\|L\|^2=12$ as upper bounds, (c) as $\Hs(\xi,\xi)\ge-8|\eta|^2$, without $\|E+M_\sigma L\|=6$; the characteristic polynomial of $Z$; the identity with the matrix of~\cite{supp}: kernel\\
Lemma~\ref{lem:deriv}(1) & derivatives of $S,\Pi,\Theta$ at $\zeta_0$: ball arithmetic, within $10^{-22}$ of the rationals\newline $\|\Phi_{hu}^0\|=4$ and $0\preceq\Phi_{uu}^0\preceq(3/2)I$: exact & the derivative values: not formalised\\
Lemma~\ref{lem:remainder} & third derivatives of $\Pi,\Theta$ on $\mathbf B_1,\dots,\mathbf B_5$: Taylor models in ball arithmetic (Appendix~\ref{app:remainder}) & not formalised; enters as (h4)\\
(C1)--(C6) and $\Gamma$ (Tables~\ref{tab:pairs} and~\ref{tab:mainrow}) & ball arithmetic & $\Gamma\ge0.2437$ from the certified constants: kernel\\
Theorem~\ref{thm:local} & proof in Section~\ref{sec:local} & kernel, from (h0)--(h4), for $c=0$, without identifying $V_0$ with the regular 24-cell\newline Lemma~\ref{lem:hull} and inequality~\eqref{eq:schur}: kernel\\
\bottomrule
\end{tabular}
\end{table}

\appendix

\section{Proofs for \texorpdfstring{Section~\ref{sec:local}}{Section 7}}\label{app:proofs}

Throughout, the notation of Section~\ref{sec:local} is in force, with $\bar d=D_{\rm eff}$ and conditions (C2)--(C4) of Section~\ref{ssec:assembly}. In particular $\bar d$ bounds $\|d\|$ and every $|d_i|$, and $0\le\eta_i\le\bar\eta$.

\subsection{The square overlaps}\label{app:square}

We prove the second inequality of Lemma~\ref{lem:decomp}. Let $Q$ be a square at the vertex $v_k$, formed by the orthogonal pairs $\{a_1,a'_1\}$ and $\{a_2,a'_2\}$. Apply Lemma~\ref{lem:pair} to each pair, with $w=w_{a_r}$, $w'=w_{a'_r}$, $h=h_{a_r}$ and $h'=h_{a'_r}$, and denote the resulting quantities by $\alpha_r,\alpha'_r,p_r,n_r,\check h_r,\hat c_r,\hat g_r$ for $r=1,2$. Suppose the four caps of $Q$ meet, so that $\hat g_1,\hat g_2>0$. By Lemma~\ref{lem:pair}, a common point $x$ satisfies
\[
\hat c_1<\langle x,p_1\rangle<\sqrt2,\qquad |\langle x,n_1\rangle-\check h_1|<\frac{\alpha_1}{\alpha'_1}\bigl(\langle x,p_1\rangle-\hat c_1\bigr),\qquad |\langle x,n_2\rangle-\check h_2|<\frac{\alpha_2}{\alpha'_2}\,\hat g_2 ,
\]
the last because $\langle x,p_2\rangle<\sqrt2$. Let $\mathrm{Pr}$ be the orthogonal projection onto the plane orthogonal to $p_1$ and $n_1$. For fixed $\langle x,p_1\rangle$ and $\langle x,n_1\rangle$, the projection $\mathrm{Pr}\,x$ lies in a disc of radius $(2-\langle x,p_1\rangle^2)^{1/2}$ and in a strip of width $2(\alpha_2/\alpha'_2)\hat g_2/|\mathrm{Pr}\,n_2|$. Put $\lambda=\sqrt2-\langle x,p_1\rangle\in(0,\hat g_1)$. Then $\langle x,p_1\rangle-\hat c_1=\hat g_1-\lambda$ and $2-\langle x,p_1\rangle^2\le2\sqrt2\,\lambda$, so
\[
\vol\Bigl(\bigcap_{a\in Q}K_{y_a}\Bigr)\le\int_0^{\hat g_1}2\frac{\alpha_1}{\alpha'_1}(\hat g_1-\lambda)\cdot4\frac{\alpha_2}{\alpha'_2}\frac{\hat g_2}{|\mathrm{Pr}\,n_2|}(2\sqrt2\,\lambda)^{1/2}\,d\lambda=\frac{32}{15}2^{3/4}\frac{\alpha_1\alpha_2}{\alpha'_1\alpha'_2}\frac{\hat g_1^{5/2}\hat g_2}{|\mathrm{Pr}\,n_2|},
\]
and the same holds with $1$ and $2$ exchanged. By Lemma~\ref{lem:gauge}(6), $\alpha_r/\alpha'_r=((1+u)/(1-u))^{1/2}\le((1+\bar u_\perp)/(1-\bar u_\perp))^{1/2}$. As in the proof of Lemma~\ref{lem:activity}, $|p_r-v_k|\le2\sqrt2\,\bar d$, and likewise $|n_r-f_{kj_r}|\le2\sqrt2\,\bar d$, where $j_r$ is the index of the pair. Since $f_{kj_2}$ is orthogonal to $v_k$ and $f_{kj_1}$, we get $|\langle n_2,p_1\rangle|,|\langle n_2,n_1\rangle|\le4\sqrt2\,\bar d$ and $|\mathrm{Pr}\,n_2|^2\ge1-64\bar d^2$. With $\hat g_r\le u_{a_ra'_r}/\sqrt2\le\bar g$ (Lemma~\ref{lem:pair}) this gives
\[
\vol\Bigl(\bigcap_{a\in Q}K_{y_a}\Bigr)\le k_{\rm sq}\,\hat g_1\hat g_2\min(\hat g_1,\hat g_2)^{3/2}\le\tfrac12k_{\rm sq}\,\bar g^{3/2}\bigl(\hat g_1^2+\hat g_2^2\bigr).
\]
Each orthogonal pair lies in exactly two squares, and $\hat g^+\le u^+/\sqrt2$ for each pair, so the sum over all squares is at most $\frac12k_{\rm sq}\bar g^{3/2}\sum_O(u_{ij}^+)^2$. By Lemma~\ref{lem:gauge}(3) and Lemma~\ref{lem:Lambda}(3),
\[
\Bigl(\sum_Ou_{ij}^2\Bigr)^{1/2}\le\|\Lambda_O\|\,|\tau|+\Bigl(\sum_O|d_i|^2|d_j|^2\Bigr)^{1/2}\le\bigl(2+\sqrt3\,\bar d\chi^{1/2}\bigr)|\tau| ,
\]
because each root lies in six orthogonal pairs, so that $\sum_O|d_i|^2|d_j|^2\le\frac{\bar d^2}2\sum_O(|d_i|^2+|d_j|^2)=3\bar d^2\|d\|^2\le3\bar d^2\chi|\tau|^2$. This proves $\mathcal N\ge-A_{\rm sq}|\tau|^2$.

\subsection{The hull deficit}\label{app:hull}

We prove Lemma~\ref{lem:deficit}. Put $\varepsilon_q=2\bar\eta/(1+\bar\eta)+2\bar d$. Then $|q_i-2u_i|\le2(1-1/h_i)+2|d_i|\le\varepsilon_q$ for all $i$. By (C3), $\varepsilon_q<\sqrt2$; on the certified pairs of Table~\ref{tab:pairs}, $\varepsilon_q\le0.0755$. This condition is used three times: for the positive factor $1-\varepsilon_q/\sqrt2$ in (a), for $\langle x,v_k\rangle>0$ on $C_k$, which makes $t_*$ well defined in Lemma~\ref{lem:height}(2), and for $\sqrt2-\hat\Delta>0$ in $t_{\max}$.

\emph{(a) Localisation.} For a unit vector $e$, the support functions satisfy $h_J(e)\ge\max_i\langle q_i,e\rangle\ge h_{J_0}(e)-\varepsilon_q\ge(1-\varepsilon_q/\sqrt2)\,h_{J_0}(e)$, because $h_{J_0}\ge\sqrt2$. Since $1-\varepsilon_q/\sqrt2>0$, the right-hand side is the support function of $(1-\varepsilon_q/\sqrt2)J_0$, so $J\supseteq(1-\varepsilon_q/\sqrt2)J_0=\{x:\langle x,v_k\rangle\le\sqrt2-\varepsilon_q\text{ for all }k\}$. So $(P\cap B)\setminus J$ is contained in the union of the sets $X_k=(P\cap C_k)\setminus J$, where $C_k=\{x\in B:\langle x,v_k\rangle>\sqrt2-\varepsilon_q\}$. For $x\in C_k$ we have $\langle x,v_k\rangle>\sqrt2-\varepsilon_q>0$, and the vector $z=x-\sqrt2v_k$ satisfies $|z|^2=|x|^2-2\sqrt2\langle x,v_k\rangle+2<2\sqrt2(\sqrt2-\langle x,v_k\rangle)<2\sqrt2\,\varepsilon_q$.

Fix $k$ for the rest of the proof, and write $v=v_k$ and $f_j=f_{kj}$. For $j=1,2,3$ write $j+=a_{kj}$ and $j-=a'_{kj}$, so that $u_{j\pm}=(v\pm f_j)/\sqrt2$. For $b\in N(k)$ let $j(b)$ be its pair and $s_b=\pm1$ its sign. For $x\in\R^4$ write $z=x-\sqrt2v=z_0v+z_\perp$ with $z_\perp=\sum_lz_lf_l$. Since $q_b=(2/h_b)(u_b+d_b)$,
\[
q_b-\sqrt2v=\theta_bv+P_b,\qquad P_b=s_b\sqrt2\,f_{j(b)}+r_b,
\]
with $\theta_b=\sqrt2(h_b^{-1}-1)+2h_b^{-1}\langle v,d_b\rangle$ and $r_b=s_b\sqrt2(h_b^{-1}-1)f_{j(b)}+2h_b^{-1}(d_b-\langle v,d_b\rangle v)$. If $b'$ is the partner of $b$, then $v=(u_b+u_{b'})/\sqrt2$, so $\langle v,d_b\rangle=(\langle u_{b'},t_b\rangle+n_b)/\sqrt2$ and $|\langle v,d_b\rangle|\le\bar\nu|d_b|$ with $\bar\nu=(1+\bar d/2)/\sqrt2$. Hence $|\theta_b|\le\sqrt2\eta_b+2\bar\nu|d_b|$ and $|r_b|\le\sqrt2\eta_b+2|d_b|$. Put $\bar\theta_j=\frac12(\theta_{j+}+\theta_{j-})$, $\mathrm{spr}_j=\max_{l\ne j,\pm}|\theta_{l\pm}-\bar\theta_j|$ and $\bar r=\max_b|r_b|$.

\emph{(b) Height of the hull.} Let $\Omega=\conv\{q_b:b\in N(k)\}\subseteq J$, and let $\Omega^\perp$ be its orthogonal projection to $v^\perp$, which is the convex hull of the $P_b$. For $y\in\Omega^\perp$ let $\mathrm{hup}(y)$ and $\mathrm{low}(y)$ be the largest and the smallest $t$ with $\sqrt2v+y+tv\in\Omega$. For $y\in v^\perp$ write $y_l=\langle y,f_l\rangle$ and $|y|_1=\sum_l|y_l|$.

\begin{lemma}\label{lem:height}
\begin{enumerate}
\item If $|y|_1+\sqrt3\,\bar r\le\sqrt2$, then $y\in\Omega^\perp$ and, for each $j$, with $l_1,l_2$ the other two indices,
\[
\mathrm{hup}(y)\ \ge\ \bar\theta_j-\frac{|y_j|+\bar r}{2\sqrt2}\,|\theta_{j+}-\theta_{j-}|-\frac{|y_{l_1}|+|y_{l_2}|+2\bar r}{\sqrt2}\,\mathrm{spr}_j .
\]
\item Let $x\in C_k$, $z=x-\sqrt2v$ and $\hat\theta\ge\max_b|\theta_b|$, and suppose that $t|z_\perp|_1+\sqrt3\,\bar r<\sqrt2$ for all $t\in[1,t_*]$, where $t_*=(\sqrt2+\hat\theta)/(\sqrt2+z_0)$; note that $t_*>1$, because $z_0<0$ for $x\in B$. If $x\notin J$, then $z_0>\mathrm{hup}(z_\perp)$.
\end{enumerate}
\end{lemma}

\begin{proof}
(1) For $y'\in v^\perp$ define $\lambda^0(y')\in\R^{N(k)}$ by $\lambda^0_{l\pm}(y')=\max(\pm y'_l,0)/\sqrt2$ for $l\ne j$ and $\lambda^0_{j\pm}(y')=\frac12(1-a(y'))\pm y'_j/(2\sqrt2)$, where $a(y')=(|y'_{l_1}|+|y'_{l_2}|)/\sqrt2$. Then $\lambda^0$ is continuous, $\sum_b\lambda^0_b=1$, $\sum_b\lambda^0_b(y')\,s_b\sqrt2f_{j(b)}=y'$, and $\lambda^0(y')\ge0$ if and only if $|y'|_1\le\sqrt2$. On the closed ball of radius $\bar r$ about $y$ we have $|y'|_1\le|y|_1+\sqrt3|y'-y|\le\sqrt2$, so $\lambda^0\ge0$ there, and the continuous map $y'\mapsto y-\sum_b\lambda^0_b(y')r_b$ maps this ball into itself. By Brouwer's theorem it has a fixed point $y^*$. With $\lambda=\lambda^0(y^*)$ we get $\lambda\ge0$, $\sum_b\lambda_b=1$ and $\sum_b\lambda_bP_b=y^*+\sum_b\lambda_br_b=y$. So $y\in\Omega^\perp$, and $\sum_b\lambda_bq_b=\sqrt2v+y+(\sum_b\lambda_b\theta_b)v\in\Omega$, whence $\mathrm{hup}(y)\ge\sum_b\lambda_b\theta_b$. For $l\ne j$ only one of $\lambda_{l+},\lambda_{l-}$ is nonzero, so
\[
\sum_b\lambda_b\theta_b=\bar\theta_j+\frac{y^*_j}{2\sqrt2}(\theta_{j+}-\theta_{j-})+\sum_{l\ne j}\frac{|y^*_l|}{\sqrt2}\bigl(\theta_{l,\pm}-\bar\theta_j\bigr),
\]
with the sign of $y^*_l$ in $\theta_{l,\pm}$. Since $|y^*_l|\le|y_l|+\bar r$, the bound follows.

(2) We show that $z_0\le\mathrm{hup}(z_\perp)$ implies $x\in J$; here $z_\perp\in\Omega^\perp$ by (1). For $t\ge1$ we have $tx=\sqrt2v+tz_\perp+\varrho(t)v$ with $\varrho(t)=t(\sqrt2+z_0)-\sqrt2$. Since $\sqrt2+z_0=\langle x,v\rangle>0$, $\varrho$ is increasing, and $\varrho(t_*)=\hat\theta$. By (1), every $tz_\perp$ with $t\in[1,t_*]$ lies in the interior of $\Omega^\perp$, where $\mathrm{hup}$ is concave and $\mathrm{low}$ is convex, hence both are continuous. Every point of $\Omega$ has height in $[\min_b\theta_b,\max_b\theta_b]$, so $\mathrm{low}\le\mathrm{hup}\le\hat\theta$. If $z_0\ge\mathrm{low}(z_\perp)$, then $x\in\Omega$. Otherwise $\varrho(t)-\mathrm{low}(tz_\perp)$ is negative at $t=1$ and nonnegative at $t=t_*$, so it vanishes at some $t_1\in(1,t_*]$. Then $\mathrm{low}(t_1z_\perp)=\varrho(t_1)\le\mathrm{hup}(t_1z_\perp)$, so $t_1x\in\Omega$ and $x=t_1^{-1}(t_1x)\in\conv(\{0\}\cup\Omega)\subseteq J$.
\end{proof}

Let $\hat\Delta\ge-z_0$, $\tilde Y\ge\max_l|z_l|$ and $\hat r\ge\bar r$ be bounds valid on $X_k$, and $\hat\theta\ge\max_b|\theta_b|$. Then $t_*\le t_{\max}:=1+(\hat\theta+\hat\Delta)/(\sqrt2-\hat\Delta)$ on $X_k$. If
\begin{equation}\label{eq:region}
3\,t_{\max}\tilde Y+\sqrt3\,\hat r<\sqrt2 ,
\end{equation}
then Lemma~\ref{lem:height}(2) applies on $X_k$, and every $x\in X_k$ satisfies $z_0>\bar\theta_j-\mathrm{err}_j(z)$ for each $j$, where
\[
\mathrm{err}_j(z)=\frac{|z_j|+\bar r}{2\sqrt2}\,|\theta_{j+}-\theta_{j-}|+\frac{|z_{l_1}|+|z_{l_2}|+2\bar r}{\sqrt2}\,\mathrm{spr}_j .
\]

\emph{(c) Volume.} For $b\in N(k)$ put $\psi_b=h_b-\sqrt2\langle v,w_b\rangle=\eta_b-\sqrt2\langle v,d_b\rangle$, and for each pair $l$ put $m_l=(\psi_{l+}+\psi_{l-})/\sqrt2$ and $o_l=(\psi_{l+}-\psi_{l-})/\sqrt2$. Let $x\in X_k$. Then $z_0<0$ because $\langle x,v\rangle\le|x|<\sqrt2$, and the facet inequalities $\langle x,w_{l\pm}\rangle\le h_{l\pm}$ read $(z_0\pm z_l)/\sqrt2\le\psi_{l\pm}-\langle z,d_{l\pm}\rangle$. Hence $z_l$ lies in the interval
\[
I_l=\bigl[\,o_l-(m_l-z_0)-\sqrt2|z||d_{l-}|,\ \ o_l+(m_l-z_0)+\sqrt2|z||d_{l+}|\,\bigr].
\]
Let $\bar Y\ge\sup_{X_k}|z|$, put $\Delta_j=-\bar\theta_j+\sup_{X_k}\mathrm{err}_j$ and $\Delta_*=\min_j\Delta_j$, and for $l=1,2,3$ put
\[
H_l=m_l+\Delta_*+\frac{\bar Y}{\sqrt2}\bigl(|d_{l+}|+|d_{l-}|\bigr),\qquad H_l^+=\max(H_l,0).
\]
By (b), $0<-z_0<\Delta_*$ on $X_k$, so $X_k=\emptyset$ if $\Delta_*\le0$. For $x\in X_k$ the interval $I_l$ has length $2(m_l-z_0)+\sqrt2|z|(|d_{l+}|+|d_{l-}|)\le2H_l$, so $X_k=\emptyset$ if some $H_l<0$. In every case $X_k$ lies in the set of $z$ with $0<-z_0<\Delta_*^+$ and each $z_l$ in an interval of length $2H_l^+$, and integrating over $z_1,z_2,z_3$ and then over $z_0$ gives
\[
\vol(X_k)\le\Delta_*^+\prod_{l=1}^32H_l^+ .
\]
Put $\alpha_j=\sqrt2\,\Delta_j^+$, $\gamma_l=\sqrt2\,\bigl(m_l+\frac{\bar Y}{\sqrt2}(|d_{l+}|+|d_{l-}|)\bigr)^+$, $W_k=\sum_j\max(\alpha_j,\gamma_j)$ and $\alpha_{\min}=\min_j\alpha_j=\sqrt2\,\Delta_*^+\le W_k/3$. If $\Delta_*\le0$, then $X_k=\emptyset$ and the next display holds trivially. If $\Delta_*>0$, then $\sqrt2\,H_l^+\le\gamma_l+\alpha_{\min}$ for each $l$: if $H_l\ge0$ this follows from the definitions, and otherwise the left-hand side is $0$. By the arithmetic--geometric mean inequality,
\[
\vol(X_k)\le2\alpha_{\min}\prod_l(\gamma_l+\alpha_{\min})\le2\alpha_{\min}\Bigl(\frac{W_k}3+\alpha_{\min}\Bigr)^3\le\frac{16}{81}W_k^4 .
\]

\emph{(d) Second-order bookkeeping.} Write $e_j=\eta_{j+}+\eta_{j-}$ and $u_j=u_{j+,j-}$. From $\langle v,d_{j+}+d_{j-}\rangle=\bigl(u_j-\langle d_{j+},d_{j-}\rangle-\frac12(|d_{j+}|^2+|d_{j-}|^2)\bigr)/\sqrt2$, $0\le1-h_b^{-1}\le\eta_b$ and $|\langle v,d_b\rangle|\le\bar\nu|d_b|$ we get
\[
-\bar\theta_j\le\frac{e_j-u_j}{\sqrt2}+\varpi_j,\qquad m_j\le\frac{e_j-u_j}{\sqrt2}+\varpi'_j,
\]
with $\varpi_j=(\bar d/\sqrt2+\bar\nu\bar\eta)(|d_{j+}|+|d_{j-}|)$ and $\varpi'_j=(\bar d/\sqrt2)(|d_{j+}|+|d_{j-}|)$. By Lemma~\ref{lem:gauge}(3), $u_j=(\Lambda_O\tau)_{j+,j-}+\langle d_{j+},d_{j-}\rangle$. Put
\[
R_{kj}=2|\langle d_{j+},d_{j-}\rangle|+\sqrt2\bigl(\varpi_j+\varpi'_j+\sup_{X_k}\mathrm{err}_j\bigr)+\bar Y\bigl(|d_{j+}|+|d_{j-}|\bigr),\qquad R_k=\sum_jR_{kj} .
\]
If $X_k\ne\emptyset$, every $\Delta_j$ is positive, and $\alpha_j$ and $\gamma_j$ are at most $e_j-(\Lambda_O\tau)_{j+,j-}+R_{kj}$, which is therefore positive. Summing over $j$ gives $W_k\le\sum_je_{kj}-\sigma_k(\tau)+R_k$, so
\[
\vol(X_k)\le\tfrac{16}{81}\bar M^2\Bigl(\sum_je_{kj}-\sigma_k(\tau)+R_k\Bigr)^2
\]
for any bound $\bar M\ge W_k$.

\emph{A priori bounds.} Put $d_2=\sqrt2\,\bar d\ge|d_{l+}|+|d_{l-}|$ and
\begin{gather*}
\bar u_O=\min\bigl(\bar u_\perp,\ d_2+\tfrac12\bar d^2\bigr),\quad \hat\theta=\sqrt2\bar\eta+2\bar\nu\bar d,\quad \hat r=\sqrt2\bar\eta+2\bar d,\quad \widehat{\Delta\theta}=\sqrt2\bar\eta+2\bar\nu d_2,\\
\widehat{\mathrm{spr}}=\hat\theta+\sqrt2\bar\eta+\bar\nu d_2,\quad \hat o=\bar\eta/\sqrt2+\bar\nu d_2,\quad \hat\varpi=(\bar d/\sqrt2+\bar\nu\bar\eta)d_2,\quad \hat\varpi'=(\bar d/\sqrt2)d_2,\\
\hat m=(2\bar\eta+\bar u_O)/\sqrt2+\hat\varpi',\qquad \hat K=(2\bar\eta+\bar u_O)/\sqrt2+\hat\varpi .
\end{gather*}
These bound $|u_l|$ on $O$, $|\theta_b|$, $|r_b|$, $|\theta_{j+}-\theta_{j-}|$, $\mathrm{spr}_j$, $|o_l|$, $\varpi_j$, $\varpi'_j$, $m_l$ and $-\bar\theta_j$, respectively. Start with $\hat\Delta=\varepsilon_q$ and $\bar Y=(2\sqrt2\,\varepsilon_q)^{1/2}$, which are valid by (a), and repeat the following step. Put $\tilde Y=\hat o+\hat m+\hat\Delta+\sqrt2\bar Y\bar d$, which bounds $|z_l|$ by (c); replace $\bar Y$ by $\min(\bar Y,\hat\Delta+\sqrt3\tilde Y)$ and recompute $\tilde Y$; check~\eqref{eq:region}; put
\[
\mathrm{err}=\frac{\tilde Y+\hat r}{2\sqrt2}\,\widehat{\Delta\theta}+\frac{2\tilde Y+2\hat r}{\sqrt2}\,\widehat{\mathrm{spr}}\ \ge\ \sup_{X_k}\mathrm{err}_j ,
\]
and replace $\hat\Delta$ by $\min(\hat\Delta,\hat K+\mathrm{err})$. Each step derives valid bounds from valid ones, so the bounds after any number of steps may be used. Then $R_k\le R_{\max}:=3\bigl(\frac12d_2^2+\sqrt2\hat\varpi+\sqrt2\hat\varpi'+\sqrt2\,\mathrm{err}+\bar Yd_2\bigr)$. By (d), $\alpha_j$ and $\gamma_j$ are at most $2\bar\eta+\bar u_O+R_{\max}/3$, so $\bar M=3(2\bar\eta+\bar u_O)+R_{\max}$ bounds $W_k$.

\emph{Summation.} Put $f_1=\frac12(\tilde Y+\hat r)$ and $f_2=2(\tilde Y+\hat r)$. Then $\sqrt2\sup_{X_k}\mathrm{err}_j\le f_1|\theta_{j+}-\theta_{j-}|+f_2\,\mathrm{spr}_j$, and
\begin{gather*}
|\theta_{j+}-\theta_{j-}|\le\sqrt2|\eta_{j+}-\eta_{j-}|+2\bar\nu(|d_{j+}|+|d_{j-}|),\\
\mathrm{spr}_j\le\sqrt2\sum_{b\notin j}\eta_b+2\bar\nu\sum_{b\notin j}|d_b|+\frac{e_j}{\sqrt2}+\bar\nu(|d_{j+}|+|d_{j-}|),
\end{gather*}
where $b\notin j$ runs over the four elements of $N(k)$ outside the pair $j$. With $2|\langle d_{j+},d_{j-}\rangle|\le\frac12d_2(|d_{j+}|+|d_{j-}|)$ this gives
\[
R_{kj}\le C_1(|d_{j+}|+|d_{j-}|)+C_2|\eta_{j+}-\eta_{j-}|+C_3\sum_{b\notin j}\eta_b+C_4\sum_{b\notin j}|d_b|+C_5e_j ,
\]
with $C_1=\frac12d_2+2\bar d+\sqrt2\bar\nu\bar\eta+\bar Y+2\bar\nu f_1+\bar\nu f_2$, $C_2=\sqrt2f_1$, $C_3=\sqrt2f_2$, $C_4=2\bar\nu f_2$ and $C_5=f_2/\sqrt2$. Sum over the $72$ pairs $(k,j)$. Each root lies in six orthogonal pairs and in six sets $N(k)$, so
\begin{gather*}
\sum(|d_{j+}|^2+|d_{j-}|^2)=6\|d\|^2,\qquad \sum\sum_{b\notin j}|d_b|^2=12\|d\|^2,\\
\sum|\eta_{j+}-\eta_{j-}|^2\le6|\eta|^2,\qquad \sum e_j^2\le12|\eta|^2,\qquad \sum\sum_{b\notin j}\eta_b^2=12|\eta|^2 ,
\end{gather*}
and $\|d\|^2\le\chi|\tau|^2$. By $(\sum_jR_{kj})^2\le3\sum_jR_{kj}^2$ and the Cauchy--Schwarz inequality $(\sum_ic_iy_i)^2\le(\sum_ic_i)(\sum_ic_iy_i^2)$ for $c_i\ge0$, with $C_{\rm tot}=2C_1+C_2+4C_3+4C_4+C_5$,
\[
\sum_kR_k^2\le S_t|\tau|^2+S_e|\eta|^2,\qquad S_t=3C_{\rm tot}(6C_1+12C_4)\chi,\qquad S_e=3C_{\rm tot}(6C_2+12C_3+12C_5).
\]
Finally put $w(\eta)=(E+M_\sigma L)\eta$. Since $\sum_je_{kj}=(E\eta)_k$ and $\sigma_k(\tau)=\sigma_k(\tau')-(M_\sigma L\eta)_k$, we have $\sum_je_{kj}-\sigma_k(\tau)=w_k(\eta)-\sigma_k(\tau')$, and $|w(\eta)|\le6|\eta|$ by Lemma~\ref{lem:deriv}(2)(d). For $\kappa_2,\kappa_3>0$ it follows that
\begin{multline*}
\sum_k\vol(X_k)\le\tfrac{16}{81}\bar M^2\Bigl[(1+\kappa_2)\sum_k\sigma_k(\tau')^2\\
+(1+\kappa_2^{-1})\bigl((1+\kappa_3)\,36|\eta|^2+(1+\kappa_3^{-1})(S_t|\tau|^2+S_e|\eta|^2)\bigr)\Bigr],
\end{multline*}
which is Lemma~\ref{lem:deficit} with
\begin{equation}\label{eq:hullconst}
\begin{gathered}
A_\sigma=\tfrac{16}{81}\bar M^2(1+\kappa_2),\qquad A_t^{\rm h}=\tfrac{16}{81}\bar M^2(1+\kappa_2^{-1})(1+\kappa_3^{-1})S_t,\\
A_e^{\rm h}=\tfrac{16}{81}\bar M^2(1+\kappa_2^{-1})\bigl(36(1+\kappa_3)+(1+\kappa_3^{-1})S_e\bigr).
\end{gathered}
\end{equation}

\subsection{The third-order remainder}\label{app:remainder}

We prove Lemma~\ref{lem:remainder}. By the symmetry of $D_4$, which acts transitively on roots, contact pairs and contact triangles, and the symmetry of $\Pi$ in $h_1,h_2$ and of $\Theta$ under permutations of its three vectors, the derivatives of $\Phi$ at $\zeta_0$ are $g_h=-S'+8\Pi_{h_1}-12\Theta_{h_1}$ and $g_u=\Pi_u-3\Theta_{u_{12}}$, and
\begin{align*}
(\Phi_{hh})_{kl}&=\begin{cases}-S''+8\Pi_{h_1h_1}-12\Theta_{h_1h_1}&\text{if }k=l,\\ \Pi_{h_1h_2}-3\Theta_{h_1h_2}&\text{if }\{k,l\}\in T,\\ 0&\text{otherwise},\end{cases}\\
(\Phi_{hu})_{k,ij}&=\begin{cases}\Pi_{h_1u}-3\Theta_{h_1u_{12}}&\text{if }k\in\{i,j\},\\ -\Theta_{h_3u_{12}}&\text{if }\{i,j,k\}\text{ is a contact triangle},\\ 0&\text{otherwise},\end{cases}\\
(\Phi_{uu})_{ef}&=\begin{cases}\Pi_{uu}-3\Theta_{u_{12}u_{12}}&\text{if }e=f,\\ -\Theta_{u_{12}u_{13}}&\text{if }e\ne f\text{ lie in a common contact triangle},\\ 0&\text{otherwise},\end{cases}
\end{align*}
with all partial derivatives of $S,\Pi,\Theta$ taken at $h=1$, $u=\frac12$. These partial derivatives, of order at most two, are enclosed in ball arithmetic with radius at most $6\cdot10^{-37}$, and the resulting values lie within $10^{-22}$ of $\frac43,\frac14,-4,1,-1,\frac13,1,-\frac16$, which is Lemma~\ref{lem:deriv}(1). Hence $D^2\Phi(\zeta_0)-D^2\Phi^0$ is a symmetric matrix with at most $29$ nonzero entries in each row ($9+20$ in a row of a height, $5+7$ in a row of an inner product), all at most $10^{-22}$ in absolute value, and its norm is at most $2.9\cdot10^{-21}$. Since
\[
\widetilde\Hs(\xi,\xi)-\Hs(\xi,\xi)=\bigl(2g_u-\tfrac12\bigr)Q_t(\tau)+\bigl(D^2\Phi(\zeta_0)-D^2\Phi^0\bigr)\bigl[(\eta,\Lambda\tau)\bigr]^2 ,
\]
$|Q_t(\tau)|\le6|\tau|^2$ (each root lies in eight contact pairs) and $\|\Lambda\|=2$, we obtain $|\widetilde\Hs(\xi,\xi)-\Hs(\xi,\xi)|\le1.2\cdot10^{-21}|\tau|^2+2.9\cdot10^{-21}(|\eta|^2+4|\tau|^2)\le1.3\cdot10^{-20}|\xi|^2$, which is the first claim of Lemma~\ref{lem:deriv}(2). Consequently $g_h\ge\frac43-\varepsilon_0$ and $0<g_u\le\frac14+\varepsilon_0$. The matrix $\Phi_{hu}-\Phi_{hu}^0$ has at most $20$ nonzero entries in each row and $5$ in each column, all at most $\varepsilon_0$, so $\|\Phi_{hu}\|\le4+10\varepsilon_0$. The matrix $\Phi_{uu}-\Phi_{uu}^0$ has at most $7$ nonzero entries in each row, so $\|\Phi_{uu}\|\le\frac32+7\varepsilon_0$ and $\Phi_{uu}\succeq-7\varepsilon_0I$. Finally $\|\widetilde\Hs-\Hs\|\le1.3\cdot10^{-20}\le96\,\varepsilon_0$.

Each local term $f\in\{S(h_i),\Pi(h_i,h_j;u_{ij}),\Theta(\dots)\}$ is real-analytic on the box: its closed form is valid there, the vertex of the corresponding cone lying inside the ball~\cite{supp}. The box is convex and contains $\zeta_0$ and, by Lemma~\ref{lem:gauge}(5),(6), the actual arguments. So $f(\zeta_0+\Delta)=f(\zeta_0)+Df[\Delta]+\frac12D^2f[\Delta]^2+\frac16D^3f(\zeta^*)[\Delta]^3$ for some $\zeta^*$ on the segment. Summing over the local terms and substituting $\Delta h=\eta$, $\Delta u=\Lambda\tau+c$ and $\sum_T\Delta u_{ij}=Q_d$ (Lemma~\ref{lem:gauge}(3)) gives
\[
\Phi=8+g_hs+\tfrac12\widetilde\Hs(\xi,\xi)+g_u\bigl(Q_d-Q_t(\tau)\bigr)+D^2\Phi(\zeta_0)\bigl[(\eta,\Lambda\tau),(0,c)\bigr]+\tfrac12c^{\top}\Phi_{uu}c+R_\Phi ,
\]
where $R_\Phi$ is the sum of the cubic terms. We bound the terms in turn. First, $g_hs\ge(\frac43-\varepsilon_0)s$ and $\frac12\widetilde\Hs(\xi,\xi)\ge\frac12\Hs(\xi,\xi)-48\varepsilon_0(|\tau|^2+|\eta|^2)$. By Lemma~\ref{lem:gauge}(4), $g_u(Q_d-Q_t)\ge-(\frac14+\varepsilon_0)(2\sqrt3\chi\bar d+\chi^2\bar d^2)|\tau|^2$. The next term is $\eta^{\top}\Phi_{hu}c+(\Lambda\tau)^{\top}\Phi_{uu}c$, and $|c|\le3\bar d\|d\|\le c_*|\tau|$ with $c_*=3\bar d\chi^{1/2}$. So for any $\kappa_1>0$ it is at least
\[
-(4+10\varepsilon_0)c_*|\eta||\tau|-2(\tfrac32+7\varepsilon_0)c_*|\tau|^2\ \ge\ -c_*\Bigl((2+5\varepsilon_0)\bigl(\kappa_1^{-1}|\eta|^2+\kappa_1|\tau|^2\bigr)+(3+14\varepsilon_0)|\tau|^2\Bigr).
\]
Further, $\frac12c^{\top}\Phi_{uu}c\ge-\frac72\varepsilon_0c_*^2|\tau|^2$.

For the cubic terms let $M_{abc}$ be an upper bound for $|\partial_a\partial_b\partial_cf|$ on the box, for each local term $f$ and each multi-index of order three. These bounds come from closed forms of lower derivatives. For the pair term,
\begin{gather*}
\frac{\partial\Pi}{\partial h_1}=-\frac\pi3\Bigl(2(2-h_1^2)^{3/2}-3(2-h_1^2)\frac{h_2-uh_1}{(1-u^2)^{1/2}}+\frac{(h_2-uh_1)^3}{(1-u^2)^{3/2}}\Bigr),\\
\frac{\partial\Pi}{\partial u}=\frac{\pi}{4(1-u^2)^{1/2}}\Bigl(2-\frac{h_1^2+h_2^2-2uh_1h_2}{1-u^2}\Bigr)^2,
\end{gather*}
and symmetrically in $h_2$. For the triple term,
\begin{gather*}
\frac{\partial\Theta}{\partial u_{ab}}=\frac1{2(1-u_{ab}^2)^{1/2}}\int_{F_{ab}}(2-|x|^2)\,dA,\\
\frac{\partial^2\Theta}{\partial h_a\partial h_b}=\frac{|F_{ab}|}{(1-u_{ab}^2)^{1/2}}\ \ (a\ne b),\qquad \frac{\partial^2\Theta}{\partial h_a^2}=\frac{h_a|\mathcal S_a|}{(2-h_a^2)^{1/2}}-\sum_{b\ne a}\frac{u_{ab}|F_{ab}|}{(1-u_{ab}^2)^{1/2}},
\end{gather*}
where $F_{ab}$ is the two-dimensional face of the region $\{|x|<\sqrt2,\ \langle x,w_c\rangle>h_c\ \forall c\}$ in the plane $\langle x,w_a\rangle=h_a$, $\langle x,w_b\rangle=h_b$ (a circular segment), and $\mathcal S_a$ is the part of the sphere $|x|=\sqrt2$ on the boundary of its face in the hyperplane $\langle x,w_a\rangle=h_a$ (the intersection of two spherical caps). These have closed forms in square roots and inverse cosines, valid on the boxes~\cite{supp}. A third partial derivative with an index $u$ is a second derivative of one of the forms for $\partial\Pi/\partial u$ or $\partial\Theta/\partial u_{ab}$, and the others are derivatives of the remaining forms. On each box these forms are expanded as Taylor models in ball arithmetic~\cite{Arb} on a cover of the box by cells. The required derivatives of the Taylor models are bounded on each cell, and the maxima over the cells, rounded up with a small safety factor, are the $M_{abc}$ (Table~\ref{tab:verif}). Then $\frac16|D^3f(\zeta^*)[\Delta]^3|\le\frac16\sum_{a,b,c}M_{abc}|\Delta_a||\Delta_b||\Delta_c|$, the sum over ordered triples of local variables. We use $|\Delta h_a|\le\bar\eta$ and $|\Delta u_b|\le\Delta_u:=\max(\bar u,\bar\eta)$, and group the triples by the number of Gram variables. With the symmetric nonnegative matrices $\mathcal M_{xy}[a,b]=\sum_{c\in y}M_{abc}$ for $a,b$ of type $x$ ($x,y\in\{h,u\}$), and $\|\mathcal M\|_\infty$ the largest row sum of $\mathcal M$,
\begin{multline*}
\tfrac16|D^3f(\zeta^*)[\Delta]^3|\le\tfrac16\Bigl[\bigl(\Delta_u\|\mathcal M_{uu}\|_\infty+3\bar\eta\|\mathcal M_{uh}\|_\infty\bigr)|\Delta u_{\rm loc}|^2\\
+\bigl(3\Delta_u\|\mathcal M_{hu}\|_\infty+\bar\eta\|\mathcal M_{hh}\|_\infty\bigr)|\Delta h_{\rm loc}|^2\Bigr],
\end{multline*}
where $\Delta u_{\rm loc}$ and $\Delta h_{\rm loc}$ are the local variables of $f$. Each $\Delta u_{ij}^2$ occurs in one $\Pi$ term and three $\Theta$ terms, and each $\eta_i^2$ in one $S$ term, eight $\Pi$ terms and twelve $\Theta$ terms. On $[1,1+\bar\eta]$ we have $|S'''(h)|=8\pi(h^2-1)(2-h^2)^{-1/2}\le M_S:=8\pi\bar\eta(2+\bar\eta)(2-(1+\bar\eta)^2)^{-1/2}$. Hence $|R_\Phi|\le R_u|\Delta u|^2+R_h|\eta|^2$, where
\begin{gather*}
R_u=\tfrac16\bigl[\Delta_u\lambda_{uu}(\Pi)+3\bar\eta\lambda_{uh}(\Pi)+3\bigl(\Delta_u\lambda_{uu}(\Theta)+3\bar\eta\lambda_{uh}(\Theta)\bigr)\bigr],\\
R_h=\tfrac16\bigl[M_S\bar\eta+8\bigl(3\Delta_u\lambda_{hu}(\Pi)+\bar\eta\lambda_{hh}(\Pi)\bigr)+12\bigl(3\Delta_u\lambda_{hu}(\Theta)+\bar\eta\lambda_{hh}(\Theta)\bigr)\bigr],
\end{gather*}
where $\lambda_{xy}(f)=\|\mathcal M_{xy}\|_\infty$ for the local term $f$, and $|\Delta u|\le|\Lambda\tau|+|c|\le(2+c_*)|\tau|$. For $\sigma=\frac1{125}$ (box $\mathbf B_1$) this gives $R_u\le0.049195$ and $R_h\le0.819561$, and for the row $(\rho,\sigma)=(\tfrac25,\tfrac3{100})$ of Table~\ref{tab:pairs} (box $\mathbf B_2$) it gives $R_u\le0.207857$ and $R_h\le3.389261$. Collecting the terms proves Lemma~\ref{lem:remainder} with
\begin{gather*}
A_t^{(3)}=\bigl(\tfrac14+\varepsilon_0\bigr)\bigl(2\sqrt3\chi\bar d+\chi^2\bar d^2\bigr)+c_*\bigl((2+5\varepsilon_0)\kappa_1+3+14\varepsilon_0\bigr)+\tfrac72\varepsilon_0c_*^2+R_u(2+c_*)^2+48\varepsilon_0,\\
A_e^{(3)}=c_*(2+5\varepsilon_0)/\kappa_1+R_h+48\varepsilon_0 .
\end{gather*}

\section*{Data availability}
The certificate and its checker, the interval-arithmetic proofs of Lemma~\ref{lem:approx}, the construction scripts, the exact computation behind Remark~\ref{rem:poly}, the programs and logs behind Section~\ref{sec:local} and the Lean projects of Section~\ref{sec:lean} are in~\cite{supp}.

\section*{Use of AI tools}
Generative AI tools were used extensively to write and run code, to carry out and check computations, and to draft text. The author checked the results and the text, and takes responsibility for the content.

\begin{thebibliography}{99}
\bibitem{Arb} F.~Johansson, \emph{Arb: efficient arbitrary-precision midpoint-radius interval arithmetic}, IEEE Trans. Comput. \textbf{66} (2017), 1281--1292.
\bibitem{BBMB} D.~Bhattacharjee, U.~Bhattacharya, P.~Mandal and S.~Bhattacharya, \emph{The sphere packing problem in dimension 4 and the twenty-four-cell conjecture}, arXiv:2609.25120v2 (2026).
\bibitem{BBMBd} D.~Bhattacharjee, U.~Bhattacharya, P.~Mandal and S.~Bhattacharya, \emph{The sphere packing problem in dimension 4 and the twenty-four-cell conjecture}, unrefereed draft, file \texttt{paper/D4.tex} at commit \texttt{c85496134f} (21 October 2026) of \url{https://github.com/creelie/d4-voronoi-cells}.
\bibitem{CY} K.~C.~Chung and T.~H.~Yao, \emph{On lattices admitting unique Lagrange interpolations}, SIAM J. Numer. Anal. \textbf{14} (1977), 735--743.
\bibitem{CdLS} H.~Cohn, D.~de~Laat and A.~Salmon, \emph{Three-point bounds for sphere packing}, arXiv:2206.15373 (2022).
\bibitem{CJKT} H.~Cohn, Y.~Jiao, A.~Kumar and S.~Torquato, \emph{Rigidity of spherical codes}, Geom. Topol. \textbf{15} (2011), 2235--2273.
\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{FT} L.~Fejes T\'oth, \emph{Lagerungen in der Ebene, auf der Kugel und im Raum}, Springer, Berlin, 1953.
\bibitem{HM} T.~C.~Hales and S.~McLaughlin, \emph{The dodecahedral conjecture}, J. Amer. Math. Soc. \textbf{23} (2010), 299--344.
\bibitem{KZ} A.~Korkine and G.~Zolotareff, \emph{Sur les formes quadratiques positives quaternaires}, Math. Ann. \textbf{5} (1872), 581--583.
\bibitem{LLdMK} D.~de~Laat, N.~M.~Leijenhorst and W.~H.~H.~de~Muinck Keizer, \emph{Optimality and uniqueness of the $D_4$ root system}, arXiv:2404.18794 (2024).
\bibitem{LdL} N.~M.~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{Mus} O.~R.~Musin, \emph{The kissing number in four dimensions}, Ann. of Math. \textbf{168} (2008), 1--32.
\bibitem{Mus18} O.~R.~Musin, \emph{Towards a proof of the 24-cell conjecture}, Acta Math. Hungar. \textbf{155} (2018), 184--199.
\bibitem{Nic} R.~A.~Nicolaides, \emph{On a class of finite elements generated by Lagrange interpolation}, SIAM J. Numer. Anal. \textbf{9} (1972), 435--445.
\bibitem{supp} T.~S.~Tomar, \emph{Supplementary files for ``The 24-cell conjecture in the all-contact case and near $D_4$''}, Zenodo (2026), \href{https://doi.org/\suppdoi}{doi:\suppdoi}.
\end{thebibliography}

\end{document}