\section{Formal verification and data}\label{sec:verification}
A development of the results in the Lean~4 theorem prover\cite{dMU21}, built on Mathlib\cite{Mathlib20}, is available at
\begin{center}\small\url{https://github.com/macgregor-sudo/tight-39-code}\end{center}
at revision \texttt{46f01c1}. It is registered as
\href{https://palomar-registry.org/entry?id=PALOMAR-2026-10-29-000034&version=1}{\texttt{PALOMAR-2026-10-29-000034}, version~1},
in the Palomar registry\cite{Palomar}. The registry's record for that revision reports
that the $29$ submitted theorems were accepted by the Lean kernel and,
independently, by the external checker NanoDa, with no axioms
beyond \texttt{propext}, \texttt{Quot.sound} and \texttt{Classical.choice}.
It includes a Comparator configuration listing the $29$ targets. A third checker, con-ron, was run
and stopped at its resource ceiling; no acceptance by it is claimed.
Registration is not acceptance by a human referee.

What was checked is stated in one file:
\texttt{Challenge.lean} ($993$ lines) imports only Mathlib and contains the $29$ statements with
every definition they use. The registry also checks that \texttt{Solution.lean}, which assembles the proofs in the directory \texttt{Proofs}
($956$ Lean files, about $151{,}000$ lines), states the same theorems with the same definitions.

The formal development uses the product of $J$, the frame equations, the
automorphism action and the quotient $\mathcal M$ as defined in this paper.
Its predicate \texttt{IsGoodPhase} says that no entry of the four triples
\eqref{eq:phase-triples} has cube one, which by Proposition~\ref{prop:kernel} is nonresonance.
The dimension formula \eqref{eq:fullkernel} that gives this equivalence is itself a registered
target, \texttt{finrank\_original\_derivative\_kernel}, at every $\xi$.

Table~\ref{tab:status} gives the status of every numbered theorem, proposition, lemma and
corollary. \emph{Registered} means that it is stated by one of the $29$ registered targets,
\emph{compiled} that a declaration of the development at the revision above states it but was
not submitted as a target, and \emph{text} that its proof is in this paper only. Where the
formal statement is narrower than the printed one, the last column says how.
\begin{table}[p]
\centering\scriptsize
\caption{Status of the numbered statements. Declarations are named without their namespaces.}\label{tab:status}
\begin{tabular}{@{}llp{3.7in}@{}}
\hline
Statement&Status&Lean declarations; difference from the printed statement\tabularnewline\hline
Thm.~\ref{thm:real}&registered&\raggedright\texttt{normal\_form\_exists}; \texttt{native\_A5\_geometry} for the common part\tabularnewline
Thm.~\ref{thm:bound}&registered&\raggedright\texttt{native\_real\_endpoint}; stated for $S_\xi$, item~(1) below\tabularnewline
Thm.~\ref{thm:patches}&compiled&\raggedright\texttt{originalCode\_has\_ten\_patches}; item~(2) below\tabularnewline
Cor.~\ref{cor:no24}&registered&\raggedright\texttt{originalCode\_no\_open24\_chart}, \texttt{originalCode\_no\_charted24\_neighborhood}; only $n=24$, the general case is text\tabularnewline
Lem.~\ref{lem:positive}&compiled&\raggedright\texttt{overlap\_nonneg}\tabularnewline
Prop.~\ref{prop:frames}&registered&\raggedright\texttt{code\_bound}, \texttt{code\_bound\_sharp}, \texttt{tight\_code\_iff\_frames}; uniqueness of the partition is compiled only (\texttt{tight\_code\_frames}), item~(3) below\tabularnewline
Lem.~\ref{lem:partition}&compiled&\raggedright\texttt{partition\_native\_nhds}\tabularnewline
Lem.~\ref{lem:span}&text&\tabularnewline
Lem.~\ref{lem:subalgebras}&text&\raggedright Appendix~\ref{app:subalgebras}\tabularnewline
Lem.~\ref{lem:dictionary}&registered&\raggedright(i) \texttt{native\_idempotent\_iff\_scaled\_specialUnitary\_\allowbreak of\_literal\_quartet\_readouts}, \texttt{nativeComplementaryPoint\_scaled\_hidden\_inverse}, \texttt{state\_equivalence}; (ii) \texttt{native\_complementary\_frame\_iff\_exists\_central\_order}; (iii) \texttt{native\_ordered\_central\_triples\_overlap\_iff\_\allowbreak hilbertSchmidt}; also \texttt{nine\_frame\_array}. Only for quartet~$0$ of $P$; the condition $p+\theta p+\theta^2p=e$ is not stated\tabularnewline
Lem.~\ref{lem:stabilizer}&registered&\raggedright\texttt{quartet\_fixer\_classification}, \texttt{quartet\_fixer\_converse}; only for quartet~$0$ of $P$\tabularnewline
Lem.~\ref{lem:embedded}&registered&\raggedright\texttt{full\_A2}; only for quartet~$0$ of $P$\tabularnewline
Lem.~\ref{lem:anchored}&text&\raggedright\texttt{native\_A5\_geometry} states, at nonresonant $\xi$, that the members with $h=I$, moved by automorphisms, are zeros of $F$\tabularnewline
Lem.~\ref{lem:fourier}&registered&\raggedright\texttt{unrestricted\_matrix\_normal\_form}, \texttt{firstOrder\_dimension}, \texttt{resonance\_count\_cases}\tabularnewline
Lem.~\ref{lem:K}&registered&\raggedright\texttt{full\_A4}: $\theta_0$ and $\theta_1$, of order three and commuting, their permutation table, and the action of $K$ on $\mathcal T$ and $\mathcal O$; the rest of (b) and (c) is text\tabularnewline
Lem.~\ref{lem:repK}&text&\tabularnewline
Lem.~\ref{lem:quartet}&text&\raggedright Appendix~\ref{app:quartet-proof}; the dimension $8$ is compiled for the standard quartet (\texttt{finrank\_quartetFirstOrder\_std})\tabularnewline
Lem.~\ref{lem:TH}&compiled&\raggedright\texttt{finrank\_anchorFixed}, the dimension only\tabularnewline
Lem.~\ref{lem:TK}&compiled&\raggedright\texttt{finrank\_commonFixed}\tabularnewline
Lem.~\ref{lem:orbit}&registered&\raggedright\texttt{full\_A4}: the three dimensions and injectivity of $\delta\mapsto\delta P$; triviality of the stabilizer is text\tabularnewline
Prop.~\ref{prop:kernel}&registered&\raggedright\texttt{finrank\_original\_derivative\_kernel} for \eqref{eq:fullkernel}; \texttt{full\_A4} for the action of $K$ on $\overline{\mathcal T}$; both at every $\xi$\tabularnewline
Lem.~\ref{lem:slice}&text&\raggedright Appendix~\ref{app:slice-proof}; \texttt{native\_A5\_geometry} gives, at nonresonant $\xi$, an analytic chart near $P$ and the open embedding of the slice zeros into $\mathcal Z/F_4$; the open embedding is compiled at every $\xi$ (\texttt{exists\_sliceToOrbit\_isOpenEmbedding})\tabularnewline
Lem.~\ref{lem:families}&registered&\raggedright\texttt{native\_A5\_geometry}, at nonresonant $\xi$ only: the two consequences listed in part~(a) and part~(b); the first sentence of (a) and part~(c) are text\tabularnewline
Prop.~\ref{prop:simultaneous}&registered&\raggedright\texttt{native\_A5\_geometry}\tabularnewline
Lem.~\ref{lem:stress}&registered&\raggedright\texttt{supported\_stress\_local\_criterion}\tabularnewline
Lem.~\ref{lem:array}&compiled&\raggedright\texttt{quartic\_identity\_values}; the three identities of its proof are computer algebra, not formalized\tabularnewline
Lem.~\ref{lem:stress-calculus}&text&\raggedright Appendix~\ref{app:calculus}\tabularnewline
Prop.~\ref{prop:finite}&compiled&\raggedright\texttt{H\_equilibrium}, \texttt{T\_equilibrium}, \texttt{H\_reproduction\_phase}, \texttt{T\_reproduction\_phase}; support: \texttt{hasAnchorSupport}\tabularnewline
Lem.~\ref{lem:reduction}&compiled&\raggedright part~(i): \texttt{originalF\_zero\_iff\_coordinates}; Appendix~\ref{app:reduction}\tabularnewline
Lem.~\ref{lem:reduced}&text&\tabularnewline
Prop.~\ref{prop:exhaustion}&compiled&\raggedright\texttt{local\_reduced\_bound}\tabularnewline
Lem.~\ref{lem:cone-sharp}&text&\tabularnewline
Lem.~\ref{lem:finite-patch}&text&\tabularnewline
Prop.~\ref{prop:unlabelled-patch}&text&\raggedright compiled on a dense subset of $\mathcal N$ (\texttt{native\_code\_ten\_patches})\tabularnewline
\hline
\end{tabular}
\end{table}

Three of the differences in Table~\ref{tab:status} need a comment.
\begin{enumerate}
\item[(1)] \emph{The distance bound.} For
nonresonant $\xi$ write $P=P(\xi)$, let $S_0$ be the union of suitable neighborhoods of $P$ in the four families, and
let $S_\xi=F_4S_0$. \texttt{native\_real\_endpoint} asserts that
\leannote{whole-orbit estimate}{Proofs/PairingR.lean}{23}some open neighborhood
$U$ of $F_4P$ and some constant $C$ satisfy
\begin{equation}\label{eq:whole-bound}
 \operatorname{dist}(y,S_\xi)^2\le C\|F(y)\|,\qquad
 F(y)=0\ \Longleftrightarrow\ y\in S_\xi\quad(y\in U),
\end{equation}
for both the coordinate norm and the norm of the trace form, and that every exponent
$\alpha>1/2$ fails for $S_\xi$. This form is equivalent to Theorem~\ref{thm:bound}. It implies part~(a) with $U_\xi=U$, since
$S_\xi\subset\mathcal Z$. Conversely, in the notation of Section~\ref{sec:quantitative}, for
$S_0=(M_0\cup\cdots\cup M_3)\cap S_\varepsilon$ the proof given there shows that
$\mathcal Z\cap U_\xi=S_\xi$. If the $2r$-neighborhood of the orbit lies in $U_\xi$ and $y$
is within $r$ of the orbit, the zeros within $r$ of $y$ include an orbit point and lie in
$U_\xi\cap\mathcal Z=S_\xi$; so $\operatorname{dist}(y,S_\xi)=\operatorname{dist}(y,\mathcal Z)$
and \eqref{eq:whole-bound} holds there with $C=C_\xi$. The lower
bound for an arbitrary nonempty $\Sigma\subset\mathcal Z$ is the compiled theorem
\texttt{native\_zero\_set\_lower\_bound}, which was not submitted as a separate target.
\item[(2)] \emph{The open patches.} The open-patch theorem is compiled, and the formal proof of
the registered corollary rests on the same statement, but it was not submitted
as a separate target.
\item[(3)] \emph{The frames.} The formal statement corresponding to
Proposition~\ref{prop:frames} asserts that a partition into frames exists and not that it is
unique.
\end{enumerate}

The formal proof of the open-patch theorem
\leannote{formal patch endpoint}{Proofs/NativeCodeTenPatches.lean}{63}uses a nonzero Jacobian minor and complex local isolation on
a dense subset of $\mathcal N$, where Section~\ref{sec:quotient} combines Theorem~\ref{thm:real}
with Lemma~\ref{lem:finite-patch}. The isolation rests on a bound for the Hilbert--Samuel
function of the complexified equations at $P(\xi)$, obtained from the stresses of
Proposition~\ref{prop:finite}. The formal route thus avoids Theorem~\ref{thm:real},
Lemma~\ref{lem:stress} and Proposition~\ref{prop:exhaustion}, but not Proposition~\ref{prop:finite}. The printed proof of
Lemma~\ref{lem:stress} obtains both of its limits from one expansion, where the formal proof
treats the two limits separately; the statement is the same. The formal check covers
the Lean statements, not the prose of this paper.

The finite identities of Appendix~\ref{app:quadrics} and the quartic identity
\eqref{eq:quartic} are part of the formal
development. The coefficients of the former are supplied with this paper as the ancillary
file \texttt{anc/native-data.json}, exported from the definitions at the
revision above. What was replayed from the file, and in what arithmetic, is stated at the end of
Appendix~\ref{app:quadrics}. The re-expressions of \eqref{eq:quartic} in the proof of Lemma~\ref{lem:array}, and the matrix form
\eqref{eq:Hmatrix} of the quadratic maps, were verified by computer algebra and are not formalized.

\paragraph{Acknowledgements.}
The formal development reuses or adapts Lean code by Bastiaan J.~Braams,
Akhil Mathew and Kai Lam, the fixed-point theorems of harfe, and smaller
excerpts from code by A.~Chernikov and by OpenAI and from the author's earlier
repositories; the
\href{https://github.com/macgregor-sudo/tight-39-code/blob/46f01c135aacea9003435e7f1dc99b4a69568e83/THIRD_PARTY_NOTICES.md}{third-party notices}
at the revision above record the sources, authors and licenses.

\paragraph{Use of AI.}
Except for attributed third-party material, all text and code of this work
was generated by AI systems under the author's direction: Anthropic's Claude
Fable~5.2 and OpenAI's Astra GPT~6. The work has not had independent human
peer review. The author is responsible for the work; AI systems are not
authors. Robert is an amateur who welcomes collaboration
(\href{mailto:macgregor@gmail.com}{macgregor@gmail.com}).