\section{No further solutions}\label{sec:exhaustion}
This section proves Proposition~\ref{prop:exhaustion}, which gives Theorem~\ref{thm:real}.

\subsection{A stress criterion}
The criterion assumes the following.
\begin{enumerate}
\item[(S1)] $E=W_0\mathbin\perp\cdots\mathbin\perp W_{m-1}$ is a finite-dimensional
Euclidean space, $\mathcal A=\bigcup_iW_i$, and $\Lambda,\mathcal R$ are finite-dimensional real normed spaces.
\item[(S2)] $f:\Lambda\times E\to \mathcal R$ is $C^2$ near zero and vanishes near zero on each branch $\Lambda\times W_i$.
\item[(S3)] The quadratic part $q(u)=\tfrac12D^2f(0)[(0,u),(0,u)]$ has zero set exactly
$\mathcal A$.
\end{enumerate}
Write $\beta$ for the polar form of $q$, the symmetric bilinear map with $\beta(u,u)=q(u)$.

\begin{lemma}[A stress criterion for the distance bound]\label{lem:stress}
Assume \textup{(S1)--(S3)}. \leannote{supported stresses}{Proofs/SupportedStressCriterionV3.lean}{27}Suppose that for each $i$ and each unit vector $w\in W_i$ there is a continuous field of covectors
$\ell(\lambda,a)\in \mathcal R^*$, defined for $(\lambda,a)$ near zero in $\Lambda\times W_i$ and allowed to depend on $w$, such that
\begin{align}
 \ell(\lambda,a)Df(\lambda,a)(0,n)&=0 &&(n\in W_i^\perp),\label{eq:alongstress}\\
 \ell(0,0)q(v)&>0 &&(0\ne v\in W_i^\perp,\ \beta(w,v)=0).\label{eq:stresspos}
\end{align}
Then there are $c>0$ and a neighborhood of zero in $\Lambda\times E$ on which
\[
 \operatorname{dist}(u,\mathcal A)^2\le c\|f(\lambda,u)\|.
\]
In particular $f(\lambda,u)=0$ there if and only if $u\in\mathcal A$.
\end{lemma}

\begin{proof}
Each $f(\lambda,\cdot)$ vanishes on every $W_j$, and these subspaces span $E$. Hence
$D_uf(\lambda,0)=0$ for small $\lambda$.

\emph{A violating sequence.}
Suppose the bound fails for every constant and every neighborhood. Then there is a
sequence with
\[
 (\lambda_k,u_k)\to0,\qquad
 \|f(\lambda_k,u_k)\|=o(\delta_k^2),\qquad
 \delta_k=\operatorname{dist}(u_k,\mathcal A)>0.
\]
Each $u_k$ has a nearest subspace $W_i$, and one index $i$ occurs infinitely often; pass to
that subsequence. Put
\[
 a_k=\operatorname{proj}_{W_i}u_k,\qquad n_k=u_k-a_k\in W_i^\perp,\qquad
 \text{so that }\|n_k\|=\delta_k .
\]
The nearest subspace is the one in which $u_k$ has its largest component, so $a_k\ne0$ and
$\|n_k\|^2\le(m-1)\|a_k\|^2$. A further subsequence has
\[
 \frac{a_k}{\|a_k\|}\to w\in W_i,\qquad
 \frac{n_k}{\|n_k\|}\to v\in W_i^\perp,\qquad
 \frac{\|n_k\|}{\|a_k\|}\to\kappa\in[0,\infty),
\]
with unit vectors $w$ and $v$.

\emph{One expansion.}
Expand $f$ about its zero $(\lambda_k,a_k)$. The second derivative is continuous at the
origin, so
\[
 f(\lambda_k,u_k)=D_uf(\lambda_k,a_k)n_k+q(n_k)+o(\|n_k\|^2).
 \tag{$\ast$}
\]
The derivative in $u$ vanishes at $(\lambda_k,0)$, and integrating the second derivative
along the segment to $(\lambda_k,a_k)$ gives
\[
 D_uf(\lambda_k,a_k)n_k=2\beta(a_k,n_k)+o(\|a_k\|\|n_k\|).
\]
Divide $(\ast)$ by $\|a_k\|\|n_k\|$. The left side tends to zero, by the choice of the
sequence and because the ratio $\|n_k\|/\|a_k\|$ is bounded. In the limit
\[
 2\beta(w,v)+\kappa\,q(v)=0.
\]

