\section{Recovering frames from tight codes}\label{sec:codes}
A reader who takes the frame equations \eqref{eq:frame-equations} as
given can go on to Section~\ref{sec:families}.

The trace form on $J$ is positive definite and associative:
\[
 \langle x\circ y,z\rangle=\langle x,y\circ z\rangle.
\]
In this section $\|x\|^2=\langle x,x\rangle$.
The trace-zero subspace $J_0$ has dimension $26$. For a point $p$,
idempotency gives $\|p\|^2=1$ and $\langle p,e\rangle=1$.

The linear programming bound used here is the one formulated by Cohn, Kumar
and Minton\cite{CKM16} in their Section~2.3 (Proposition~2.5 and Lemma~2.7). In the
overlap variable $t=\langle p,q\rangle$ its degree-two certificate (the
auxiliary polynomial) is
\[
 t\,(t-1/3).
\]
For the equality
case, Lemma~2.7 of Cohn, Kumar and Minton applied to the certificate shows that a tight
$39$-point code has all overlaps in $\{0,1/3\}$ and is a projective
$2$-design\cite{CKM16}. Such a code carries a two-class association scheme\cite{Hoggar83}, so its graph of orthogonal pairs is strongly
regular. Cohn, Kumar and Minton report that
Hoggar\cite{Hoggar84} classified the admissible parameters of such graphs.

We give a direct proof from the Gram matrix, of the kind that gives the
Welch bound.

\begin{lemma}\label{lem:positive}
If \leannote{positive overlap}{Proofs/TCBasic.lean}{87}$p,q$ are idempotents, then $\langle p,q\rangle\ge0$.
\end{lemma}

\begin{proof}
Write $L_p x=p\circ x$. Associativity of the trace form makes $L_p$
self-adjoint. The polarized Jordan identity, specialized to $p\circ p=p$,
gives
\[
 2L_p^3-3L_p^2+L_p=0.
\]
Hence $L_p$ is positive semidefinite, with eigenvalues in
$\{0,1/2,1\}$, the Peirce eigenvalues.
Since $q\circ q=q$,
\[
 \langle p,q\rangle=\langle p,q\circ q\rangle=\langle L_pq,q\rangle\ge0.
 \qedhere
\]
\end{proof}

\begin{proposition}[The 39-point bound and frame decomposition]\label{prop:frames}
Let $p_1,\ldots,p_N$ be points such that
$\langle p_i,p_j\rangle\le1/3$ for $i\ne j$. Then $N\le39$.
If \leannote{frame equality}{Proofs/TCConsumer.lean}{75}$N=39$, the points are in exactly one way the union of thirteen pairwise
mutually unbiased Jordan frames. Conversely, the points of thirteen pairwise
mutually unbiased Jordan frames satisfy the hypothesis with $N=39$.
\end{proposition}

\begin{proof}
\emph{The bound.}
Center the points, $p_i^\circ=p_i-e/3$, and let
\[
 G^\circ=\bigl(\langle p_i^\circ,p_j^\circ\rangle\bigr)_{i,j=1}^N
\]
be their Gram matrix. The $p_i^\circ$ lie in $J_0$, so $G^\circ$ is positive
semidefinite of rank at most $26$. Its diagonal entries are $2/3$, and
Lemma~\ref{lem:positive} puts its off-diagonal entries in $[-1/3,0]$. Let
$s$ be the sum of all its entries:
\[
 s=\mathbf1^{\mathsf T}G^\circ\mathbf1=\Bigl\|\sum_i p_i^\circ\Bigr\|^2\ge0.
\]
Cauchy--Schwarz for the at most $26$ nonzero eigenvalues of $G^\circ$
gives
\[
 (\operatorname{tr}G^\circ)^2\le26\operatorname{tr}\bigl((G^\circ)^2\bigr).
\]
Here $\operatorname{tr}G^\circ=2N/3$. The square of each off-diagonal entry is at most $-1/3$ times the entry, and
\begin{align}\label{eq:gram-bound}
 (2N/3)^2
 &\le26\sum_{i,j}(G^\circ_{ij})^2\\
 &\le26\left(\frac{4N}{9}-\frac13\sum_{i\ne j}G^\circ_{ij}\right)
 =26\left(\frac{2N}{3}-\frac s3\right)
 \le\frac{52N}{3}.\nonumber
\end{align}
This yields $N\le\tfrac32\cdot26=39$.

\emph{Equality.}
At $N=39$ all inequalities are equalities. Each off-diagonal entry of
$G^\circ$ is $0$ or $-1/3$, and $s=0$. Consequently
\begin{equation}\label{eq:equality-data}
 \langle p_i,p_j\rangle\in\{0,1/3\}\ (i\ne j),\qquad
 \sum_i p_i=13e.
