\section{Open patches in the unlabeled space \texorpdfstring{$\mathcal M$}{M}}\label{sec:quotient}
This section proves Theorem~\ref{thm:patches} and Corollary~\ref{cor:no24}. Only nonresonant members of
the family enter, so the germ of $\mathcal M$ at the original code is not determined.

\subsection{Open patches modulo \texorpdfstring{$F_4$}{F4}}
The canonical partition \leannote{code/frame topology}{Proofs/TCStable.lean}{93}of a tight code into
thirteen frames is locally constant by Lemma~\ref{lem:partition}, so the zero set $\mathcal Z$
of $F$ is open in $\mathcal C$ (Section~\ref{sec:codes}). It is $F_4$-invariant, so its
quotient $\mathcal Z/F_4$ is open in $Y$.

Now fix $\xi$, and let $S_\varepsilon$ and $U_\varepsilon$ be the slice and the tube of
Lemma~\ref{lem:slice} at $P(\xi)$. \leannote{open labeled slice}{Proofs/GSQuot.lean}{75}By part~(b) of that lemma, applied to the zeros in the tube,
sending a point to its orbit is a
homeomorphism from the zero set $\mathcal Z\cap S_\varepsilon$ in the slice onto
$(\mathcal Z\cap U_\varepsilon)/F_4$. The latter is open in $\mathcal Z/F_4$ and hence in $Y$.

Let $\xi$ be nonresonant. In the model \eqref{eq:axes} the set
$\mathbb R^4\times(W_i\setminus\{0\})$ is open, because its complement, the union of the other
three branches, is closed; it is a ten-dimensional manifold, and the origin
lies in its closure. By Theorem~\ref{thm:real} and the homeomorphism just described, every
neighborhood of the class of $P(\xi)$ in $Y$ contains a nonempty open subset of $Y$
homeomorphic to an open subset of $\mathbb R^{10}$.

\subsection{Passing to the unlabeled quotient}
The symmetric group $\Gamma=\mathfrak S_{39}$ acts on $Y$ by homeomorphisms,
and $Y/\Gamma=\mathcal M$. It need not preserve $\mathcal Z/F_4$, since permuting points can
change the chosen frame partition.

\begin{lemma}[Quotient by a finite group]\label{lem:finite-patch}
Let a finite group $\Gamma$ act by homeomorphisms on a Hausdorff space $Y$, with quotient map
$q\colon Y\to Y/\Gamma$, and write $\Gamma_y$ for the stabilizer of $y$.
\begin{enumerate}
\item[\textup{(a)}] Every $y\in Y$ has an open neighborhood $\Omega_y$ with
$\gamma \Omega_y\cap \Omega_y=\varnothing$ for all $\gamma\notin\Gamma_y$. In particular the stabilizer
of every point of $\Omega_y$ is contained in $\Gamma_y$.
\item[\textup{(b)}] Let $\Omega$ be an open subset of $\Omega_y$ all of whose points have stabilizer
$\Gamma_y$. Then $q$ restricts to a homeomorphism from $\Omega$ onto an open subset of $Y/\Gamma$.
\item[\textup{(c)}] If $\Omega\subset Y$ is a nonempty open set locally homeomorphic to
$\mathbb R^n$, then its image in $Y/\Gamma$ contains a nonempty open
subset homeomorphic to a nonempty open subset of $\mathbb R^n$.
\end{enumerate}
\end{lemma}
\begin{proof}
(a) For each $\gamma\notin\Gamma_y$ choose disjoint open sets $\Omega'_\gamma\ni y$ and
$\Omega''_\gamma\ni\gamma y$. Let $\Omega_y$ be the intersection of the finitely many sets
$\Omega'_\gamma\cap\gamma^{-1}\Omega''_\gamma$. Then $\Omega_y\subset \Omega'_\gamma$ and
$\gamma \Omega_y\subset \Omega''_\gamma$ are disjoint. An element fixing a point $z$ of $\Omega_y$ does not move
$\Omega_y$ off itself, so it lies in $\Gamma_y$.

