\section{Introduction}\label{sec:introduction}
The points of the octonionic projective plane $\mathbb OP^2$ are the
trace-one idempotents of the Albert algebra $J=H_3(\mathbb O)$. Two points
have an \emph{overlap} $\langle p,q\rangle=\operatorname{tr}(p\circ q)$,
the inner product of
Cohn, Kumar and Minton\cite{CKM16}, or $1-\rho^2$ for the chordal distance $\rho$ of $p$ and $q$. A
\emph{code} is a finite set of points. By a linear programming
bound, Lemma~2.7 of Cohn, Kumar and Minton, a code in which distinct points have overlap at most $1/3$ has at
most $39$ points; a code attaining this
number is a \emph{tight $39$-point code}. These authors record that Hoggar\cite{Hoggar84} conjectured that such a code
exists, and in their Theorem~8.3 they constructed one\cite{CKM16}:
thirteen triples of mutually orthogonal points, with overlap $1/3$ between
points of different triples. They show that it is tight
and universally optimal\cite{CK07}, that is, it minimizes potential energy
for every completely monotonic function of squared chordal distance.

Four unit complex numbers can be inserted into its defining formula\cite{CKM16}, giving
a four-parameter family of tight codes that remains four-dimensional modulo
the isometry group $F_4$ of $\mathbb OP^2$. Write $P(\xi)$ for the member with
parameters $\xi\in(S^1)^4$; the code they constructed is $P(1)$, the
\emph{original code}.

This paper describes the local geometry of the space of tight $39$-point
codes around this family. Outside a closed nowhere-dense set of
\emph{resonant} parameters, the tight codes near $P(\xi)$, with their points
labeled, are, modulo $F_4$, exactly the members of four ten-dimensional
families, any two of which meet exactly in the four-parameter family
(Theorem~\ref{thm:real}). The original
code is resonant, and our methods do not determine the codes near it. But
nonresonant members accumulate at it, and it follows that any neighborhood of
it in the space of unlabeled tight $39$-point codes modulo $F_4$ that is a manifold has
dimension ten (Theorem~\ref{thm:patches}, Corollary~\ref{cor:no24}).

\subsection{Setting}
The Albert algebra $J$ is the exceptional Euclidean, or formally real,
Jordan algebra. It has dimension $27$ and a unit $e$ of trace three. Its
product is $x\circ y=(xy+yx)/2$, and its trace form is
$\langle x,y\rangle=\operatorname{tr}(x\circ y)$. The automorphism group
of $J$ is $F_4$; it has dimension $52$ and preserves the trace form. Points are the primitive idempotents\cite{Baez02}. A
\emph{Jordan frame} is a triple of points with sum $e$ and
pairwise zero Jordan products. Two frames are \emph{mutually unbiased}, as
for bases of $\mathbb C^d$, when all nine overlaps between
their points equal $1/3$.

The spaces studied are
\begin{equation}\label{eq:moduli}
\begin{gathered}
\mathcal C=\{(p_k)\in J^{39}:p_k\text{ a point},\
 \langle p_k,p_m\rangle\le1/3\ (k\ne m)\},\\
Y=\mathcal C/F_4,\qquad
\mathcal M=Y/\mathfrak S_{39},
\end{gathered}
\end{equation}
where the symmetric group $\mathfrak S_{39}$ permutes the labels and the
quotients carry their quotient topologies. The \emph{unlabeled space} $\mathcal M$ is the
space of tight $39$-point codes modulo $F_4$ in the sense of Cohn, Kumar and Minton.

Every element of
$\mathcal C$ is a union of thirteen pairwise mutually unbiased Jordan frames
in exactly one way, and the partition into frames is locally constant on
$\mathcal C$ (Proposition~\ref{prop:frames}, Lemma~\ref{lem:partition}). Near a
given code, $\mathcal C$ is therefore the real zero set $\mathcal Z$ of
one polynomial map $F$ of degree two on $J^{39}$, the residual of the
\emph{frame equations} \eqref{eq:frame-equations}.

