\section{The quadratic maps and their coefficients}\label{app:quadrics}
Apart from Appendices~\ref{app:normalization}--\ref{app:calculus}, this appendix is needed only to repeat the verification.

\subsection{The maps in matrix form}
The map $H$ and the first component of $T$ have a short description in the coordinates
$(a,B)$ of Section~\ref{sec:families}. From the twelve numbers $u_{ia}$ form the pair
\[
 a=\begin{pmatrix}0&\bar u_{01}&u_{02}\\u_{01}&0&\bar u_{00}\\
 \bar u_{02}&u_{00}&0\end{pmatrix},\qquad
 B=\begin{pmatrix}u_{21}&u_{32}&u_{10}\\-u_{11}&u_{22}&-u_{30}\\u_{31}&u_{12}&u_{20}\end{pmatrix},
\]
and put
\[
 a'=a^2-BB^*,\qquad B'=-aB+\operatorname{adj}(B)^*.
\]
Since $\operatorname{tr}a=0$, the square formula \eqref{eq:titssquare} shows that $B'$ is the
second component of $(a,B)^2$ and that $a'$ agrees with the first component off the diagonal.
With $\sigma$ as in Section~\ref{sec:exhaustion},
\begin{equation}\label{eq:Hmatrix}
\begin{aligned}
 H_0(u)+\sigma(u_0)&=\bigl(a'_{12},\ a'_{01},\ a'_{20}\bigr),\\
 H_1(u)+\sigma(u_1)&=\bigl(-\overline{B'_{02}},\ \overline{B'_{10}},\ -\overline{B'_{21}}\bigr),\\
 H_2(u)+\sigma(u_2)&=\bigl(\overline{B'_{22}},\ \overline{B'_{00}},\ \overline{B'_{11}}\bigr),\\
 H_3(u)+\sigma(u_3)&=\bigl(\overline{B'_{12}},\ -\overline{B'_{20}},\ -\overline{B'_{01}}\bigr),\\
 T_0(u)&=\bigl(-(B^*B)_{12},\ -(B^*B)_{02},\ (B^*B)_{10}\bigr),
\end{aligned}
\end{equation}
with matrix indices running over $0,1,2$.

The equations \eqref{eq:Hmatrix} were verified by expansion in computer algebra against the
formulas written out below, which are the definition used in the formal development. The
pair $(a,B)$ is an element of $J$ with zero diagonal, so $\sigma+H$ is, up to signs and
conjugations, the off-diagonal part of its square. It is not claimed to be the first-order
deformation with coordinates $u$. For $T_1$, $T_2$, $T_3$ we give only the written-out
formulas.

\subsection{The identities in the proof of Lemma~\ref{lem:array}}\label{app:array-proof}

Identity \eqref{eq:counting} counts pairs of entries
of the array: pairs in different rows on the left; on the right, pairs in different columns,
less those in one row, plus those in one column. For \eqref{eq:second} we have only the
expansion.

Identity \eqref{eq:composition} is the multiplicativity of the octonion norm. By
\eqref{eq:Hmatrix} the twelve components of $\sigma+H$ are, up to signs and conjugations, the
off-diagonal coordinates of the square of an element of $J$ with zero diagonal. In the coordinates of Appendix~\ref{app:coordinates} the three
octonion entries of that element have the columns $x_1,x_2,x_3$ as coordinates, again up to
signs and conjugations, and the off-diagonal entries of its square are the conjugates of their
pairwise products.

\subsection{The maps written out}
The formulas below \leannote{quadratic maps}{Proofs/BookHTQuartic.lean}{31}fix all signs and conjugations in
\eqref{eq:quartic}.
\begin{align*}
H_0={}&\bigl(u_{30}\bar u_{20}+u_{11}\bar u_{31}-u_{22}\bar u_{12},\quad
 u_{10}\bar u_{30}+u_{21}\bar u_{11}-u_{32}\bar u_{22},\\[-2pt]
 &\hspace{30mm}-u_{20}\bar u_{10}-u_{31}\bar u_{21}-u_{12}\bar u_{32}\bigr),\\
H_1={}&\bigl(-u_{01}\bar u_{30}+\bar u_{02}\bar u_{20}+u_{31}u_{22},\quad
 -u_{00}\bar u_{31}-\bar u_{01}\bar u_{21}-u_{20}u_{32},\\[-2pt]
 &\hspace{30mm}\bar u_{00}\bar u_{22}+u_{02}\bar u_{32}-u_{30}u_{21}\bigr),\\
H_2={}&\bigl(\bar u_{00}\bar u_{30}-u_{02}\bar u_{10}+u_{32}u_{11},\quad
 u_{01}\bar u_{11}-\bar u_{02}\bar u_{31}+u_{30}u_{12},\\[-2pt]
 &\hspace{30mm}-u_{00}\bar u_{12}-\bar u_{01}\bar u_{32}-u_{10}u_{31}\bigr),\\
H_3={}&\bigl(-u_{00}\bar u_{20}-\bar u_{01}\bar u_{10}-u_{21}u_{12},\quad
 -\bar u_{00}\bar u_{11}+u_{02}\bar u_{21}+u_{10}u_{22},\\[-2pt]
 &\hspace{30mm}u_{01}\bar u_{22}+\bar u_{02}\bar u_{12}-u_{20}u_{11}\bigr).
\end{align*}
\begin{align*}
T_0={}&\bigl(-u_{10}\bar u_{32}+u_{30}\bar u_{22}-u_{20}\bar u_{12},\quad
 -u_{10}\bar u_{21}-u_{30}\bar u_{11}-u_{20}\bar u_{31},\\[-2pt]
 &\hspace{30mm}-u_{11}\bar u_{22}+u_{31}\bar u_{12}+u_{21}\bar u_{32}\bigr),\\
T_1={}&\bigl(u_{00}u_{21}+\bar u_{01}u_{31}-\bar u_{30}\bar u_{22},\quad
 -u_{00}\bar u_{32}-\bar u_{02}\bar u_{22}-u_{20}u_{31},\\[-2pt]
 &\hspace{30mm}u_{01}u_{20}-\bar u_{02}u_{30}+\bar u_{32}\bar u_{21}\bigr),\\
T_2={}&\bigl(u_{00}u_{32}+\bar u_{01}u_{12}+\bar u_{30}\bar u_{11},\quad
 -u_{00}\bar u_{10}+\bar u_{02}\bar u_{30}-u_{31}u_{12},\\[-2pt]
 &\hspace{30mm}u_{01}u_{31}-\bar u_{02}u_{11}+\bar u_{10}\bar u_{32}\bigr),\\
T_3={}&\bigl(u_{00}u_{10}+\bar u_{01}u_{20}-\bar u_{22}\bar u_{11},\quad
 -u_{00}\bar u_{21}+\bar u_{02}\bar u_{11}-u_{20}u_{12},\\[-2pt]
 &\hspace{30mm}u_{01}u_{12}+\bar u_{02}u_{22}+\bar u_{10}\bar u_{21}\bigr).
\end{align*}

\subsection{Normalizing the transverse coordinates}\label{app:normalization}
Use the anti-Hermitian generators $\sqrt{-1}\,(E_{rs}+E_{sr})$ and
$E_{rs}-E_{sr}$, in pair order $01,02,12$. For quartet $i$, the infinitesimal simultaneous
conjugation with parameter $u_i$ has zero diagonal coordinates. Writing
$u_{ia}=x_a+\sqrt{-1}\,y_a$ in row $i$, its six off-diagonal coordinates are
\[
\begin{array}{c|rrrrrr}
 i&01\text{ imaginary}&01\text{ real}&02\text{ imaginary}&02\text{ real}&12\text{ imaginary}&12\text{ real}\\\hline
 0&y_0&-x_0&y_2&x_2&y_1&-x_1\\
 1&y_0&x_0&y_1&-x_1&y_2&x_2\\
 2&y_1&-x_1&y_2&x_2&y_0&-x_0\\
 3&y_2&x_2&y_0&-x_0&y_1&x_1
\end{array}
\]

By Section~\ref{sec:exhaustion}, $V_\xi u$ is the sum over $i$ of the velocities of
\eqref{eq:anchored-family} with equal left and right parameters $g=h=e^{t\mathfrak n_i(u_i)}$, transported
back to the original coordinates. A motion of the right parameter alone is tangent to the $F_4$-orbit
(Lemma~\ref{lem:stabilizer}), so the projection to $\mathcal O^\perp$ is that of the
derivative in the left parameter.

Each row of the table maps $u_i$ invertibly and real-linearly onto the six off-diagonal
parameters. In the family of quartet $i$ the tangent space of $M_*$ has only diagonal left
parameters and parameters $d$ (proof of Lemma~\ref{lem:families}(b), Appendix~\ref{app:inclusion}), and the parametrization
of $M_i$ has injective derivative, so the image of row $i$ meets the tangent space of $M_*$
only at zero. Hence the projected image of row $i$ is a complement of the tangent space of $M_*$
in that of $M_i$. At nonresonant parameters these are $\overline{\mathcal T}^K$ and
$\overline{\mathcal T}^{K_i}$ (Lemma~\ref{lem:families}(c)), and by \eqref{eq:Qsplit}
($4+4\cdot6=28$) the four images and $\overline{\mathcal T}^K$ span $\overline{\mathcal T}$.

At nonresonant parameters the image of row $i$ is the isotypic part $W_i$ itself, although the
proofs use only that it is a complement. For $j\ne i$, in the coordinates of quartet $i$, the map
$\theta_j$ is $(a,B)\mapsto(g'ag'^*,g'Bh'^*)$ with $g'$ and $h'$ diagonal and the entries of
$g'$ distinct, as for $\theta_1$ in the proof of Lemma~\ref{lem:TK}. As in that proof,
$\tilde\theta_j$ replaces the left parameter $\dot g$ by $g'\dot gg'^*$ modulo $\mathcal O$, and
this multiplies each off-diagonal entry by a cube root of unity other than one. So the image, which
lies in $\overline{\mathcal T}^{K_i}$, has average zero over $K$; hence it lies in $W_i$, and both
have dimension six.

\subsection{Proof of Lemma~\ref{lem:reduction}}\label{app:reduction}
\emph{Normalizing the chart.}
Let $\Pi$ be the orthogonal projection of $J^{39}$ onto $\mathcal O^\perp$. By the preceding
subsection and Lemma~\ref{lem:families}(c), $\Pi V_\xi$ maps the $i$th factor $\mathbb C^3$ of
$\mathbb C^{12}$ isomorphically onto a complement of the tangent space of $M_*$ in the
tangent space of $M_i$ at $P$. A linear change of the parameters $(\lambda,u_i)$ fixing the
points with $u_i=0$ makes the derivative in $u_i$ of the parametrization of $M_i$ in
Proposition~\ref{prop:simultaneous} equal to this map. The transverse coordinates of the
chart are then the $u_i$ of \eqref{eq:array}, with the norm of $\mathbb C^{12}$ on
$E=\bigoplus_iW_i$.

\emph{Solving for $\eta$.}
Let $\Phi(\lambda,u,\eta)$ be the point of the slice with coordinates $(\lambda,u,\eta)$ in
this chart, and let $\pi_{\operatorname{im}DF_P}$ be the orthogonal projection of the
residual space onto the image of $DF_P$. The map
\[
 (\lambda,u,\eta)\longmapsto
 \bigl(\lambda,u,\pi_{\operatorname{im}DF_P}F(\Phi(\lambda,u,\eta))\bigr)
\]
has invertible derivative at the origin, since the directions $(\lambda,u)$ span the
kernel of $DF_P$ in the slice and $DF_P$ maps the $973$ directions $\eta$ isomorphically
onto its image. By the inverse function theorem the equation
$\pi_{\operatorname{im}DF_P}F(\Phi(\lambda,u,\eta))=0$ is solved near the origin by
$\eta=\hat\eta(\lambda,u)$, with $\hat\eta$ analytic. Put
\[
 b(\lambda,u)=\Phi(\lambda,u,\hat\eta(\lambda,u))-P,\qquad
 f(\lambda,u)=F(P+b(\lambda,u)),
\]
Then $b$ is analytic with values in $\mathcal O^\perp$,
and $b(0)=0$.

(i) A zero of $F$ near $P$ in the slice is a point $\Phi(\lambda,u,\eta)$ at which the last
component of the map above vanishes. So $\eta=\hat\eta(\lambda,u)$, the point is
$P+b(\lambda,u)$, and $f(\lambda,u)=0$. The converse holds by the definition of $f$.

(ii) For $u\in W_i$ the point $\Phi(\lambda,u,0)$ lies in $M_i$ and is a zero
of $F$, so $\hat\eta(\lambda,u)=0$ by uniqueness. Thus $P+b(\lambda,u)$ is the point of $M_i$
with coordinates $(\lambda,u)$, and $f$ vanishes on $\Lambda\times\bigcup_iW_i$.

(iii) $D\hat\eta(0)=0$, because the directions $(\lambda,u)$ lie in the
kernel of $DF_P$. Hence $D_ub(0)$ is the derivative of the chart in $u$ at the origin, which
is $\Pi V_\xi$ by the normalization.

\subsection{Proof of Lemma~\ref{lem:stress-calculus}}\label{app:calculus}
(a) Apply $\ell$ to $F(x+v)=DF_xv+\mathcal Q(v)$.

(b) Differentiate $F(gy)=\rho_gF(y)$ in $g$, and then in $y$ at $x$ in the direction $v$:
\begin{align*}
 DF_y(\delta y)&=\rho_\delta F(y),\\
 2\mathcal B(v,\delta x)+DF_x(\delta v)&=\rho_\delta DF_xv=0.
\end{align*}
Apply $\ell$ to the second line. For the last assertion, the first line at $y=x$ shows that
$\delta x$ lies in $\ker DF_x$ as well; so the first assertion applies to the cross term and to
the square of $\delta x$.

(c) The first assertion follows from $DF_{gx}\circ g=\rho_g\circ DF_x$, the second from
$DF_{x'}=DF_x+2\mathcal B(x'-x,\cdot\,)$.

(d) Let $\gamma$ be the curve, with $\gamma(0)=x$ and $\gamma'(0)=v$. Differentiating
$F(\gamma(t))=0$ twice at $t=0$ gives
$DF_x\gamma''(0)+2\mathcal Q(\gamma'(0))=0$; apply $\ell$. A quadratic form that vanishes on
a linear subspace has vanishing polar form there.

\subsection{Exact coefficient data}
The ancillary file \texttt{native-data.json} holds the coefficients of
$V_\xi$, $h_{ia}$ and $t_{ia}$ as exact integer tuples.
All indices start at zero.
The explanatory strings inside the file use an earlier notation: there a coefficient is written
$[A,B,C,D,N]$, the parameters $\xi_1,\ldots,\xi_4$ are called $A,B,C,D$, and the file's $z$, $y_j$,
$u_j$, $K_j$, $R$, $S$, $d_i(u)$, $\lambda$ and $d_0,d_1,d_2$ are our $u$, $\tilde u_j$, $U_j$,
$V^{(j)}$, $V'^{(j)}$, $V''^{(j)}$, $\tau_i(U)$, $h^*$ and $\alpha_1,\alpha_2,\alpha_3$; the matrices
$V'^{(j)}$ and $V''^{(j)}$ are stored under the keys \texttt{real\_difference} and
\texttt{imaginary\_sum}, and ``phase'', ``anchor'' and ``sheet'' there mean parameter, quartet and family.

\paragraph{Encoding.}
A coefficient $[n_1,n_2,n_3,n_4,N]$ means
\[
 \bigl(n_1+n_2\sqrt{-1}+n_3\sqrt3+n_4\sqrt{-1}\sqrt3\bigr)/N .
\]
A sparse matrix entry $[r,s,n_1,n_2,n_3,n_4,N]$ adds
this coefficient in row $r$, column $s$; unspecified entries are zero. An entry of a list
for $h$ is $[r,n_1,n_2,n_3,n_4,N]$, the coefficient of residual row $r$; apply its list's
\texttt{conjugated} and \texttt{negated} flags to the coefficient, not its row index, before
summing. An entry of a list for $t$ appends four integer exponents to this six-tuple.

\paragraph{Coordinates and residual rows.}
A point of $J$ has the $27$ real coordinates
$(\alpha_1,\alpha_2,\alpha_3,o_{01},o_{02},o_{12})$:
the diagonal, then the three octonions above it, each
in basis $(1,i,j,k,\ell,i\ell,j\ell,k\ell)$. The cyclic
coordinates of Appendix~\ref{app:coordinates} satisfy $o_{01}=x_3$, $o_{02}=\bar x_2$,
$o_{12}=x_1$, and $n=j\ell$, $in=-k\ell$.
Point $p=3f+t$ has coordinates $27p+k$, $0\le k<27$. The rows of $F$ are
\[
\begin{array}{c|l}
\text{row}&\text{equation}\\\hline
27p+k &(P_p^2-P_p)_k\\
1053+p&\operatorname{tr}P_p-1\\
1092+27f+k &(\sum_t P_{3f+t}-e)_k\\
1443+p(77-p)/2+q-p-1&\langle P_p,P_q\rangle-\gamma_{pq}\quad(p<q),
\end{array}
\]
where $\gamma_{pq}=0$ within a frame and $1/3$ otherwise.

\paragraph{The directions $V_\xi u$.}
Place the four triples $u_0,u_1,u_2,u_3$ in coordinates
$(0,1,2)$, $(6,9,12)$, $(8,11,14)$, $(7,10,13)$ of $\tilde u\in\mathbb C^{24}$.
The remaining coordinate in each ordered pair
\[
\begin{gathered}
 (0,3),(1,5),(2,4),(6,15),(9,21),(12,18),\\
 (8,16),(11,22),(14,19),(7,17),(10,23),(13,20)
\end{gathered}
\]
is minus the conjugate of the first. For each pair $(j,j')$, the file
gives two sparse real $27\times27$ matrices $V'^{(j)}$ and $V''^{(j)}$. Set
\[
 V^{(j)}=\bigl(V'^{(j)}-\sqrt{-1}\,V''^{(j)}\bigr)/2,\qquad
 V^{(j')}=-\bigl(V'^{(j)}+\sqrt{-1}\,V''^{(j)}\bigr)/2 .
\]
At every point $p$ put
\[
 (V_\xi u)_p=\operatorname{Re}\sum_{j=0}^{23}\tilde u_jV^{(j)}P(\xi)_p.
\]
Substituting the matrices $G_i$, $L_i$, $R_i$ of Appendix~\ref{app:coordinates} and the table of Appendix~\ref{app:normalization}
shows that this is the transported family velocity for every $\xi\in(S^1)^4$. The same matrix
acts on every point; the $V^{(j)}$ are not asserted to be derivations of $J$.
As a redundant check, the file also stores $V^{(j)}P(\xi_*)$, for the base
parameter $\xi_*$ below, as column \texttt{eigen\_index[j]} of \texttt{seed\_columns}, with
common denominator $384540$.

\paragraph{The covectors $t_{ia}$.}
Put
\[
 \xi_*=\bigl((3+4\sqrt{-1})/5,\ (5+12\sqrt{-1})/13,\ (15+8\sqrt{-1})/17,\ (21+20\sqrt{-1})/29\bigr)
\]
and $U_j=\xi_{j+1}/\xi_{*,j+1}$ for $j=0,\ldots,3$.
The file stores each $t_{ia}$ with Laurent monomial coefficients:
an entry $(r,c,\nu)$ contributes $cU_0^{\nu_0}\cdots
U_3^{\nu_3}$ to row $r$ of $t_{ia}$; as the $U_j$ are units, no further denominators arise.

\paragraph{The covectors $h_{ia}$.}
The file stores the twelve $h_{ia}$ at $\xi_*$, written $h^*_{ia}$.
The automorphism $\tau_i(U)$ fixes the first three diagonal
coordinates. On each coordinate pair $(x_j,y_j)$ in positions
$(3+2j,4+2j)$, $0\le j<12$,
it multiplies $x_j-\sqrt{-1}\,y_j$ and $x_j+\sqrt{-1}\,y_j$ by $\chi_j,\chi'_j$, respectively.
For $i=0,1$ it is the identity. For $i=2$ put
\[
 (\varphi_0,\varphi_1,\varphi_2)=(U_0U_1,U_1^{-1},U_0^{-1}),\qquad(\psi_0,\psi_1,\psi_2)=(1,1,1);
\]
for $i=3$ put
\[
 (\varphi_0,\varphi_1,\varphi_2)=(1,1,1),\qquad
 (\psi_0,\psi_1,\psi_2)=(U_3,(U_2U_3)^{-1},U_2).
\]
In either case the character table is
\[
\begin{array}{c|cc@{\qquad}c|cc}
j&\chi_j&\chi'_j&j&\chi_j&\chi'_j\\\hline
0&\varphi_1^2\varphi_2&\varphi_0^2\varphi_2&6&\varphi_1\psi_0\psi_2&\varphi_0\varphi_2\psi_1\\
1&\varphi_2\psi_1\psi_2&\varphi_0\varphi_1\psi_0&7&\varphi_0\varphi_2\psi_2&\varphi_1\psi_0\psi_1\\
2&\varphi_2\psi_0\psi_2&\varphi_0\varphi_1\psi_1&8&\varphi_0\varphi_2^2&\varphi_0\varphi_1^2\\
3&\varphi_0\varphi_1\psi_2&\varphi_2\psi_0\psi_1&9&\varphi_0\psi_1\psi_2&\varphi_1\varphi_2\psi_0\\
4&\varphi_1\varphi_2^2&\varphi_0^2\varphi_1&10&\varphi_0\psi_0\psi_2&\varphi_1\varphi_2\psi_1\\
5&\varphi_1\psi_1\psi_2&\varphi_0\varphi_2\psi_0&11&\varphi_1\varphi_2\psi_2&\varphi_0\psi_0\psi_1
\end{array}
\]
That these maps are automorphisms of $J$ follows by substitution in the product formula of
Appendix~\ref{app:coordinates}. On the twelve points
of quartet $i$, $\tau_i(U)P(\xi_*)=P(\xi)$.
Let
\[
\begin{gathered}
 c_0=c_1=(1,1,1),\qquad c_2=((U_0U_1)^{-1},U_0,U_1),\\
 c_3=(U_3,(U_2U_3)^{-1},U_2),
\end{gathered}
\]
with entries $c_{ia}$ (these triples are not the class $c_0$ of the introduction). Then
\[
 h_{ia}=c_{ia}^{-1}\,h^*_{ia}\,\rho_{\tau_i(U)}^{-1},
\]
with $\rho$ as in Section~\ref{sec:exhaustion}.

That $h_{ia}$ is a stress at $P(\xi)$ follows from
Lemma~\ref{lem:stress-calculus}(c) and the following: $h^*_{ia}$ is a stress at $P(\xi_*)$; the quadratic form
$h^*_{ia}\mathcal Q$ is supported on the twelve points of quartet $i$; the configurations
$\tau_i(U)P(\xi_*)$ and $P(\xi)$ agree at those twelve points; and $F$ is equivariant. The
normalization by $c_{ia}$ is needed for reproduction, not for equilibrium.

\paragraph{The identities to be checked.}
The finite verification of \eqref{eq:equilibrium}--\eqref{eq:reproduction} has three
checks, with $F$ formed by the Jordan square and trace-form formulas of
Appendix~\ref{app:coordinates}.
\begin{enumerate}
\item[(i)] \emph{Equilibrium.} For each of the $24$ covectors, the contraction with the
$2184\times1053$ matrix $DF_P$ is zero.
\item[(ii)] \emph{Reproduction.} For each covector, substitute $V_\xi u$ into the homogeneous
quadratic part of $F$, contract, and collect the $300$ monomials of degree two in the $24$ real and
imaginary parts of the entries of $u$. The coefficients are those of the displayed
component of $H$ or $T$.
\item[(iii)] \emph{Support.} For each of the twelve $h_{ia}$, the contraction with the homogeneous
quadratic part has no monomial involving a point outside the twelve points of quartet $i$.
\end{enumerate}
These are finite polynomial identities over $\mathbb Q(\sqrt{-1},\sqrt3)$, Laurent in the
parameters $\xi_j$, with their conjugates replaced by inverses. Equality is coefficient equality, not agreement at sampled parameters. In the formal
development each check reduces to finitely many equalities of integer-coded data, decided by
evaluation in the Lean kernel. For $t$, the stored Laurent coefficients \leannote{all-parameter T identity}{Proofs/HTPhaseCompleteTValue.lean}{94}supply the identities for all $\xi$ directly.
For $h$, the formal development derives reproduction at every $\xi$ from the identities for
$h^*_{ia}$ at $\xi_*$. Only the twelve points of quartet $i$ enter, and there the transport
multiplies each coordinate of $u$ and of $\bar u$ by a monomial in $U$; every monomial of
$H_i(u)_a$ then acquires the factor $c_{ia}$, which the normalization removes
\textup{(}\texttt{H\_reproduction\_phase}, the declaration behind the note on
Proposition~\ref{prop:finite}\textup{)}.

Outside the formal development, the script \texttt{anc/finite-identities.py}, which uses only the
Python standard library, replays checks (i)--(iii) from the file in exact arithmetic over
$\mathbb Q(\sqrt{-1},\sqrt3)$. It compares Laurent coefficients in $U_0,\ldots,U_3$, so the checks
hold for every $\xi\in(S^1)^4$. It forms $P(\xi)$, $F$, $H$ and $T$ from \eqref{eq:literal} and
the formulas of this appendix. It also checks, identically in $\xi$, that $F(P(\xi))=0$, that
$DF_PV_\xi u=0$, and that the formula above for $V_\xi u$ is the sum of the four family
velocities of Section~\ref{sec:exhaustion}, built from Appendix~\ref{app:coordinates} and the
table of Appendix~\ref{app:normalization}. It does not compare these formulas with the definitions of the formal development.