(b) The elements of $\Gamma_y$ fix $\Omega$ pointwise, and the others move it off itself, so
$q$ is injective on $\Omega$. The image of an open subset $\Omega'$ of $\Omega$ is open, because its preimage
$\bigcup_{\gamma\in\Gamma}\gamma \Omega'$ is open. Thus the restriction is an open continuous
injection.

(c) Choose $y\in \Omega$ whose stabilizer has the least order among points of $\Omega$. By (a) the
stabilizers of the points of $\Omega\cap \Omega_y$ are subgroups of $\Gamma_y$, and by minimality they equal
$\Gamma_y$. Apply (b) to a coordinate ball about $y$ in
$\Omega\cap \Omega_y$.
\end{proof}

The space $Y$ is Hausdorff because $F_4$ is compact: its quotient topology is induced by the
metric
\[
 d_Y([x],[x'])=\min_{g\in F_4}\|x-gx'\|
\]
in the norm of the trace form. As in the lemma, $q\colon Y\to\mathcal M$ is the quotient map.

\begin{proposition}\label{prop:unlabelled-patch}
Let $\xi$ be nonresonant. Every open neighborhood $\Omega$ of the class of $P(\xi)$ in $\mathcal M$ contains a
nonempty open subset of $\mathcal M$ homeomorphic to a nonempty open subset of $\mathbb R^{10}$.
\end{proposition}
\begin{proof}
The open set $q^{-1}(\Omega)\ni[P(\xi)]$ contains, by the end of the previous subsection, a nonempty
open subset $\Omega'$ of $Y$ homeomorphic to an open subset of $\mathbb R^{10}$.
Lemma~\ref{lem:finite-patch}(c), applied to $\Omega'$, gives the required subset of $\mathcal M$ inside
$q(\Omega')\subset \Omega$.
\end{proof}

\begin{remark}[The unlabeled germ]\label{rem:aut}
Let $\operatorname{Aut}(P)\subset F_4$ be the group of automorphisms of $J$ that permute the
points of $P=P(\xi)$; it contains $K$. For $h\in\operatorname{Aut}(P)$ let
$\sigma_h\in\mathfrak S_{39}$ be the relabeling with $\sigma_hhP=P$, and let $\tilde h=\sigma_hh$:
it applies $h$ to each point and then restores the labels of $P$, as in Lemma~\ref{lem:K}(c). The map
$h\mapsto\sigma_h$ is a homomorphism onto the stabilizer $\Gamma_y$ of $y=[P]$ in
$\mathfrak S_{39}$: if $\sigma P=gP$ with $g\in F_4$, then $g^{-1}$ permutes the points of $P$ and
$\sigma=\sigma_{g^{-1}}$. It is injective because only the identity fixes every point
\textup{(}Lemma~\ref{lem:orbit}\textup{)}, so $\operatorname{Aut}(P)$ is finite.

Since $h$ preserves overlaps, $\sigma_h$ maps frames to frames, so $\sigma_h$ and $\tilde h$
preserve $\mathcal Z$. The map $\tilde h$ is orthogonal, fixes $P$ and satisfies
$\tilde h(gx)=(hgh^{-1})\tilde hx$ for $g\in F_4$. Hence it preserves $\mathcal O$,
$\mathcal O^\perp$, $S_\varepsilon$ and $U_\varepsilon=F_4S_\varepsilon$, and
$\operatorname{Aut}(P)$ acts on $\mathcal Z\cap S_\varepsilon$. The maps $\tilde h$ and $\sigma_h$
induce the same map of $Y$, so the homeomorphism $s\mapsto[s]$ from $\mathcal Z\cap S_\varepsilon$
onto $V=(\mathcal Z\cap U_\varepsilon)/F_4$ carries $\tilde h$ to $\sigma_h$.

Let $\Omega$ be the intersection of the sets $\gamma(\Omega_y\cap V)$ with $\gamma\in\Gamma_y$, where $\Omega_y$ is
as in Lemma~\ref{lem:finite-patch}(a). It is a $\Gamma_y$-invariant open neighborhood of $y$, and
every $\gamma\notin\Gamma_y$ moves it off itself. So $q$ induces a continuous injection of
$\Omega/\Gamma_y$ into $\mathcal M$, which is open by the argument for part~(b) of that lemma. Thus a
neighborhood of the class of $P$ in $\mathcal M$ is homeomorphic to the quotient by
$\operatorname{Aut}(P)$ of an invariant open neighborhood of $P$ in $\mathcal Z\cap S_\varepsilon$.
For nonresonant $\xi$ this is, by Theorem~\ref{thm:real}, a neighborhood of the origin in the
model \eqref{eq:axes} modulo an action of $\operatorname{Aut}(P)$ by homeomorphisms fixing the
origin. We determine neither the group nor the action.

Modulo $F_4$ and relabeling, each member of $M_i$ is quartet~$0$ together with the nine frames of
$kE_{ab}(d)k^*$, where $k\in SU(3)$ is a scalar multiple of $G_i^*gL_i$ (Appendix~\ref{app:coordinates}): conjugation by the diagonal
matrix $G_i^*$ in the coordinates of quartet $i$ is an automorphism of $J$ taking that quartet to
quartet~$0$ (Appendix~\ref{app:inclusion} and \eqref{eq:anchorbinding}), and Lemma~\ref{lem:stabilizer} removes the right
factor. So, for nonresonant $\xi$, near the class of $P(\xi)$ in $\mathcal M$ the four families are four pieces of the image
of the one map of Lemma~\ref{lem:embedded}, near the four points $([G_i^*L_i],d_i(\xi))$ of
$PSU(3)\times T^2$, and by Theorem~\ref{thm:real} they make up all of $\mathcal M$ there. In $Y$ any
two of them meet only in the four-parameter family; whether they are identified further in
$\mathcal M$ depends on $\operatorname{Aut}(P)$. This remark is not part of the formal development.
\end{remark}

\subsection{Patches near the original code}
Nonresonant parameters approach $\xi=1$, since the resonant ones form a finite union of cosets
of closed subgroups of codimension one (Section~\ref{sec:families}).

By continuity of the configuration and quotient maps, every open neighborhood of $c_0$ contains
the class of such a member, and Proposition~\ref{prop:unlabelled-patch} at that parameter gives
the patch. This proves Theorem~\ref{thm:patches}.

\begin{proof}[Proof of Corollary~\ref{cor:no24}]
Let a neighborhood of $c_0$ in $\mathcal M$ be homeomorphic to an open subset of $\mathbb R^n$.
It contains an open neighborhood $\Omega$ of $c_0$, again
homeomorphic to an open subset of $\mathbb R^n$. By Theorem~\ref{thm:patches}, $\Omega$ contains a nonempty open
subset of $\mathcal M$ homeomorphic to an open subset of
$\mathbb R^{10}$. The image of that subset in the chart is open in $\mathbb R^n$, so
$n=10$ by invariance of dimension.
\end{proof}
The case $n=24$ is the
\href{https://github.com/macgregor-sudo/tight-39-code/blob/46f01c135aacea9003435e7f1dc99b4a69568e83/Proofs/NativeOriginalCodeNoManifold24.lean\#L37}{formally verified statement}.
In the labeled space $Y$ more is true: no neighborhood of $[P(1)]$ is
homeomorphic to an open subset of any $\mathbb R^n$. Such a neighborhood would contain the class of
a nonresonant $P(\xi)$ as an interior point. By Theorem~\ref{thm:real} and the slice homeomorphism
of the first subsection, $Y$ near that class is the model \eqref{eq:axes} near the origin. Write the model as
$\mathbb R^4\times C$, where $C$ is the union of four $6$-planes meeting only at the origin.
Since $C\setminus0$ is homotopy equivalent to four disjoint $5$-spheres, $H_*(C,C\setminus0)$ is
$\mathbb Z^3$ in degree $1$ and $\mathbb Z^4$ in degree $6$, and by the K\"unneth formula the local
homology of the model at the origin is $\mathbb Z^3$ in degree $5$ and $\mathbb Z^4$ in degree
$10$, which is not that of a manifold point. The argument does not apply to $\mathcal M$, whose germ there is the
model modulo the finite group of Remark~\ref{rem:aut}: a quotient of the model by a finite group
that permutes its branches can be a manifold.