\section{The formal developments}\label{app:lean}

The existence statements of Theorems~\ref{thm:D} and~\ref{thm:A} have formal
counterparts in Lean~4 on top of Mathlib, with all dependencies pinned to fixed commits: the existence statement of
Theorem~\ref{thm:D}(i), for Fourier quasicrystals, in the development \cite{Mar26},
recorded in Palomar as \cite{PalStr}; and the existence statement of
Theorem~\ref{thm:A}(i), for all crystalline measures and without the symmetry of
$\Lambda$, in the development \cite{MS26}, recorded in Palomar as \cite{Pal26}. A Palomar record certifies that the formal proof of the statement of
record has been machine-checked; as the registry itself states, it does not certify
novelty, nor that the formal statement matches an informal one. We therefore record
the relevant data and describe each statement of record explicitly. According to
the two records, the proofs were rechecked during registration by the kernel
checkers \texttt{nanoda} and \texttt{con-ron}, and copies of the source and
dependency repositories at the verified commits are retained in Palomar's archive.

\subsection*{The Fourier quasicrystals of Theorem~\ref{thm:D}}
The development \cite{Mar26} was registered in Palomar on 8 October 2026
\cite{PalStr}.
\begin{itemize}[leftmargin=2em]
\item Toolchain: \texttt{leanprover/lean4:v4.35.0-rc3}, with Mathlib and the
other dependencies pinned in \texttt{lake-manifest.json}.
\item Statement of record: the theorem \texttt{strongCardinalClaim} in the file
\texttt{Challenge.lean}, proved in \texttt{Solution.lean} from the theorem
\path{exists_stronglyTemperedMeyerSpace_rank_aleph0} of the module
\texttt{OriginalClassicalStrongCountable}.
\item Build and check: \texttt{lake exe cache get Challenge.lean Solution.lean},
then \texttt{lake build Challenge Solution} and \texttt{python3 scripts/check.py}.
A configuration file restricts the axioms
of the main theorem to \texttt{propext}, \texttt{Classical.choice} and
\texttt{Quot.sound}.
\end{itemize}
In the notation of this paper the statement of record asserts: there is
$\Lambda\subset\R$ meeting every bounded interval in a finite set such that
$\dim_\C\M^{\mathrm{str}}_\Lambda=\aleph_0$. Here $\M^{\mathrm{str}}_\Lambda$ is defined
as the linear span of the tempered distributions $T$ such that $T$ and $\F T$ are
given on compactly supported Schwartz functions by local atomic formulas on
$\Lambda$ whose coefficients $a_x$ satisfy $\sum_{x\in\Lambda}|a_x|(1+|x|)^{-N}<\infty$
for some $N$ (possibly different for $T$ and $\F T$), and the statement includes that
this span consists exactly of such $T$. Since $X_N(\Lambda)\subseteq X_{N+1}(\Lambda)$,
this is the space $\bigcup_NX_N(\Lambda)$ of Section~\ref{subsec:strong}. The
Fourier transform is that of Mathlib, with kernel $e^{-2\pi\ii x\xi}$.

The statement of record concerns the rank only: it does not identify a basis, and
the finite dimension of every layer $X_N(\Lambda)$, although proved in the
development, is not part of it. The formal witness is a union of a coarse cone and of
blocks of the kind used in Section~\ref{sec:fqcount}, with the same slope $\beta$
(Section~\ref{subsec:beta}), the same scale $c=2^{1/4}$ and the same Lee--Yang
factors $p_a$. It differs from the set of Theorem~\ref{thm:fqcount} in the choice of
the remaining data: the sheet number of a block at the prime $m$ is the least $s$ with
$2m^4\le s^3$, the parameters are taken in disjoint dyadic intervals, and the formal
proof follows the corresponding, less simplified, route. The radii are obtained from
a compactness statement, as in Lemma~\ref{lem:compact}, and are then selected by
classical choice (Remark~\ref{rem:fqcount}). Thus the set $\Lambda$ of
Theorem~\ref{thm:fqcount}, parts~(ii) and~(iii) of Theorem~\ref{thm:D} and
Proposition~\ref{prop:finiteunion} as stated here are not part of this formal
statement. The following table indicates, by module name (in the directory
\texttt{MeyerGeneralProblem/Cardinal/Strong}), where the formal proof establishes
analogues of some of the main steps; since the two routes differ in their
parameters, the correspondence is only approximate.

\begin{center}\small
\begin{tabular}{>{\raggedright\arraybackslash}p{0.3\textwidth}>{\raggedright\arraybackslash}p{0.64\textwidth}}
\hline
Paper & Modules\\
\hline
Lemma~\ref{lem:beta} & \texttt{ParityContinuants}, \texttt{ParityLimit},
 \texttt{ParityBarrier}, \texttt{QuarterPhase}\\
Lemma~\ref{lem:strongorder} & \texttt{ReturnMassGrowth}\\
Proposition~\ref{prop:noreturn} & \texttt{OriginalStrongNoReturn},
 \texttt{OriginalNoReturnGeometry}\\
Lemma~\ref{lem:splitting} & \texttt{ScheduledOriginalChartLocalSplitting},
 \texttt{ScheduledOriginalGlobalSplitting}\\