The family rests on four subalgebras of $J$
(Lemma~\ref{lem:subalgebras}). Let \emph{frame~$0$} be the frame of diagonal
matrix units and $D$ its span. There are subalgebras $A_0,\ldots,A_3$, each
a copy of $H_3(\mathbb C)$ containing $D$, that are otherwise orthogonal to
one another:
\[
 J=D\oplus N_0\oplus N_1\oplus N_2\oplus N_3,\qquad A_i=D\oplus N_i.
\]
A point that has overlap $1/3$ with the points of frame~$0$ has component
$e/3$ in $D$, so two such points in different subalgebras have overlap $1/3$. The code $P(\xi)$, written out in \eqref{eq:literal}, is
frame~$0$ with three further frames in each subalgebra. These form with
frame~$0$ a \emph{complex quartet}: a complete set of four mutually unbiased
bases of $\mathbb C^3$ (Figure~\ref{fig:flower}). The parameters enter
through diagonal conjugations within the subalgebras.

\begin{conceptfigure}
\centering
\includegraphics{figures/fig1-frames.pdf}
\captionof{figure}{Each disc is a Jordan frame. Frames $3i+1$, $3i+2$,
$3i+3$ make up \emph{lobe}~$i$; with frame~$0$ they form complex
quartet~$i$, which spans $A_i$.}\label{fig:flower}
\end{conceptfigure}

A parameter $\xi$ is \emph{nonresonant} if the linearized frame equations at
$P(\xi)$ have a solution space of dimension $80$, the least that occurs on
the family. By Proposition~\ref{prop:kernel} the resonant parameters are
those at which one of twelve nonconstant monomials $\pm\xi_1^{a_1}\xi_2^{a_2}\xi_3^{a_3}\xi_4^{a_4}$,
listed in Section~\ref{sec:families}, has cube one. The set
$\mathcal N\subset(S^1)^4$ of nonresonant parameters is therefore open and
dense.

\subsection{Results}
The local model is the \emph{germ} at the origin of
\begin{equation}\label{eq:axes}
 \mathbb R^4\times\bigcup_{i=0}^3 W_i\ \subset\ \mathbb R^4\times\mathbb R^{24},
 \qquad W_i=\mathbb R^6_i\subset\bigoplus_{j=0}^3\mathbb R^6_j=\mathbb R^{24},
\end{equation}
four copies of $\mathbb R^{10}$ that meet pairwise in $\mathbb R^4\times\{0\}$
and whose \emph{transverse spaces} $W_i$ are linearly independent.

\begin{theorem}[Local solutions at nonresonant parameters]\label{thm:real}
Let $\mathcal Z$ be the real zero set of the frame equations. At every
$\xi\in\mathcal N$, the germ \leannote{real germ}{Proofs/PairingR.lean}{57}of $\mathcal Z$ at $P(\xi)$ in a local slice transverse to the $F_4$-orbit is homeomorphic to the germ of \eqref{eq:axes}
at the origin. Its four branches are the families $M_0,\ldots,M_3$
constructed in Sections~\ref{sec:families} and~\ref{sec:linear}, one for each
complex quartet. Their common part is the slice image of the four-parameter
family $\xi^{\prime}\mapsto P(\xi^{\prime})$ near $\xi$.
\end{theorem}

The proof gives more: near $P(\xi)$ the slice has analytic coordinates in which its
intersection with $\mathcal Z$ is, near the origin, the product of \eqref{eq:axes} with the
origin of $\mathbb R^{973}$ (Propositions~\ref{prop:simultaneous} and~\ref{prop:exhaustion}).
The registered statement of Theorem~\ref{thm:real} gives such a chart as a homeomorphism only;
the analytic chart of Proposition~\ref{prop:simultaneous}, in which the families are coordinate
subspaces, is registered separately.

In the family $M_i$ the twelve points of quartet~$i$ stay fixed, up to an
$F_4$ motion, while the other nine frames move. So every labeled tight code
near $P(\xi)$ contains, up to $F_4$, one of the four complex quartets of
$P(\xi)$.

