\section{A sharp bound on distance to the solution set}\label{sec:quantitative}
This section proves Theorem~\ref{thm:bound}. Part~(a) is the bound of
Proposition~\ref{prop:exhaustion} in the slice, carried to a neighborhood of the orbit by
Lemma~\ref{lem:slice}. Fix a nonresonant $\xi$ and write $P=P(\xi)$. Distances in $J^{39}$
are measured in the norm of the trace form, for which $F_4$ acts by isometries.

\subsection{The bound near the orbit}

\paragraph{In the slice.}
Let $s$ be a point of the slice near $P$, with coordinates $(\lambda,u,\eta)$ in the chart of
Proposition~\ref{prop:simultaneous}, and let $s'=P+b(\lambda,u)$ have the same $(\lambda,u)$.
The Lyapunov--Schmidt reduction (Appendix~\ref{app:reduction}) replaces the last coordinate
by one that vanishes exactly at such points $s'$, the component of $F(s)$ in the image of
$DF_P$.
This change of coordinates and $F$ are locally Lipschitz, so for some constant $c$
\[
 \|s-s'\|\le c\|F(s)\|,\qquad
 \|F(s')\|\le c\|F(s)\|.
\]
By definition $F(s')=f(\lambda,u)$. A point $u'$ of $\bigcup_iW_i$ nearest to $u$ is an
orthogonal projection of it, so no farther from the origin, and $P+b(\lambda,u')$ lies in a
family, hence in $\mathcal Z$. Since $b$ is locally Lipschitz, the reduced bound of
Proposition~\ref{prop:exhaustion} gives a constant $c'$ with
\[
 \operatorname{dist}(s',\mathcal Z)^2\le c'\|F(s')\|.
\]
For $s$ so close to $P$ that $\|F(s)\|\le1$, the two combine:
\[
 \operatorname{dist}(s,\mathcal Z)^2
 \le2\|s-s'\|^2+2\operatorname{dist}(s',\mathcal Z)^2
 \le(2c^2+2cc')\,\|F(s)\|.
\]

\paragraph{The whole orbit.}
Choose $\varepsilon$ in Lemma~\ref{lem:slice} so small that this estimate holds on $S_\varepsilon$
and that the zeros of $F$ there are the points of the four families
(Proposition~\ref{prop:exhaustion}). Let $U_\xi$ be the tube $U_\varepsilon=F_4S_\varepsilon$, an
open neighborhood of the orbit. Every point of the tube is $y=gs$ with $g\in F_4$ and
$s\in S_\varepsilon$. The isometry $g$ preserves the zero set, and $F(gs)=\rho_gF(s)$ by the
equivariance of Section~\ref{sec:exhaustion}, so
\[
 \operatorname{dist}(y,\mathcal Z)=\operatorname{dist}(s,\mathcal Z),\qquad
 \|F(s)\|\le c''\|F(y)\|.
\]
Here $c''$ bounds the operator norms of the $\rho_g^{-1}$; it is finite because $F_4$ is
compact. Hence
\[
 \operatorname{dist}(y,\mathcal Z)^2\le C_\xi\|F(y)\|\quad(y\in U_\xi),
 \qquad C_\xi=(2c^2+2cc')\,c''.
\]

An $F_4$-invariant subset of the tube is $F_4$ times its part in the slice
(Lemma~\ref{lem:slice}(b)). For the zeros in the tube that part is the union of the four
families in $S_\varepsilon$, by the choice of $\varepsilon$. Therefore
\[
 \mathcal Z\cap U_\xi
 =F_4\bigl((M_0\cup\cdots\cup M_3)\cap S_\varepsilon\bigr)
 \subset F_4(M_0\cup\cdots\cup M_3)\cap U_\xi
 \subset\mathcal Z\cap U_\xi .
\]
The last inclusion holds because the families consist of zeros and $\mathcal Z$ is invariant.
This proves part~(a). The formal statement has the union of the families in place of the zero
set; that form, and its equivalence with part~(a), is item~(1) of
Section~\ref{sec:verification}.

\subsection{Optimality of the square-root exponent}

\begin{lemma}[Kernel larger than the tangent cone]\label{lem:cone-sharp}
Let $G$ be a $C^2$ map between finite-dimensional normed spaces with $G(p)=0$, and let
$v\in\ker DG_p$. Suppose that $v$ is not in the tangent cone of $G^{-1}(0)$ at $p$: it is not a
limit of vectors $(x_k-p)/t_k$ with $G(x_k)=0$ and $t_k\downarrow0$. Then there is $c>0$ such
that, for all small $t>0$,
\[
 \operatorname{dist}\bigl(p+tv,G^{-1}(0)\bigr)\ge ct,\qquad\text{whereas}\qquad
 \|G(p+tv)\|=O(t^2).
\]
In particular no bound
$\operatorname{dist}(y,G^{-1}(0))\le C\|G(y)\|^\alpha$ with $\alpha>1/2$ holds on a neighborhood
of $p$.
\end{lemma}
\begin{proof}
If there were no such $c$, the distance would be $o(t_k)$ along some sequence
$t_k\downarrow0$. Zeros $x_k$ of $G$ with $\|x_k-p-t_kv\|=o(t_k)$ would then satisfy
$(x_k-p)/t_k\to v$, against the hypothesis. The second estimate is Taylor's formula, since $G(p)=0$ and
$DG_pv=0$. A bound with exponent $\alpha$ would give $ct\le C't^{2\alpha}$ for all small
$t>0$, which is impossible when $2\alpha>1$.
\end{proof}

\paragraph{The witness.}
For the frame equations, let every $u_i$ be $(1,1,1)$ and put $v=V_\xi u$, a sum of
velocities of the four families and so a first-order deformation. Let $h=h_{00}$. It is a complex-valued stress at
$P$ by \eqref{eq:equilibrium}, and its energy
\textup{(}Definition~\ref{def:stress}\textup{)} is given by
Lemma~\ref{lem:stress-calculus}(a):
\[
 E_h(P+w)=h\mathcal Q(w).
\]
The energy vanishes at every point of $\mathcal Z$, whereas $E_h(P+v)=H_0(u)_0=1$, by
\eqref{eq:reproduction} and the formula for $H_0$ in Appendix~\ref{app:quadrics}. The form
$h\mathcal Q$ is continuous, so it has no zero in some ball of radius $c>0$ about $v$; it is
homogeneous, so it has none in the ball of radius $ct$ about $tv$. Hence
\leannote{sharpness witness}{Proofs/NativePhaseSharpness.lean}{99}
\[
 \operatorname{dist}(P+tv,\Sigma)\ge ct\quad(t>0)
\]
for every nonempty $\Sigma\subset\mathcal Z$. In particular $v$ is not in the tangent cone of
$\mathcal Z$ at $P$, and Lemma~\ref{lem:cone-sharp}, applied to $F$ at $P$, gives part~(b).

The same inequality excludes an exponent above $1/2$ for the distance to any
nonempty subset of the zero set. Lemma~\ref{lem:cone-sharp} applies equally to any $C^2$ map
vanishing exactly on $\mathcal Z$ near $P$, since its derivative at $P$ vanishes on the orbit
tangent space and on the tangent spaces of the families, which together span $\mathcal T$
(Proposition~\ref{prop:kernel}, Lemma~\ref{lem:families}(c)).

The witness can be moved onto configurations whose thirteen triples are Jordan frames. On
them only the overlaps between distinct frames can fail. Fix a frame $r$. If it lies in quartet $i$, the family of quartet $i$ does not move it.
Otherwise, in the coordinates of quartet $i$, frame $r$ is the orbit of $\theta_i$ on a point
$p(U)$ (Lemma~\ref{lem:dictionary}), and with $N=\mathfrak n_i(u_i)$ the family moves it by right
multiplication with $U^*e^{tN}Ue^{-tN}$. This is an automorphism of $J$ by
Lemma~\ref{lem:stabilizer}; let $\delta_{i,r}$ be its derivative at $t=0$, a derivation. With
$\delta_r$ the sum of the $\delta_{i,r}$ over the families that move frame $r$, the component of
$v$ at frame $r$ is $\delta_r$ applied to the points of that frame. Let $\gamma(t)$ have frame $r$ equal to
$\exp(t\delta_r)$ applied to frame $r$ of $P$. Its triples are Jordan frames, and
$\gamma(t)=P+tv+O(t^2)$. Since $DF_Pv=0$, $\|F(\gamma(t))\|=O(t^2)$, while
$\operatorname{dist}(\gamma(t),\mathcal Z)\ge ct-O(t^2)$. So no exponent above $1/2$ is
possible even on configurations whose triples are Jordan frames. This consequence is proved
here only; it is not part of the formal development.