\emph{The limit ratio is zero.}
Suppose $\kappa>0$. Since $q(w)=0$,
\[
 q(w+\kappa v)=q(w)+\kappa\bigl(2\beta(w,v)+\kappa\,q(v)\bigr)=0,
\]
so $w+\kappa v$ lies in $\mathcal A$ by \textup{(S3)}. But this vector has nonzero
components both in $W_i$ and in its orthogonal complement, so it lies in none of the
subspaces. Therefore $\kappa=0$, and then $\beta(w,v)=0$.

\emph{Contradiction.}
Take the field attached to this $i$ and $w$, and apply its value at $(\lambda_k,a_k)$ to
$(\ast)$. The first term on the right vanishes exactly, by \eqref{eq:alongstress}. Divide by
$\|n_k\|^2$ and pass to the limit. The left side tends to zero, by the choice of the sequence
and because the field is bounded near zero. By continuity
of the field the right side tends to $\ell(0,0)q(v)$, which is therefore zero. This
contradicts \eqref{eq:stresspos}.

The distance bound follows. The zero-set assertion follows from it, because $\mathcal A$ is
closed and $f$ vanishes on $\Lambda\times\mathcal A$.
\end{proof}

\subsection{A quartic identity for the four transverse spaces}
In the application the quadratic part is known through two quadratic maps $H$ and $T$.

Appendix~\ref{app:quadrics} fixes coordinates on the transverse spaces, a complex triple on
each:
\[
 u=(u_0,u_1,u_2,u_3)\in\mathbb C^{12},\qquad u_i=(u_{i0},u_{i1},u_{i2})\in\mathbb C^3 .
\]
Write $W_i$ also for the set where the other three triples vanish. Norms are Euclidean, and
$\langle x,y\rangle=\sum_a\overline{x_a}y_a$. The maps are
\[
 H=(H_0,\ldots,H_3),\quad T=(T_0,\ldots,T_3),\qquad
 H_i,T_i:\mathbb C^{12}\to\mathbb C^3 .
\]
A third map involves one $u_i$ at a time:
\[
 \sigma(u_i)=(u_{i1}u_{i2},\,u_{i2}u_{i0},\,u_{i0}u_{i1}),\qquad
 \sigma(u)=(\sigma(u_0),\ldots,\sigma(u_3)).
\]

\paragraph{The array.}
Arrange the twelve coordinates in four rows and three columns:
\begin{equation}\label{eq:array}
\begin{array}{c|ccc}
 &x_1&x_2&x_3\\\hline
 u_0&u_{00}&u_{02}&u_{01}\\
 u_1&u_{10}&u_{11}&u_{12}\\
 u_2&u_{21}&u_{22}&u_{20}\\
 u_3&u_{32}&u_{30}&u_{31}
\end{array}
\end{equation}
Row $i$ holds the entries of $u_i$, in the order shown. The columns are three vectors
$x_1,x_2,x_3$ in $\mathbb C^4$, with entries $x_{r,i}$. Each monomial of $\sigma$
multiplies two entries of one row; each monomial of $H$ multiplies two entries, or their
conjugates, from different rows and different columns; each monomial of $T$, two entries from
different rows of one column.

\begin{lemma}[Quartic identity]\label{lem:array}
For all\leannote{quartic identity}{Proofs/BookHTQuartic.lean}{78} $u\in\mathbb C^{12}$,
\begin{equation}\label{eq:quartic}
 \sum_{i<j}\|u_i\|^2\|u_j\|^2
 =\sum_i\|H_i(u)\|^2+\tfrac12\sum_i\|T_i(u)\|^2
   +3\operatorname{Re}\sum_i\langle\sigma(u_i),H_i(u)\rangle.
\end{equation}
\end{lemma}

\begin{proof}
The formal development proves \eqref{eq:quartic} by direct expansion: the left side has $54$
monomials, and every other monomial on the right cancels.

