\section{Constructing the four families}\label{sec:families}
The matrices placing
$P(\xi)$ in each quartet's coordinates are needed only for verification
(Appendix~\ref{app:coordinates}).

\subsection{The family and its four subalgebras}
Fix the octonion basis $(1,i,j,k,\ell,i\ell,j\ell,k\ell)$, put $n=j\ell$,
and use left complex coefficients, so $in=-k\ell$. For two unit octonions
$u,w$ put
\[
 p(1,u,w)=\tfrac13\,vv^*,\qquad v=(1,u,w)^{\mathsf T}.
\]
Artin's theorem makes the subalgebra generated by $u,w$ associative, so
this is a point.
With $\omega=e^{2\pi i/3}$, the four-parameter family of
Cohn, Kumar and Minton is
\begin{equation}\label{eq:literal}
\begin{array}{c|c}
\text{frame}&\text{point index }t\\\hline
0&\text{the coordinate idempotent }E_{tt}\\
1+s&p(1,\omega^t,\omega^{s-t})\\
4+s&p(1,\omega^t j,\omega^{s+t}\ell)\\
7+s&p(1,\xi_1\omega^t\ell,\xi_2\omega^{s+t}n)\\
10+s&p(1,\xi_3\omega^t n,\xi_4\omega^{s+t}j).
\end{array}
\end{equation}
Here $s,t\in\{0,1,2\}$. The
parameters $\xi=(\xi_1,\ldots,\xi_4)$ are four unit complex numbers, those on
p.~49 of Cohn, Kumar and Minton\cite{CKM16}, and $\xi=1$ gives their code (8.2).
In their notation $(1,\omega^au,\omega^bw)$ the frames of the first type are the
classes of $a+b$ modulo $3$, and those of the three octonionic types the classes
of $b-a$; the proof of their Theorem~8.3 describes all four by $a+b$.

Each later row of \eqref{eq:literal} holds
three frames: for $i=0,1,2,3$ the frames $1+3i+s$ form \emph{lobe $i$}, and
frame $0$ with lobe $i$ forms \emph{quartet $i$}.

Left multiplication by
$\mathbb C=\mathbb R\oplus\mathbb Ri$ splits the octonions into four mutually
orthogonal complex lines,
\[
 \mathbb O=\mathbb C\oplus\mathbb Cj\oplus\mathbb C\ell\oplus\mathbb Cn,
\]
each closed under conjugation. The table
\begin{equation}\label{eq:latin}
\begin{array}{c|ccc}
 i&(1,2)&(1,3)&(2,3)\\\hline
 0&\mathbb C&\mathbb C&\mathbb C\\
 1&\mathbb Cj&\mathbb C\ell&\mathbb Cn\\
 2&\mathbb C\ell&\mathbb Cn&\mathbb Cj\\
 3&\mathbb Cn&\mathbb Cj&\mathbb C\ell
\end{array}
\end{equation}
assigns to each quartet one line for each of the three positions above the
diagonal. Let $A_i\subset J$ consist of the matrices whose entries in these
positions lie in the lines of row $i$. Let $D\subset J$ be the space of real
diagonal matrices, the span of frame~$0$, and let $N_i$ be the matrices in
$A_i$ with zero diagonal, so that $A_i=D\oplus N_i$. Row $0$ gives
$A_0=H_3(\mathbb C)$.

\begin{lemma}[Four subalgebras]\label{lem:subalgebras}
\begin{enumerate}
\item[\textup{(a)}] Each $A_i$ is a subalgebra of $J$ of dimension nine,
isomorphic to $H_3(\mathbb C)$ and containing $D$. The sum
\begin{equation}\label{eq:decomposition}
 J=D\oplus N_0\oplus N_1\oplus N_2\oplus N_3