\end{equation}
The Gram matrix $G=(\langle p_i,p_j\rangle)$ therefore has row sums $13$:
besides the diagonal entry $1$, each row has thirty-six entries $1/3$ and two
zeros.

\emph{Thirteen triangles.}
Join two distinct labels when their overlap is zero. This simple graph is
$2$-regular. Let $\Delta$ be its graph Laplacian. Comparing entries gives
\[
 3G=\Delta+\mathbf1\mathbf1^{\mathsf T}.
\]
If the graph has $k$ components, the kernel of $\Delta$ consists of the
vectors constant on each component. Both matrices on the right are positive
semidefinite, so the kernel of their sum is the intersection of their
kernels, of dimension $k-1$. Thus
\[
 \operatorname{rank}G=40-k.
\]
The $p_i$ lie in $J$, of dimension $27$, so $\operatorname{rank}G\le27$ and
$k\ge13$. Each component has at least three vertices; hence $k\le13$. All
thirteen components are triangles.

\emph{Frames.}
For the points $p,q,r$ of one triangle, expansion gives
\[
 \|p+q+r-e\|^2=3+3-6=0,
\]
so $p+q+r=e$. Then $e-p-q$ is the idempotent $r$; expanding
$(e-p-q)\circ(e-p-q)=e-p-q$ leaves $2p\circ q=0$.
The other pairs follow by permutation, and points of distinct components
have overlap $1/3$.

\emph{Uniqueness and converse.}
The three points of any Jordan frame contained in the code have pairwise
overlap zero, so they form a triangle of the graph, and its only triangles
are its components. The converse is immediate.
\end{proof}

The codes with $N=39$ in Proposition~\ref{prop:frames} are exactly the tight $39$-point codes of
Cohn, Kumar and Minton\cite{CKM16}. Such a code attains the bound of the certificate, so it is
tight in their sense (their Definition~2.6). Conversely, a tight code is optimal (their
Proposition~2.8): no code of its size has smaller maximal overlap. Their construction has
maximal overlap $1/3$ (their Theorem~8.3), so a tight $39$-point code has no overlap above $1/3$.
Proposition~\ref{prop:frames} does not show that an arbitrary tight
$39$-point code contains a complex quartet.

\begin{lemma}[Local constancy of the frame partition]\label{lem:partition}
The partition \leannote{partition}{Proofs/TCConsumer.lean}{117}in Proposition~\ref{prop:frames} is locally constant on $\mathcal C$.
\end{lemma}

\begin{proof}
On a small neighborhood each pair overlap changes by less than $1/6$. On
$\mathcal C$ it can only be $0$ or $1/3$, so it is constant there, and so are
the zero-overlap graph and the partition.
\end{proof}

Locally on $\mathcal C$ the points can therefore be indexed by a frame
$f\in\{0,\ldots,12\}$ and a position $t\in\{0,1,2\}$ in it, and studied
through the equations
\begin{equation}\label{eq:frame-equations}
\begin{gathered}
 p_{f,t}\circ p_{f,t}=p_{f,t},\qquad \operatorname{tr}p_{f,t}=1,
 \qquad \sum_t p_{f,t}=e,\\
 \langle p_{f,t},p_{f',t'}\rangle=
 \begin{cases}0,&f=f',\ t\ne t',\\1/3,&f\ne f'.\end{cases}
\end{gathered}
\end{equation}
Their real solution set is the set $\mathcal Z$ of the introduction. It is exactly the set of
codes in $\mathcal C$ whose frames are the triples $(p_{f,0},p_{f,1},p_{f,2})$: the equations
give overlaps $0$ within frames and $1/3$ across them, and Proposition~\ref{prop:frames} gives
the equations for such a code. By Lemma~\ref{lem:partition} it is open and closed in
$\mathcal C$, so near a point of $\mathcal Z$ every code of $\mathcal C$ lies in $\mathcal Z$. 
The residual
\[
 F:J^{39}\longrightarrow\mathbb R^{2184}
\]
consists of $1053=39\cdot27$ idempotency coordinates, $39$ trace equations,
$351$ frame-sum coordinates and $741$ distinct-pair overlap equations. Some
equations are redundant; all are retained in Theorem~\ref{thm:bound}.

\begin{lemma}[Spanning]\label{lem:span}
The thirty-nine points of a tight $39$-point code span $J$.
\end{lemma}

\begin{proof}
In the proof of Proposition~\ref{prop:frames}, $\operatorname{rank}G=40-13=27=\dim J$.
\end{proof}