The slice identifies its zero set with a neighborhood of $[P(\xi)]$ in $Y$
(Section~\ref{sec:quotient}), so the theorem describes all labeled tight
codes modulo $F_4$ near $P(\xi)$. The orbit $F_4P(\xi)$ has dimension $52$, so the
\emph{first-order deformations} (solutions of the linearized equations;
infinitesimal flexes in rigidity theory) form modulo $F_4$ a space of
dimension $80-52=28=4+4\cdot6$, the sum of the tangent spaces of the four
families. The quadratic part of the equations obstructs all of them except
those tangent to a single family (Figure~\ref{fig:book}).

\begin{conceptfigure}
\centering
\includegraphics{figures/fig2-families.pdf}
\captionof{figure}{The local model \eqref{eq:axes}: four ten-dimensional
families meet along the four-parameter family, with independent transverse
spaces.}
\label{fig:book}
\end{conceptfigure}

In the next theorem the norms on $J^{39}$ and on the residuals are any fixed
norms; they affect only the constants.

\begin{theorem}[Distance bound]\label{thm:bound}
Let $\xi\in\mathcal N$.
\begin{enumerate}
\item[\textup{(a)}] There are an open neighborhood $U_\xi$ of the orbit
$F_4P(\xi)$ in $J^{39}$ and a constant $C_\xi>0$ such that
\begin{equation}\label{eq:main-bound}
\begin{gathered}
 \mathcal Z\cap U_\xi=F_4(M_0\cup\cdots\cup M_3)\cap U_\xi,\\
 \operatorname{dist}(y,\mathcal Z)^2\le C_\xi\|F(y)\|\qquad(y\in U_\xi).
\end{gathered}
\end{equation}
\item[\textup{(b)}] The exponent cannot be improved: for no $\alpha>1/2$
does a bound $\operatorname{dist}(y,\mathcal Z)\le C\|F(y)\|^\alpha$ hold on
a neighborhood of $P(\xi)$ in $J^{39}$.
\end{enumerate}
\end{theorem}

Part~(b) holds because the linearization at
$P(\xi)$ of any $C^2$ equations with zero set $\mathcal Z$ near $P(\xi)$ has
solutions outside the \emph{tangent cone} of $\mathcal Z$, the cone of
limits of secant directions, and this excludes every
exponent above $1/2$ (Lemma~\ref{lem:cone-sharp}). Even on configurations whose thirteen triples are Jordan frames, no exponent above $1/2$ is
possible (Section~\ref{sec:quantitative}; proved in the text, not formalized).

Write $c_0=[P(1)]$ for the class of the original code in $\mathcal M$.

\begin{theorem}[Open patches near the original code]\label{thm:patches}
Every \leannote{open ten-patches}{Proofs/NativeOriginalCodeNoManifold24.lean}{30}open neighborhood $\Omega$ of $c_0$ in $\mathcal M$ contains a nonempty open
subset $V$ of $\mathcal M$ homeomorphic to a nonempty open subset of
$\mathbb R^{10}$.
\end{theorem}

The patch $V$ need not contain $c_0$. A ten-dimensional family can lie inside a manifold of larger
dimension (Figure~\ref{fig:patch}(a)); a nonempty open set homeomorphic to
an open subset of $\mathbb R^{10}$ cannot, by invariance of dimension.

\begin{corollary}[Manifold neighborhoods]\label{cor:no24}
If a neighborhood of $c_0$ in $\mathcal M$ is homeomorphic to an open subset
of $\mathbb R^n$, then $n=10$. In particular the original code has no
twenty-four-dimensional manifold neighborhood in $\mathcal M$.
\end{corollary}

The last assertion is contrary to the neighborhood statement of Conjecture~8.4
of Cohn, Kumar and Minton\cite{CKM16}.

\begin{conceptfigure}
\centering
\includegraphics{figures/fig5-patch.pdf}
\captionof{figure}{(a) A family inside a manifold of larger dimension is
not open in it. (b) Every neighborhood $\Omega$ of $c_0$ in $\mathcal M$
contains a ten-dimensional patch open in $\mathcal M$ (heavy segments). Dots
mark nonresonant members. The stippled shape at the original code is not
determined. Schematic.}\label{fig:patch}
\end{conceptfigure}