Lemma~\ref{lem:compact}, Theorem~\ref{thm:fqcount} & \texttt{OriginalClassicalAdaptiveRadii},
 \texttt{OriginalClassicalLayerExhaustion},
 \texttt{ScheduledOriginalIndependentSources},
 \texttt{OriginalClassicalStrongCountable}\\
\hline
\end{tabular}
\end{center}

\subsection*{The crystalline measures of Theorem~\ref{thm:A}}
The development \cite{MS26} consists of roughly four hundred files. It was submitted
to Palomar on 30 September 2026 \cite{Pal26}.
\begin{itemize}[leftmargin=2em]
\item Toolchain: \texttt{leanprover/lean4:v4.35.0-rc3}.
\item Statement of record: the theorem \texttt{exhaustiveCardinalClaim} in the
file \texttt{Challenge.lean}, proved in \texttt{Solution.lean}.
\item Build and check: as above, with the same restriction on the axioms of the
main theorem.
\end{itemize}
In the notation of this paper the statement of record asserts: there is
$\Lambda\subset\R$ meeting every bounded interval in a finite set such that
$\dim_\C\M_\Lambda=\aleph_0$, such that membership in $\M_\Lambda$, defined as the
annihilator of the Schwartz functions vanishing on $\Lambda$ together with the
analogous condition for the Fourier transform, is equivalent to the two local
atomic formulas, and such that for some sequence $(g_n)$ every element of
$\M_\Lambda$ is a unique finite linear combination of the $g_n$. Tempered
distributions and the Fourier transform are those of Mathlib.
% Author: report here the build and axiom-check output of both developments, and
% add a permanent archival identifier (Zenodo or Software Heritage) for each exact
% commit if the journal requires one beyond Palomar's archive.

Of the results on the spaces $\M_\Lambda$ in Sections~\ref{sec:blocks}--\ref{sec:fq},
the symmetry of $\Lambda$, parts (ii)--(iii) of Theorem~\ref{thm:A},
Theorem~\ref{thm:B}, Section~\ref{sec:pairs} and
Section~\ref{sec:fq} are not part of this formal statement. The following table
indicates, by module name (in the directory
\texttt{MeyerGeneralProblem/Cardinal/Adaptive}), where the main steps of the
proof for the profile $P_i=i$ are formalised. It is meant as a guide for the
reader; the statement of record is the one described above.

\begin{center}\small
\begin{tabular}{>{\raggedright\arraybackslash}p{0.3\textwidth}>{\raggedright\arraybackslash}p{0.64\textwidth}}
\hline
Paper & Modules\\
\hline
Theorem~\ref{thm:rapid}(a)--(c) & \texttt{ActualSmallTailUniqueness}, \texttt{SeamCompleteKernel},
 \texttt{EndpointUniformAdmission}, \texttt{RapidNativeAdmission},
 \texttt{RapidNativeExclusion}, \texttt{RapidCompleteLine}\\
Theorem~\ref{thm:rapid}(d) & \texttt{CriticalHeadInverse}, \texttt{CriticalForwardMap},
 \texttt{CriticalGreenInverse}, \texttt{BlockTailEquivalence}\\
Lemma~\ref{lem:holes}, Theorem~\ref{thm:rapid}(e) & \texttt{FiniteHoleExchange},
 \texttt{ActualHoleExchange}, \texttt{ConcreteHoleCarriers}, \texttt{FiniteHeadExhaustion}\\
Proposition~\ref{prop:block} & \texttt{HighOrderGapLines}\\
Lemmas~\ref{lem:separation}, \ref{lem:selectors} & \texttt{SectorSeparation},
 \texttt{QuantitativeSectorSeparation}, \texttt{SmoothSelectors}, \texttt{ActualSourceSplitting}\\
Lemmas~\ref{lem:sublevel}, \ref{lem:nonres} & \texttt{PolynomialSublevel},
 \texttt{QuadraticSublevel}, \texttt{CatalogueNonresonance}, \texttt{CatalogueEvents}\\
Lemmas~\ref{lem:lift}, \ref{lem:translation} & \texttt{AntiperiodicLift},
 \texttt{PeriodicLift}, \texttt{SinglePhaseLift}, \texttt{LeadingTranslationErrors},
 \texttt{PhaseTranslationErrors}\\
Proposition~\ref{prop:parameters} & \texttt{StagePhaseParameters}, \texttt{TorusPhaseNets},
 \texttt{FiniteSmoothPartition}, \texttt{ActualRecursion}, \texttt{ActualGoodScales},
 \texttt{ProbabilityBudget}\\
Sections~\ref{subsec:phaseconv}--\ref{subsec:recovery} & \texttt{ActualConvolutionVanishing},
 \texttt{PolynomialSupportDescent}, \texttt{ActualPolynomialSupport},
 \texttt{ActualAtomRecovery}, \texttt{IsolatedMassRecovery}\\
Theorem~\ref{thm:exhaust}, Corollary~\ref{cor:exhaust} & \texttt{ConstructedFiniteExhaustion},
 \texttt{ConstructedGenerators}, \texttt{SectorIndependentFamily},
 \texttt{ConstructedAlgebraicBasis}, \texttt{ConstructedNativeUpperBound}\\
\hline
\end{tabular}
\end{center}