The identity also follows from three others, which were verified by expanding both sides in
computer algebra, with $H$ and $T$ as printed in Appendix~\ref{app:quadrics}, and are not
formalized:
\begin{align}
 \|\sigma(u)+H(u)\|^2&=\sum_{r<s}\|x_r\|^2\|x_s\|^2,\label{eq:composition}\\
 \tfrac12\|T(u)\|^2+\operatorname{Re}\sum_i\langle\sigma(u_i),H_i(u)\rangle
   &=\sum_r\sum_{i<j}|x_{r,i}|^2|x_{r,j}|^2,\label{eq:second}\\
 \sum_{i<j}\|u_i\|^2\|u_j\|^2
   &=\sum_{r<s}\|x_r\|^2\|x_s\|^2-\|\sigma(u)\|^2\notag\\
   &\qquad+\sum_r\sum_{i<j}|x_{r,i}|^2|x_{r,j}|^2.\label{eq:counting}
\end{align}
Expanding the square in \eqref{eq:composition} and substituting it and \eqref{eq:second} in
\eqref{eq:counting} gives \eqref{eq:quartic}. Identity \eqref{eq:composition} is the
multiplicativity of the octonion norm; the details are in Appendix~\ref{app:array-proof}.
\end{proof}

\paragraph{Positivity.}
Let $w$ lie in $W_i$ and $n$ in its orthogonal complement, where row $i$ is zero, and
suppose that both polar terms vanish:
\[
 H(w+n)-H(w)-H(n)=0,\qquad T(w+n)-T(w)-T(n)=0.
\]
Both maps vanish at $w$, so they take the same values at $w+n$ and at $n$, and these two
points differ only in row $i$. Subtract \eqref{eq:quartic} at the second point from
\eqref{eq:quartic} at the first. All terms on the right cancel except the pairing with
$\sigma(w_i)$. Thus
\begin{equation}\label{eq:kernelstress}
 3\operatorname{Re}\langle\sigma(w_i),H_i(n)\rangle
 =\|w_i\|^2\sum_j\|n_j\|^2.
\end{equation}

\subsection{Applying the criterion to the frame equations}
Write $P=P(\xi)$. The residual $F$ is a polynomial map of degree two. Let $\mathcal Q$ be its
homogeneous quadratic part and $\mathcal B$ the polar form of $\mathcal Q$. For every
configuration $x$ and every $v\in J^{39}$,
\[
 F(x+v)=F(x)+DF_xv+\mathcal Q(v),\qquad DF_{x+v}=DF_x+2\mathcal B(v,\cdot\,).
\]
In particular
\begin{equation}\label{eq:exact-quadratic}
 F(P+v)=DF_Pv+\mathcal Q(v).
\end{equation}
For an automorphism $g$ of $J$, let $\rho_g$ act by $g$ on the idempotency and frame-sum
residuals and trivially on the scalar trace and overlap residuals. Then $F(gx)=\rho_gF(x)$
for every configuration $x$. For a derivation $\delta$ of $J$ write $\rho_\delta$ for the
derivative of $g\mapsto\rho_g$ at the identity in the direction $\delta$.

\begin{definition}[Stress and its energy]\label{def:stress}
Let $x$ be a zero of $F$. A \emph{stress} at $x$ is a linear functional $\ell$ on the
residual space with $\ell\,DF_x=0$. Its \emph{energy} is the function $E_\ell=\ell\circ F$ on
$J^{39}$.
\end{definition}
These are the equilibrium stresses, or self-stresses, of rigidity theory
(Definition~2.3.1 of Connelly and Whiteley\cite{CW96}), with the frame equations in the place of the edge-length
equations of a framework.