\subsection{What is open}
By \eqref{eq:fullkernel} the linearized equations at the original code have a solution space
of dimension $92$, that is $40$ modulo $F_4$. The four families can account
for at most $28$ of these dimensions, whereas the argument of
Section~\ref{sec:exhaustion} starts from coordinates in which they account
for every first-order deformation. Along
$\xi(t)=(e^{it},e^{-it},1,e^{-it})$, with $t\in\mathbb R/2\pi\mathbb Z$, the dimension is also $92$, except at the three
values of $t$ with $e^{3it}=-1$, where it is $104$. So the resonance at the original
code is not isolated in the family. The following questions are open. 
\begin{enumerate}
\item[(a)] The germ of $\mathcal M$ at $c_0$, and at the other resonant
members of the family. In particular the local dimension at $c_0$ is not
determined: solution sets of dimension greater than ten passing through
resonant members, away from the nonresonant ones, are not excluded.
\item[(b)] The finite group in the germ of $\mathcal M$ at a nonresonant member. That germ is
the model \eqref{eq:axes} modulo an action of the group $\operatorname{Aut}(P(\xi))$ of
automorphisms of $J$ that permute the code (Remark~\ref{rem:aut}); we determine neither the
group nor its action.
\item[(c)] Whether the constants $C_\xi$ stay bounded as $\xi$ approaches a
resonant parameter (Section~\ref{sec:quantitative}).
\item[(d)] Tight $39$-point codes away from the family. We make no claim that
every tight $39$-point code lies in one of the families described here.
\end{enumerate}

\subsection{Method and verification}


Theorem~\ref{thm:real}, Theorem~\ref{thm:bound} in an equivalent
form, and Corollary~\ref{cor:no24} for $n=24$ are formalized in Lean~4 and
registered (Section~\ref{sec:verification}); gray notes in the margin link
to the formal statements. The printed proof relies on two machine computations, both part of
the formal development. The properties of the stresses
\textup{(}linear functionals on the residuals that annihilate the linearized
equations\textup{)} of Proposition~\ref{prop:finite} are finite polynomial identities over
$\mathbb Q(i,\sqrt3)$ with Laurent dependence on the parameters (Appendix~\ref{app:quadrics}),
checked exactly. The quartic identity \eqref{eq:quartic} is checked by direct expansion.
Section~\ref{sec:verification} says which further checks were made outside the formal
development. Section~\ref{sec:outline} outlines the proof.

\subsection{Related work}
For spherical codes, Cohn, Jiao, Kumar and Torquato remark that there seems
to be no simple method to turn an infinitesimal unjamming into an actual one\cite{CJKT11}; here, at a nonresonant parameter, the first-order deformations modulo $F_4$ form a space of dimension $28$, but each family through $P(\xi)$ has dimension ten. For
complex Hadamard matrices the first-order count is the defect of Tadej and \.Zyczkowski, which by their
Theorem~4.7 is an upper bound for the dimension of a smooth family\cite{TZ08}. Barros
e S\'a and Bengtsson found perturbative evidence for two $13$-dimensional
families of Hadamard matrices of order $12$ crossing along a nine-dimensional
one, with defect $17=13+13-9$, on pp.~4 and 24--26 of their paper\cite{BSB13}. Theorem~\ref{thm:real}
describes a crossing of the same kind and proves that nothing else passes
through the point.

In rigidity theory, Connelly's second-order rigidity asks
for an equilibrium stress for each nontrivial first-order flex, and the
prestress stability of Connelly and Whiteley (their Proposition~3.4.2 and
Theorem~4.4.1) for one stress serving them all\cite{CW96}.
Lemma~\ref{lem:stress} asks for one stress field for each limiting direction
along a family, in a situation those results do not cover: several exact
families that cross.

For analytic equations some bound $\operatorname{dist}\le C\|F\|^\alpha$ is
automatic by \L{}ojasiewicz's inequality\cite{Lojasiewicz59}. The theory of $2$-regular maps\cite{AAA91} gives the
exponent $1/2$ under a surjectivity condition in every critical direction
(Theorem~4 of Izmailov and Solodov)\cite{IS01}, which makes the solution set a
manifold away from the base point and so cannot hold where the zero set is
locally \eqref{eq:axes}.