\end{equation}
is direct and orthogonal for the trace form. In particular
$A_i\cap A_{i'}=D$ for $i\ne i'$.
\item[\textup{(b)}] Let two points lie in two different subalgebras $A_i$
and $A_{i'}$, and let each have overlap $1/3$ with the three points of
frame~$0$. Then the two points have overlap $1/3$.
\item[\textup{(c)}] For every $\xi$ the points of lobe $i$ of $P(\xi)$ lie in
$A_i$. Lobes $0$ and $1$ do not depend on $\xi$. Lobes $2$ and $3$
of $P(\xi)$ are the images of the same lobes of $P(1)$ under the
automorphisms of the algebras $A_2$ and $A_3$ that fix the diagonal and
multiply the entries in positions $(1,2)$, $(1,3)$, $(2,3)$ on the left,
respectively, by
\[
 \xi_1,\ \xi_2,\ \overline{\xi_1\xi_2}\quad\text{in }A_2,\qquad\qquad
 \xi_3,\ \xi_4,\ \overline{\xi_3\xi_4}\quad\text{in }A_3.
\]
\end{enumerate}
\end{lemma}

\begin{proof}
Part~(b) follows from part~(a). A point having overlap $1/3$ with the three
points of frame~$0$ has diagonal entries $1/3$. So the two points are
$p=e/3+p'$ and $q=e/3+q'$ with $p'\in N_i$ and $q'\in N_{i'}$, and by
\eqref{eq:decomposition}
\[
 \langle p,q\rangle=\langle e/3,e/3\rangle+\langle p',q'\rangle=1/3.
\]

Parts~(a) and~(c) are verified entry by entry in
Appendix~\ref{app:subalgebras}. In \eqref{eq:latin}, each column contains each of the four lines once,
so the spaces $N_i$ are mutually orthogonal and with the diagonal fill $J$.
In each row the product of the lines in two positions lies in the line of the
third, as closure of $A_i$ under squaring requires.
\end{proof}

With the tightness of $P(1)$ (Theorem~8.3 of Cohn, Kumar and Minton\cite{CKM16}), parts (b) and~(c)
show again that every $P(\xi)$ is tight, and that each quartet $i$ is a complex quartet
lying in $A_i$.

Quartet $0$ is the standard complex quartet\cite{BBRV02}, the eigenbases of $Z$, $X$, $XZ$ and $XZ^2$,
with $X$, $Z$ as defined before \eqref{eq:ueb}.

\subsection{Coordinates relative to a quartet}
By \eqref{eq:decomposition} the orthogonal complement of
$A_0=H_3(\mathbb C)$ in $J$ is $N_1\oplus N_2\oplus N_3$. An element of this
complement has three entries above the diagonal, each in
$\mathbb Cj\oplus\mathbb C\ell\oplus\mathbb Cn$; its nine complex coordinates
are arranged in a matrix $B\in M_3(\mathbb C)$. This
gives a real-linear isomorphism
\[
 J\simeq H_3(\mathbb C)\oplus M_3(\mathbb C),\qquad x\longmapsto(a,B),
\]
written out and verified in Appendix~\ref{app:coordinates}. It is the second Tits construction for
$M_3(\mathbb C)$ with conjugate transposition, in the case that gives the
Euclidean algebra $J$; Yokota writes out the same decomposition with its
product in his Section~2.12\cite{Yokota09}.

In these coordinates the unit is $(I,0)$, the trace of $(a,B)$ is the trace
of $a$, and the trace form is
\begin{equation}\label{eq:titsmetric}
 \langle(a,B),(a',B')\rangle
 =\operatorname{Re}\operatorname{tr}(aa')+2\operatorname{Re}\operatorname{tr}(BB'^*).
\end{equation}
The square formula is
\begin{equation}\label{eq:titssquare}
 (a,B)^2=\bigl(a^2-BB^*+\operatorname{tr}(BB^*)I,\
  ((\operatorname{tr}a)I-a)B+\operatorname{adj}(B)^*\bigr).
\end{equation}
Polarization \leannote{Jordan product}{Proofs/NativeIncludedQuartetReadouts.lean}{1447}recovers the product of $J$. The formulas hold for every
complex matrix $B$.

Appendix~\ref{app:coordinates} gives, for $i=1,2,3$, an automorphism $\iota_i$
of $J$ that maps $A_0$ onto $A_i$; let $\iota_0$ be the identity. The
\emph{coordinates of quartet $i$} of an element $x$ are the pair
$(a,B)$ of $\iota_i^{-1}x$. In them $A_i$ is the set of pairs $(a,0)$.

Let $\theta_i$ be the map of $J$ that in the coordinates of quartet $i$ is
\[
 \theta_i\colon(a,B)\longmapsto(a,\omega B).
\]
It preserves squares, by \eqref{eq:titssquare} and
$\operatorname{adj}(\omega B)^*=\omega\operatorname{adj}(B)^*$. So it is an
automorphism of $J$ of order three.
Appendix~\ref{app:coordinates} gives $\theta_i$ in octonion coordinates; up
to the conventions for the
octonion basis, $\theta_0$ is the automorphism $w$ of Yokota's Section~2.12,
or its inverse\cite{Yokota09}.

The twelve points of a complex quartet in $A_i$ span $A_i$. Subtract
$e/3$ from the three points of a frame: the results span a plane, because
their Gram matrix $I-\mathbf1\mathbf1^{\mathsf T}/3$ has rank two. The four
planes are mutually orthogonal because the frames are mutually unbiased, and
with the unit they span $4\cdot2+1=9$ dimensions. Consequently a point
having overlap $1/3$ with all twelve has component $e/3$ in $A_i$: once
$e/3$ is subtracted, it is orthogonal to their span.

\begin{lemma}[Points and frames outside a quartet]\label{lem:dictionary}
Let a complex quartet lie in $A_i$. Write $\theta=\theta_i$ and use the
coordinates $(a,B)$ of quartet $i$.
\begin{enumerate}
\item[\textup{(i)}] For \leannote{points off a quartet}{Proofs/LiteralNativeQuartetReadouts.lean}{50}a point $p$ the following are equivalent: $p$ has
overlap $1/3$ with all twelve points of the quartet;
$p+\theta p+\theta^2p=e$; and
\[
 p=p(U)=(I/3,U/3)\qquad\text{with }U\in SU(3).
\]
\item[\textup{(ii)}] An ordered frame \leannote{ordered frames}{Proofs/NativeComplementaryDictionary.lean}{192}of such points is either
$(p,\theta p,\theta^2p)$ or $(p,\theta^2p,\theta p)$; here
$\theta p(U)=p(\omega U)$. The frames consisting of such points are thus
the orbits of $\theta$ on them.
\item[\textup{(iii)}] Two such frames, the orbits of $p(U)$ and $p(V)$, are
mutually unbiased if and only if $\operatorname{tr}(U^*V)=0$.
\end{enumerate}
\end{lemma}

\begin{proof}
(i) Write $p=(a,B)$. The three cube roots of unity sum to zero, so
\[
 p+\theta p+\theta^2p=(3a,0),
\]
and the second condition says $a=I/3$. The first condition implies this by
the paragraph before the lemma. Conversely, if $a=I/3$, then by
\eqref{eq:titsmetric} the overlap of $p$ with a point $(a',0)$ of the
quartet is $\operatorname{tr}(a')/3=1/3$.

Now let $a=I/3$ and put $U=3B$. By \eqref{eq:titssquare} the two components
of the idempotency equation are
\[
 BB^*=\bigl(\operatorname{tr}(BB^*)-2/9\bigr)I,\qquad
 \operatorname{adj}(B)^*=B/3.
\]
Taking traces in the first gives $\operatorname{tr}(BB^*)=1/3$, so together
they say
\[
 UU^*=I,\qquad\operatorname{adj}(U)^*=U.
\]
The adjugate identity $U\operatorname{adj}(U)=\det(U)I$ shows that these
conditions are equivalent to $U\in SU(3)$. Substitution proves the converse.

(ii) Let three such points, with matrices $U$, $V$, $V'$, form a frame.
Their sum is the unit, so
\[
 U+V+V'=0,\qquad\text{that is,}\qquad V'=-U(I+\Theta)\quad\text{with }\Theta=U^*V.
\]
Since $V'$ and $\Theta$ are unitary, this gives
\[
 \Theta+\Theta^*=-I,\qquad\text{whence}\qquad\Theta^2+\Theta+I=0.
\]
So each eigenvalue of $\Theta$ is a primitive cube root of unity. If $m$ of
them equal $\omega$, the determinant is $\omega^{6-m}$; it equals one, which
forces $m=0$ or $m=3$. Being unitary, $\Theta$ is diagonalizable, hence
scalar. So $(V,V')$ is $(\omega U,\omega^2U)$ or $(\omega^2U,\omega U)$. Conversely, the three points of an orbit of
$\theta$ sum to the unit, by~(i); their Jordan orthogonality follows as in
Proposition~\ref{prop:frames}.

(iii) By \eqref{eq:titsmetric}, for $k,l\in\mathbb Z/3$,
\begin{equation}\label{eq:central-overlap}
 \langle p(\omega^kU),p(\omega^lV)\rangle
 =\frac13+\frac29\operatorname{Re}\bigl(\omega^{k-l}\operatorname{tr}(UV^*)\bigr).
\end{equation}
The nine cross overlaps equal $1/3$ precisely when
$\operatorname{tr}(UV^*)$ and its product with $\omega$ both have real part
zero, that is, when it vanishes; and $\operatorname{tr}(U^*V)$ is its
complex conjugate.
\end{proof}

\subsection{Nine trace-orthogonal unitary matrices}
By Lemma~\ref{lem:dictionary}, a tight code that contains the quartet is
given by nine matrices in $SU(3)$, pairwise orthogonal for
$\operatorname{tr}(U^*V)$ and each determined up to a cube root of unity.
They form an orthogonal basis of $M_3(\mathbb C)$
consisting of unitary matrices, that is, a unitary error basis\cite{Knill96}.

\begin{lemma}[Pointwise stabilizer of a complex quartet]\label{lem:stabilizer}
The \leannote{pointwise stabilizer}{Proofs/NativeAnchorFixerClassification.lean}{108}automorphisms of $J$ fixing a complex quartet in $A_i$ pointwise are, in the coordinates of quartet $i$, exactly the maps
\[
 (a,B)\longmapsto(a,Bh),\qquad h\in SU(3).
\]
\end{lemma}

\begin{proof}
Such an automorphism fixes the span $A_i$ of the quartet pointwise and,
preserving the trace form, preserves the orthogonal complement.

Its action there commutes with left multiplication by every Hermitian
matrix, because
\[
 (a,0)\circ(0,B)=\left(0,\frac{(\operatorname{tr}a)I-a}{2}B\right),
\]
and every Hermitian matrix $b$ occurs as the multiplier: take
$a=(\operatorname{tr}b)I-2b$.
Hermitian matrices generate $M_3(\mathbb C)$ as a real algebra, so a
commuting real-linear map is right multiplication by a matrix $h$, the image
of $I$.

Preservation of the trace form gives $hh^*=I$, and preservation of
\eqref{eq:titssquare} at $(0,I)$ gives $\operatorname{adj}(h)^*=h$. Thus
$h\in SU(3)$. Conversely, substitution in the product obtained from
\eqref{eq:titssquare} shows that right multiplication of $B$ by any matrix
in $SU(3)$ is an automorphism.
\end{proof}

These right multiplications form the factor $SU(3)$ that fixes $H_3(\mathbb C)$
pointwise in Yokota's description\cite{Yokota09} of the subgroup
$(SU(3)\times SU(3))/(\mathbb Z/3)$
(his Proposition~2.12.1 and Theorem~2.12.2). His left action on his
matrix $M$ is our right action, since $B$ corresponds to $M^*$ up to sign
and the identification of bases.

Let $(U_r)$, $r=0,\ldots,8$, be a labeled array of representatives of
mutually unbiased frames. The right multiplication of
Lemma~\ref{lem:stabilizer} is removed by
\begin{equation}\label{eq:rightnormalization}
 U_r\longmapsto U_rU_0^*.
\end{equation}
The result is unchanged when all nine matrices are multiplied on the right
by the same matrix, and its first entry is $I$.

Let $e_0,e_1,e_2$ be the
standard basis of $\mathbb C^3$, and let
\[
 Xe_k=e_{k+1},\qquad Ze_k=\omega^ke_k,
\]
with indices modulo three (the shift and clock matrices). The triples
$d=(d_0,d_1,d_2)$ of unit complex numbers with product one form a two-torus,
written $T^2$. For $d\in T^2$ set
\begin{equation}\label{eq:ueb}
 E_{ab}(d)=X^bD_bZ^a,\qquad D_0=D_1=I,\quad D_2=\operatorname{diag}(d).
\end{equation}
These nine matrices lie in $SU(3)$ and form a unitary error basis:
different powers of $X$ have disjoint supports, and for a fixed power the
orthogonality is that of the characters $k\mapsto\omega^{ak}$ of
$\mathbb Z/3$.
This is an instance of the shift-and-multiply construction of Vollbrecht
and Werner\cite{VW00} (their eq.~(3.6)). Up to the
equivalence of unitary error bases, Svegborn, Pauwels, Gisin and
Pozas-Kerstjens\cite{SPGP26} classify a one-parameter family of bases of this form
(their Theorem~1). That equivalence allows unitary factors on both sides,
phases and relabeling. Lemma~\ref{lem:embedded} divides only by the common right factor of
Lemma~\ref{lem:stabilizer}, which leaves the eight parameters of $g$; up to conjugation and
phases, their family lies on a circle in $T^2$.

\begin{lemma}[The normalized family]\label{lem:embedded}
Applying \eqref{eq:rightnormalization} to the array $gE_{ab}(d)h^*$, with
$g,h\in SU(3)$, gives
\begin{equation}\label{eq:normalizedfamily}
 U_{ab}(g,d)=gE_{ab}(d)g^*,\qquad ([g],d)\in PSU(3)\times T^2.
\end{equation}
The \leannote{embedded family}{Proofs/NativeNormalizedA2Headline.lean}{21}map
sending $([g],d)$ to this array
is an embedding of a manifold of dimension $8+2=10$. By
Lemma~\ref{lem:dictionary} its image is a ten-parameter family of labeled
solutions of \eqref{eq:frame-equations} in which the quartet is held fixed.
\end{lemma}

\begin{proof}
The entries $gZg^*$ and $gXg^*$ of the array determine $g$ up to the center,
because a matrix commuting with both $X$ and $Z$ is scalar; then the entry
$gX^2\operatorname{diag}(d)g^*$ determines $d$. Likewise a tangent
variation fixing the first two of these entries is scalar, hence zero in
$\mathfrak{su}(3)$, and then the variation of $d$ is zero. So the map is an
injective immersion, and an embedding because its domain is compact.
The last assertion is Lemma~\ref{lem:dictionary} applied to the nine
matrices of the array, which are special unitary and pairwise
trace-orthogonal.
\end{proof}

\subsection{Applying the construction to each quartet}
For the quartets $i=0,1,2,3$, Lemma~\ref{lem:anchored} below uses the triples
\begin{equation}\label{eq:phase-triples}
\begin{aligned}
d_0(\xi)&=(\xi_1\xi_2/\xi_3,(\xi_1\xi_4)^{-1},\xi_3\xi_4/\xi_2),&
d_1(\xi)&=(\xi_1\xi_3\xi_4,-\xi_2/\xi_3,-(\xi_1\xi_2\xi_4)^{-1}),\\
d_2(\xi)&=(-\xi_3\xi_4,\xi_3^{-1},-\xi_4^{-1}),&
d_3(\xi)&=(-\xi_1^{-1},-\xi_2^{-1},\xi_1\xi_2).
\end{aligned}
\end{equation}
Each triple has product one, so it lies in $T^2$. The subscript of
$d_i(\xi)$ is the quartet, whereas $d_0,d_1,d_2$ without an argument are the
entries of a triple $d$. Each of the twelve
entries is a sign times a nontrivial character of the torus $(S^1)^4$.
Hence the parameters at which some entry has cube one form a finite union
of cosets of closed subgroups of codimension one; by
Proposition~\ref{prop:kernel} these are the resonant parameters. At
$\xi=1$ six of the twelve entries equal $1$, so the original code is
resonant.

\begin{lemma}[The four families with one quartet held fixed]\label{lem:anchored}
Fix $\xi$ and $i$. In the coordinates of quartet $i$ the nine frames of $P(\xi)$
outside quartet $i$ are represented by the matrices
\[
 \zeta_r L_i E_{s_i(r)}(d_i(\xi))R_i,\qquad r=0,\ldots,8.
\]
Here $L_i$ and $R_i$ are unitary with $\det L_i\det R_i=1$, each $\zeta_r$
is a cube root of unity, and
$s_i$ is a bijection from the nine frames onto the nine labels $(a,b)$ of
\eqref{eq:ueb}; all four are written out in
Appendix~\ref{app:coordinates}. Keep the quartet and replace these matrices
by
\begin{equation}\label{eq:anchored-family}
 \zeta_r gL_i E_{s_i(r)}(d)R_i h^*,\qquad g,h\in SU(3),\quad d\in T^2,
\end{equation}
then return to the original coordinates and labels. Every code so obtained
is a labeled solution of \eqref{eq:frame-equations}, and $g=h=I$,
$d=d_i(\xi)$ gives $P(\xi)$. Changing $h$ moves the code by an automorphism
of $J$ \textup{(}Lemma~\ref{lem:stabilizer}\textup{)}.
\end{lemma}

\begin{proof}
The matrices \eqref{eq:anchored-family} have determinant
$\zeta_r^3\det L_i\det R_i=1$ and are pairwise trace-orthogonal, because the
$E_{ab}(d)$ are and $gL_i$, $R_ih^*$ are unitary.
The selected quartet stays fixed,
and Lemma~\ref{lem:dictionary} proves all equations for the other nine frames.
The base point is \eqref{eq:anchorbinding}, and Lemma~\ref{lem:stabilizer} absorbs $h$.
\end{proof}