\begin{lemma}[Calculus of stresses]\label{lem:stress-calculus}
Let $\ell$ be a stress at a zero $x$ of $F$.
\begin{enumerate}
\item[\textup{(a)}] $E_\ell(x+v)=\ell\mathcal Q(v)$ for every $v$.
\item[\textup{(b)}] If $v\in\ker DF_x$ and $\delta$ is a derivation of $J$, then
$\ell\mathcal B(v,\delta x)=0$. Hence adding an orbit velocity $\delta x$ to such a $v$ does
not change $\ell\mathcal Q(v)$.
\item[\textup{(c)}] For $g\in F_4$ the functional $\ell\circ\rho_g^{-1}$ is a stress at $gx$.
If $x'$ is a zero of $F$ and $\ell\mathcal B(x'-x,\cdot\,)=0$, then $\ell$ is a stress at $x'$.
\item[\textup{(d)}] If $v$ is the velocity at $x$ of a $C^2$ curve of zeros of $F$, then
$\ell\mathcal Q(v)=0$. Hence $\ell\mathcal B(v,v')=0$ for any two vectors $v$, $v'$ tangent at $x$ to
one submanifold consisting of zeros of $F$.
\end{enumerate}
\end{lemma}
The proof is in Appendix~\ref{app:calculus}.

\paragraph{The machine-checked identities at $P$.}
For quartet $i$, let $P'_i(g,h,d)$ be the code \eqref{eq:anchored-family}, and let $\mathfrak n_i(u_i)$
be the matrix in $\mathfrak{su}(3)$ with zero diagonal whose off-diagonal coordinates are
those of row $i$ of the table of signed coordinates in Appendix~\ref{app:normalization}. Then
$V_\xi u$ \leannote{transverse normalization}{Proofs/HTPhaseCompleteDirectionFamily.lean}{67}is the sum of four velocities of simultaneous conjugation, one in the family of each
quartet:
\[
 V_\xi u=\sum_{i=0}^{3}\frac{d}{dt}\bigg|_{t=0}
 P'_i\bigl(e^{t\mathfrak n_i(u_i)},\,e^{t\mathfrak n_i(u_i)},\,d_i(\xi)\bigr),\qquad u\in\mathbb C^{12}.
\]
It is a first-order deformation of $P$ at every parameter. The velocity in the right parameter $h$ is an orbit
velocity (Lemma~\ref{lem:families}(a)), so taking $h=g$ rather than $h=I$ changes neither the
projection of $V_\xi u$ to $\mathcal O^\perp$ nor, by Lemma~\ref{lem:stress-calculus}(b), any
energy of a stress at $P$. At nonresonant parameters this projection identifies the four complex
triples $u_i$ with the four transverse spaces $W_i$ of Proposition~\ref{prop:kernel}
(Appendix~\ref{app:normalization}).
\begin{proposition}[Finite identities]\label{prop:finite}
\leannote{Hessian identities}{Proofs/HTPhaseCompleteHPhase.lean}{338}For every $\xi\in(S^1)^4$ there are twelve complex covectors
$h_{ia}$ and twelve $t_{ia}$ on the residual space $\mathbb R^{2184}$
\textup{(}$0\le i\le3$, $0\le a\le2$\textup{)}, specified in Appendix~\ref{app:quadrics}, such that
\begin{align}
 h_{ia}DF_P=t_{ia}DF_P&=0,\label{eq:equilibrium}\\
 h_{ia}\mathcal Q(V_\xi u)=H_i(u)_a,\qquad
 t_{ia}\mathcal Q(V_\xi u)&=T_i(u)_a\label{eq:reproduction}
\end{align}
for all $u\in\mathbb C^{12}$, and such that $h_{ia}\mathcal Q$ is supported on
the twelve points of quartet $i$: it depends on no other coordinates.
\end{proposition}
By \eqref{eq:equilibrium} the real and imaginary parts of these covectors are stresses at
$P$. The proposition does not determine the covectors. The three points of
frame~$0$ do not move in $V_\xi u$, so any covector on the idempotency equations of one of them
that annihilates their linearization may be added to each of the twenty-four; for each of the
three points these covectors form a space of dimension sixteen. The ancillary file
\texttt{native-data.json} \textup{(}Appendix~\ref{app:quadrics}\textup{)} gives one choice, with
coefficients in $\mathbb Q(\sqrt{-1},\sqrt3)$: each $t_{ia}$ with entries that are Laurent
polynomials in $\xi$, and each $h_{ia}$ at one parameter $\xi_*$, whose coordinates lie in
$\mathbb Q(\sqrt{-1})$, carried to every $\xi$ by a diagonal automorphism of $J$. In this choice
each $h_{ia}$ gives weight only to equations among the twelve points of quartet~$i$: their
idempotency equations, the frame-sum equations of its four frames, and the overlaps of points in
two different frames of the quartet. Each $t_{ia}$ gives weight only to the same kinds of
equation among the twenty-seven points outside quartet~$i$, with overlaps only between frames in
different lobes. The identities were verified by exact computation as part of the formal
development (Section~\ref{sec:verification}); Appendix~\ref{app:quadrics} lists the checks and
describes the coefficient file.

\paragraph{Stresses along each family.}
By the support condition of Proposition~\ref{prop:finite}, $h_{ia}\mathcal B(v,\cdot\,)$
vanishes whenever the components of $v$ at the twelve points of quartet $i$ vanish. Let $P'$
be a code of the form \eqref{eq:anchored-family} for this quartet. It is a zero of $F$ with
the same twelve points as $P$, so $h_{ia}$ is a stress at $P'$ by
Lemma~\ref{lem:stress-calculus}(c).

The points of $M_i$ are the slice representatives of such codes
(Lemma~\ref{lem:families}(a)). The point with parameter $p$ (a parameter of the family, not a
point of $\mathbb OP^2$) is $g(p)^{-1}P'(p)$, where $P'(p)$ has the form
\eqref{eq:anchored-family} and $g(p)\in F_4$ depends analytically on $p$
(Lemma~\ref{lem:slice}). By Lemma~\ref{lem:stress-calculus}(c) again,
\[
 h_{ia}(p)=h_{ia}\circ\rho_{g(p)}
\]
is a stress at that point. This \leannote{along-family field}{Proofs/NativePhaseAlongSheetH.lean}{165}is an analytic field of stresses along the family, equal to $h_{ia}$ at $P$.

\paragraph{Reduction to the kernel coordinates.}
In Lemma~\ref{lem:stress} take $\Lambda=\mathbb R^4$, the space of $\lambda$, $E=\mathbb C^{12}$
and $\mathcal R=\mathbb R^{2184}$, the residual space.

\begin{lemma}[The reduced equations]\label{lem:reduction}
At a nonresonant parameter, the chart of Proposition~\ref{prop:simultaneous} can be chosen
so that its transverse coordinates are those of \eqref{eq:array}, with the norm of
$\mathbb C^{12}$ on $E=\bigoplus_iW_i$. There is then an analytic map $b$ into $\mathcal O^\perp$, defined near zero in $\Lambda\times E$ and
zero at the origin, for which the map
\[
 f(\lambda,u)=F(P+b(\lambda,u)),
\]
with all residual rows retained, has three properties.
\begin{enumerate}
\item[\textup{(i)}] The \leannote{Lyapunov--Schmidt reduction}{Proofs/NativePhaseRangeReduction.lean}{163}zeros of $F$ near $P$ in the slice are exactly the points $P+b(\lambda,u)$ at which $f$
vanishes.
\item[\textup{(ii)}] For $u\in W_i$, the point $P+b(\lambda,u)$ is the point of $M_i$ with
coordinates $(\lambda,u)$; so $f$ vanishes on $\Lambda\times\bigcup_iW_i$.
\item[\textup{(iii)}] $D_ub(0)=\Pi V_\xi$, where $\Pi$ is the orthogonal projection onto
$\mathcal O^\perp$.
\end{enumerate}
\end{lemma}
The proof is a Lyapunov--Schmidt reduction, given in Appendix~\ref{app:reduction}.

\begin{lemma}[Reduced identities]\label{lem:reduced}
Put $q_f(u)=\tfrac12D^2f(0)[(0,u),(0,u)]$. Then
\[
 h_{ia}q_f(u)=H_i(u)_a,\qquad t_{ia}q_f(u)=T_i(u)_a,
\]
and the zero set of $q_f$ is the union of the four transverse spaces.
\end{lemma}
\begin{proof}
By Lemma~\ref{lem:stress-calculus}(a), $h_{ia}f(\lambda,u)=h_{ia}\mathcal Q(b(\lambda,u))$
exactly. By Lemma~\ref{lem:reduction}(iii), and since $b$ vanishes at the origin, the part of
second order in $u$ at $\lambda=0$ is
\[
 h_{ia}q_f(u)=h_{ia}\mathcal Q(\Pi V_\xi u)=h_{ia}\mathcal Q(V_\xi u)=H_i(u)_a .
\]
The second equality is Lemma~\ref{lem:stress-calculus}(b): the vector $V_\xi u$ lies in
$\ker DF_P$, and its projection differs from it by an orbit velocity. The third is
\eqref{eq:reproduction}. The same argument applies to $t_{ia}$.

The form $q_f$ vanishes on the four transverse spaces because $f$ does
(Lemma~\ref{lem:reduction}(ii)). Conversely, where $q_f$ vanishes so do $H$ and $T$, and
\eqref{eq:quartic} leaves at most one $u_i$ nonzero.
\end{proof}

\begin{proposition}[No further solutions]\label{prop:exhaustion}
At every nonresonant parameter, the real zero set of the frame equations in a
sufficiently small neighborhood of $P(\xi)$ in the slice $S$ is exactly the
union of the four families $M_i$.
In the reduced coordinates,\leannote{stress criterion}{Proofs/NativePhaseEuclideanCriterion.lean}{194}
for some $c>0$ and all $(\lambda,u)$ near zero,
\[
 \operatorname{dist}\bigl(u,\textstyle\bigcup_iW_i\bigr)^2\le c\|f(\lambda,u)\|.
\]
\end{proposition}
\begin{proof}
We check the hypotheses of Lemma~\ref{lem:stress} for the map $f$ of
Lemma~\ref{lem:reduction}. Conditions \textup{(S1)} and \textup{(S2)} hold by that lemma, and
\textup{(S3)} is Lemma~\ref{lem:reduced}.

For the stresses, fix $i$ and a unit vector $w\in W_i$. By Lemma~\ref{lem:reduction}(ii) the
point $P+b(\lambda,u)$ with $u\in W_i$ lies in $M_i$; let $p$ be its parameter and take the
real field
\[
 \ell_{i,w}(p)=3\operatorname{Re}\sum_{a=0}^2
       \overline{\sigma(w_i)_a}\,h_{ia}(p),
\]
with $h_{ia}(p)$ the field along the family constructed above. It is continuous and a stress
at that point. By the chain rule $Df=DF\circ Db$ it annihilates the derivative of $f$ there,
which gives \eqref{eq:alongstress}.

Let $v\in W_i^\perp$ satisfy $\beta_f(w,v)=0$, where $\beta_f$ is the polar form of $q_f$.
Then both polar terms of $H$ and $T$ vanish at this pair, by Lemma~\ref{lem:reduced}, so
\eqref{eq:kernelstress} applies with $n=v$. Since $w_i$ is a unit vector, it gives
\[
 \ell_{i,w}(0)q_f(v)=3\operatorname{Re}\langle\sigma(w_i),H_i(v)\rangle=\|v\|^2,
\]
which is \eqref{eq:stresspos}.

Lemma~\ref{lem:stress} therefore gives the bound and shows that $f$ vanishes near
zero only where $u$ lies in one of the transverse spaces. By Lemma~\ref{lem:reduction}(i)
the zeros of $F$ near $P$ in the slice are then the points $P+b(\lambda,u)$ with such $u$,
and by Lemma~\ref{lem:reduction}(ii) these are the points of the four families.
\end{proof}

\begin{proof}[Proof of Theorem~\ref{thm:real}]
In the coordinates of Proposition~\ref{prop:simultaneous} each family is a coordinate
subspace. So by Proposition~\ref{prop:exhaustion} the zero set of $F$ in a small slice is a
neighborhood of the origin in $\mathbb R^4\times\bigcup_i\mathbb R^6_i\times\{0\}$, the model
\eqref{eq:axes}, with the families as branches. Their common part, where $u$ and $\eta$
vanish, is the family $M_*$ of Lemma~\ref{lem:families}(b), the slice image of the
four-parameter family.
\end{proof}
The constants and neighborhoods may depend on $\xi$.