%
%
%
%
%
\section{Computer-Assisted Parts, Data, Validation and Lean}\label{app:cert}
Every computer-assisted result consists of a written reduction, a theorem proved in the text, and an explicit finite predicate checked over a finite set. Table~\ref{tab:ca} lists these items, followed by the exact computations quoted as parameters or as results of exhaustive searches in a stated scope. The data (check vectors, designs, window systems, tables, certificates) are archived, each item with a verifier that reads only the data files, never the search programs. Searches (over check vectors, for window systems, SAT solvers) only produced the data (Section~\ref{sec:conventions}).

\begin{table}[tp]
\centering
\footnotesize
\caption{The computer-assisted items: the finite check, its scope, and the independent verification. Below the middle rule: exact computations that are quoted but are not part of a proof of a theorem, proposition or corollary.}
\label{tab:ca}\label{tab:checks}
\setlength{\tabcolsep}{3pt}
\begin{tabular}{@{}>{\raggedright\arraybackslash}p{0.18\textwidth}>{\raggedright\arraybackslash}p{0.30\textwidth}>{\raggedright\arraybackslash}p{0.22\textwidth}>{\raggedright\arraybackslash}p{0.26\textwidth}@{}}
\toprule
result & finite check & scope & verified by\\
\midrule
Tab.~\ref{tab:residue} (Thm.~\ref{thm:residue}, Cor.~\ref{cor:korobov}) & exact $\ljit(\Lambda_v)^2$ by enumeration of $\Lambda_v$ in a box; for entries marked E, all check vectors $(x,-1)$ & the $18$ rows, the Korobov column & three programs; a brute force at $s=4$, $p=1009$\\
Thm.~\ref{thm:block}(c) below its proof range & exact $\LB(F)$ of $U^*_4$, $U^*_5$ (Lem.~\ref{lem:cert}, $j=1$) & every prime $7\le p\le109$ ($s=4$), $19\le p\le109$ ($s=5$) & two programs; a third at $24$ of them; Lean kernel\\
Thm.~\ref{thm:block}(d) & hypothesis of Lem.~\ref{lem:signclass}; exact $\LB(F)$ below its range & $s=4,\dots,7$; primes as in the proof & two programs; Lean kernel in part (App.~\ref{app:lean})\\
Prop.~\ref{prop:primepower} & exact $\beta_q(k)$; for $s\le3$ for every $f$, $k$ & the $26$ rows of Tab.~\ref{tab:primepower} & two or three programs; Lean kernel\\
Thm.~\ref{thm:p7} & no vanishing combination in $\LB(\mathsf w)$ & $5$ classes of steps, $\le7^6$ combinations each & three programs (App.~\ref{app:p7}); Lean kernel\\
Thm.~\ref{thm:A3} & $\mathcal P(p_0)$, $p_0=19\,673\,600$ & one exact evaluation & second evaluation of $\mathcal P$; Lean kernel\\
Rem.~\ref{rem:A3range} & hypotheses of Prop.~\ref{prop:steer} and Lem.~\ref{lem:W}, crosses in $\F_p$ & $1\,035\,877$ primes in $[3\cdot10^6,1.97\cdot10^7]$ & checker with its own exact window bound\\
thresholds after Thm.~\ref{thm:A}, $s=4,5$ (not part of its proof) & $\mathcal P(p_0)$ & one exact evaluation each & spot check above $p_0$; Lean kernel\\
Cor.~\ref{cor:HB17} & conditions of Thm.~\ref{thm:HB}, coverings as set identities & $715$ primes, $3677<p<10^4$ & second program; Lean kernel\\
Thms.~\ref{thm:B2}, \ref{thm:S3}, \ref{thm:K4}, \ref{thm:S4}, Rem.~\ref{rem:B3} & response sets (Prop.~\ref{prop:automaton}) and the minimum of Lem.~\ref{lem:cert} & Tab.~\ref{tab:frames} & second program; Lean kernel\\
Tab.~\ref{tab:practice}, certified bounds & generator matrices rebuilt from Def.~\ref{def:residue}, exact $\ljit(\Lambda_v)^2$ & $p=13$, $17$, $23$, $31$ & three programs\\
\midrule
Tab.~\ref{tab:sobolpar} & orders $\nu$, $k$ and the levels $L$, $m$ & $s=2,\dots,7$ & second program\\
Cor.~\ref{cor:halton}, explicit pairs & the two points of each pair are closer than the bound & $244$ cases of bases and carrying coordinate & exact distances of the pairs\\
Rem.~\ref{rem:skelsearch} (exhaustive in its scope) & branch and bound over the check-vector sequences of the best class & $s=2$; $p=11$, $13$, $17$; $K_{\max}=10$, $8$, $11$ & independent reproduction\\
example after Cor.~\ref{cor:nodesign} & dimension of a space of relations & $s=4$, $J=3$; $p=11$, $K=4,\dots,11$; $p=13,17$, $K=4$ & two methods (and the audit)\\
Lem.~\ref{lem:witness} brackets & explicit close pairs of points & $K=18$ ($\F_4$), $K=75$, $64$ & second program for Thm.~\ref{thm:K4} only\\
optimality remark after Thm.~\ref{thm:block}(d) & no $\delta\in[0,A]^s$ with a smaller $A$ in Lem.~\ref{lem:signclass} & $s=4,5,6$ & two programs\\
Sec.~\ref{sec:hammersley}, Fig.~\ref{fig:hammersley} & exact toroidal $\delta(\hat P_m)$ of the Hammersley lifts & $s=2$: $p=5,\dots,19$, $m\le10$ ($p=5$); $s=3$: $p=5,\dots,13$, $m\le8$ & $O(N^2)$ check for small $N$; audit program with its own matrices\\
\bottomrule
\end{tabular}
\end{table}

\subsection{Verification}\label{app:verification}
Every finite check used in a proof was carried out by at least two programs (Table~\ref{tab:ca}), the second written from the statements of the paper only. Remark~\ref{rem:A3range} and the brackets of Appendix~\ref{app:sharp} for Theorems~\ref{thm:S3}, \ref{thm:S4} rest on one program each, the thresholds quoted after Theorem~\ref{thm:A} on one program and the Lean kernel.

\emph{Residue and block-periodic sequences.} The values $\ljit(\Lambda_v)^2$ of Table~\ref{tab:residue} were computed by the search, by an independent enumeration in the audit, and by a short program that enumerates, for a claimed value $L$, the box $|b_c|\le1+\lfloor\sqrt L\rfloor$ (which contains every lattice vector with $\|(|b|-\mathbf 1)_+\|_2^2\le L$); it also checks the Korobov column and the check vectors of Table~\ref{tab:practice}. The entry $s=4$, $p=1009$ was also confirmed by a brute force over the box $|b_c|\le6$. For Theorem~\ref{thm:block}(c) the two programs evaluate the one-digit relaxation from its definition (from the two possible differences of positions, resp.\ by the minimum over all positions $R$) on one data file of $U^*_4$, $U^*_5$ (for $s=4$ the matrices printed after Theorem~\ref{thm:block}), and the second rejects a design whose largest diagonal entry is changed by one. For Theorem~\ref{thm:block}(d) two independent programs computed the hypothesis of Lemma~\ref{lem:signclass} and $\LB(F)$; the files of $U^*_4,\dots,U^*_7$ agree with an independent implementation of the definition in \cite{Gru26geo}, which reproduces $a^*_s$ and the largest entries listed there%
, and their reachability was checked by exact interpolation over $\mathbb Q$ (only the primes $2,3,5$ occur in denominators and leading coefficients). The values $\beta_q$ of Proposition~\ref{prop:primepower} were computed by two audits with their own field arithmetic; for $s\le3$ also as maxima over every power-basis encoding and every weight (with the search program), and by a third program. The generator matrices of Table~\ref{tab:practice} were rebuilt entry by entry from Definition~\ref{def:residue}, and $\mathcal J$ was recomputed by an independent pipeline.

\emph{Window systems.} The verifiers were in addition run by an adversarial audit with its own implementation. The common verifier checks for a record: admissibility of the $\lambda_c$ and the places modulo $p$; the crosses $\kappa_{c\leftarrow c'}$, recomputed by Proposition~\ref{prop:LI}(c) in two normalisations, against the stored ones; integrality of the crosses of a rational system; condition (i) of Proposition~\ref{prop:steer}; condition (ii) for every column, exactly (an exact scan for at most two restricted crosses, enumeration of $\F_p^j$ when $p^{j-1}\le2\cdot10^6$) or by Lemma~\ref{lem:ws} in the stored order of the rows; and $\LB(W)$ from its definition. All five archived window systems pass (the four ordered systems of Section~\ref{sec:practice} and the staggered system of Figure~\ref{fig:bsgeom}). Each of the $30$ copies with one stored cross changed by one is rejected; of the $22$ copies with an own window shortened by one at one end, $18$ are rejected and $4$ (two windows, both ends) are valid with the same bound: those windows were longer than needed. The exact separations quoted for figures and tables come from exact minimum-distance programs on the generated points.

\subsection{Archive}\label{app:archive}
The archive (directory \texttt{archive} of the repository named on the title page, release v1.0.0, archived at Zenodo) has one directory per item:
%
%
\texttt{verify} (the verifier of the window systems, corruption test);
\texttt{residue\_tables} (Table~\ref{tab:residue}, with the three enumeration programs);
\texttt{block\_lb} (the designs of Theorem~\ref{thm:block}(c),(d), the evaluations of $\LB(F)$, the check of Lemma~\ref{lem:signclass}, the check of the files of $U^*_s$ and the optimality search after Theorem~\ref{thm:block}(d), with the programs);
\texttt{primepower} (Table~\ref{tab:primepower} and the zeros of $\beta_q$ after it, with the programs);
\texttt{p7\_\allowbreak graph\_\allowbreak certificate} (Theorem~\ref{thm:p7});
\texttt{bs\_ruleB\_s3} (Theorem~\ref{thm:A3}, Remark~\ref{rem:A3range});
\texttt{bs\_\allowbreak s45\_\allowbreak thresholds} (Theorem~\ref{thm:A});
\texttt{selection\_rule} (Remark~\ref{rem:steerrule}, the window system of Figure~\ref{fig:bsgeom});
\texttt{practice} (the residue sequences of Table~\ref{tab:practice} by places, scale and check vector, with generator matrices and the computation of $\mathcal J$; the ordered window systems of Section~\ref{sec:practice}; a point generator);
\texttt{b2\_dropin} (Theorem~\ref{thm:B2} as a table of $32$-bit direction numbers, with a reference implementation in C and a check of its points);
\texttt{failure} (Table~\ref{tab:sobolpar}, the explicit pairs of Section~\ref{sec:fail});
\texttt{exact\_relations} (Remark~\ref{rem:skelsearch}, the example after Corollary~\ref{cor:nodesign});
\texttt{hammersley} (Section~\ref{sec:hammersley}: the exact separations of the lifts and the check of the pairs of Proposition~\ref{prop:liftcarry}, with the programs);
\texttt{common} (a shared C\texttt{++} header).
Each directory has a README with the statement it supports and the command that re-runs its check; every check runs in less than a minute on one core. Requirements: Python~3, C\texttt{++}17 and C compilers, SymPy (exact rational evaluations; one program in \texttt{block\_lb}), NumPy (two programs in \texttt{practice}, one in \texttt{hammersley}). The record format of the window systems is described in \texttt{verify/README}. The automata of Section~\ref{sec:frames} and the range of Corollary~\ref{cor:HB17} are part of the Lean development. The points shown in the figures are exact points of the constructions, computed from their generator matrices, except in the panels marked as schematic; the scripts that generate every figure, with their data, are in the directory \texttt{paper/scripts} of the same repository.

\subsection{Lean}\label{app:lean}
The written proofs are the primary evidence; the formalization is an additional, independent check, not a replacement. The library \texttt{GeoSeq} (Lean~4 with Mathlib), which extends the Lean development of \cite{Gru26geo}, contains formal statements and proofs of most results of this paper. Every formalized statement is restated in a separate statement file and compared with its proof by the Comparator tool, which re-checks the proofs with two independent kernels (the Lean kernel and NanoDa) and admits only the three standard axioms (propositional extensionality, quotient soundness, choice). No proof uses \texttt{sorry} or \texttt{native\_decide}; finite computations are evaluated by the Lean kernel.

\emph{Formalized results of this version.} Section~\ref{sec:fail}: every definition, lemma, theorem and corollary, and Remarks~\ref{rem:faurerate} and~\ref{rem:randomize}; the results on carry pairs also over every finite field, for every digit code with a carry pair, e.g.\ every natural identification (\texttt{carryPair\_nat}, \texttt{nonqu\_code}). Lemma~\ref{lem:resform} ((b) over every field), Lemma~\ref{lem:reschange} over every commutative ring (\texttt{reschange}), Lemma~\ref{lem:prefix} and Remark~\ref{rem:prefixcases}. Section~\ref{sec:residue}: every definition, lemma, theorem, corollary and example (Theorem~\ref{thm:WF} for Definition~\ref{def:WF}). Section~\ref{sec:block}: Theorem~\ref{thm:block}(i)--(iii) for every reachable design, with the design multipliers over every field (\texttt{designNum\_exists}, \texttt{designNum\_order}); cases (a), (b); (c) for every $s\ge3$ at $p\ge5a^*_s+4$ (\texttt{blkS\_block}), and for $s=4,5$ with the computer-assisted ranges and the equality of $\LB(F)$ (\texttt{blk4\_LB\_eq}, \texttt{blk5\_LB\_eq}); (d) for $s=4,5,6$ at every prime $p\ge11$, $23$, $125$ (\texttt{blk4d\_block}, \dots, \texttt{blk6d\_block}), with Lemma~\ref{lem:signclass} (\texttt{sc\_LB}); Theorem~\ref{thm:blocktwo}, Proposition~\ref{prop:implied}, Corollary~\ref{cor:gauss}. Section~\ref{sec:count}: every definition, lemma, theorem, proposition and corollary (with the upper densities). Section~\ref{sec:antipode} and Appendix~\ref{app:LFdata}: every lemma, proposition, theorem and corollary (Section~\ref{sec:joint} is new). Lemma~\ref{lem:shift}. Section~\ref{sec:hammersley}: Propositions~\ref{prop:liftslab} and~\ref{prop:liftcarry} with the constant $\gamma$ (\texttt{liftslab\_i}, \texttt{liftslab\_ii}, \texttt{liftcarry\_sharp}, \texttt{liftcarry\_closed0}, \texttt{liftcarry\_closedMu}, \texttt{lift\_not\_wellsep}; the display of Proposition~\ref{prop:liftcarry} as a sum over the coordinates), (i) and (ii) of Proposition~\ref{prop:liftslab} over every finite field and digit code, Proposition~\ref{prop:liftcarry} for every digital shift. Proposition~\ref{prop:primepower} for every finite field and digit code (\texttt{primepower\_of\_check}), with all rows of Table~\ref{tab:primepower} evaluated on explicit models $\F_p[x]/(f)$ (increments checked per model). Theorem~\ref{thm:coverage} (\texttt{coverage\_pp\_of\_parts}, \texttt{coverage\_pp\_new}), except $p=11,13,17$ in (d) and case (e). Kept from the previous version, with statements that agree up to wording: Lemmas~\ref{lem:t0} and~\ref{lem:cert}, Remark~\ref{rem:onedigit}, Proposition~\ref{prop:law}, Example~\ref{ex:running}; Theorems~\ref{thm:B2}, \ref{thm:S3}, \ref{thm:K4}, \ref{thm:S4} and~\ref{thm:p7} and Remark~\ref{rem:B3} with their automata (for the instances used), Lemma~\ref{lem:octave}, Corollary~\ref{cor:allprimes}, and Propositions~\ref{prop:N2} and~\ref{prop:rank2}.

\emph{Where the formal statements differ in form.} The theorems of Sections~\ref{sec:count} and~\ref{sec:joint} are proved in residue form and transferred to Definition~\ref{def:selfsim} by bridge theorems (e.g.\ \texttt{selfsim\_joint\_ii}); Propositions~\ref{prop:onerel}(i) and~\ref{prop:blockrel} are derived from Theorem~\ref{thm:count}, for every scramble of a frame. In Theorem~\ref{thm:block}(c),(d) the computer-assisted parts are checkers (one-digit relaxation, hypothesis of Lemma~\ref{lem:signclass}) proved sound once and evaluated by the kernel; the upper bounds behind the equalities hold for every prime (\texttt{axis\_term}). Case (c) for general $s$ uses the formal $U^*_s$ of the nets library, defined by choice: $a^*_s$ is not evaluated, and the equality of $\LB(F)$ is proved under the hypothesis $\alpha_0=a^*_s$ (\texttt{blkS\_LB\_eq\_of}), checked in the paper for $s\le10$; the column of ones is proved for every $s$ (\texttt{ustar\_col0}). For $s=4,5,6$ the literal matrices of the nets' computation are used, with reachability proved directly. The square-lattice clause of Corollary~\ref{cor:gauss} is formalized as an inclusion, Theorem~\ref{thm:coverage} as an assembly.

\emph{Not formalized.} Theorem~\ref{thm:block}(d) for $s=7$, for $s=6$ below $p=125$, for $s=4,5$ below $p=11$, $23$; $a^*_s$ for $s\ge6$; the optimality remark after Theorem~\ref{thm:block}(d); Remark~\ref{rem:randomize}(a),(b) for prime powers; Tables~\ref{tab:residue}, \ref{tab:sobolpar}, \ref{tab:practice}, and the optimality over $f$, $k$ in Table~\ref{tab:primepower}; Remark~\ref{rem:A3range}, Lemmas~\ref{lem:riordan} and~\ref{lem:witness}, the binary-sequence clauses of Theorems~\ref{thm:K4} and~\ref{thm:S4}, Remark~\ref{rem:toeplitz}; in Section~\ref{sec:hammersley} the list of covered sequences after Proposition~\ref{prop:liftcarry} (of which the residue and staggered residue sequences with the places $0,1$ are formalized), in-slab bounds for the lifts of the sequences over $\F_4$, and the computed comparison; the other remarks and the figures.

\emph{Configurations.} The new results are compared in $59$ Comparator configurations with $730$ theorems: $32$ with $311$ theorems from the first stages, $27$ with $419$ added for this version (\texttt{comparatorGeoSeqV10\_1*}, \texttt{V10\_2}, \texttt{V10\_3}, \texttt{V10\_3x}, \texttt{V10\_4*}, \texttt{V10\_5}, the last with the $51$ theorems of Section~\ref{sec:hammersley}). All of them, and the Palomar entry below, were accepted by both kernels. Results kept from the previous version are compared in its configurations. All configurations, of both versions and of the Palomar entry, were re-run once in sequence on the final state of the library and accepted by both kernels; the configuration of Section~\ref{sec:hammersley} was added afterwards, without changing any earlier Lean module.

\emph{Palomar entry.} A self-contained entry in the format of the Palomar collection (one file of $195$ lines importing only Mathlib) states the two headline results with their own definitions, checked against those of the library by bridge theorems: Corollary~\ref{cor:halton}, and Theorem~\ref{thm:residue} with Corollaries~\ref{cor:korobov} and~\ref{cor:residueQU} for the Korobov check vector and Faure places ($(0,s)$-sequence for every prime $p>2^s$, separation bound at every prefix $P_{sK-1}$, bounded mesh ratio).

\subsection{The Small-Base Bounds: Explicit Close Pairs}\label{app:sharp}
The certified bounds of Theorems~\ref{thm:S3}, \ref{thm:K4} and~\ref{thm:S4} are far below the exact separations of Table~\ref{tab:frames}, but this is not a weakness of the bound (for Theorem~\ref{thm:K4} by two programs, for the others by one). A carry of length $l$ exists only from level $K=l$ on, and the binding steps involve long carries, which the computable prefixes do not contain. The next lemma turns a binding configuration into a pair of points.

\begin{lemma}[Explicit close pairs]\label{lem:witness}
Let the offset map be the same at every level, and fix $j$, a step $e$, carry lengths and carry digits of the moving coordinates, with the changes $\sigma_c$ of Lemma~\ref{lem:cert}. At a level $K$ at least the largest carry length, the cells with this carry pattern are given by prescribing some of their finest digits. If the affine map from the remaining cell digits to the geometric digits $(R_c)_c\in\F_q^{sj}$ is onto, then $\sep{P_{sK}}\le\bigl(\sum_c(f_j(e_c,\sigma_c)+2q^{-j})^2\bigr)^{1/2}$.
\end{lemma}

\begin{proof}
Choose $R^*_c$ attaining the minimum in $f_j(e_c,\sigma_c)$ and, by surjectivity, a cell $n$ with the carry pattern and $R(n)=R^*$. The neighbour $n+e$ has the geometric digits $R^*_c\oplus\sigma_c$, so by (\ref{eq:cellunits}) the two points differ in coordinate $c$ by at most $f_j(e_c,\sigma_c)+2q^{-j}$ cell units.
\end{proof}

For Theorem~\ref{thm:K4} the binding configuration (carry lengths $9$ and $16$) is realisable at $K=18$, where the map has full rank, and gives two points of $P_{54}$ at distance $0.112940$ cell units. So $0.112930\le\inf_K\sep{P_{3K}}\le0.112940$ (computer-assisted), to $0.01\%$. Likewise $\sep{P_{225}}\le0.05616$ for Theorem~\ref{thm:S3} and $\sep{P_{256}}\le0.03176$ for Theorem~\ref{thm:S4}. Larger constants in these frames need other multipliers, not better bounds.

As binary sequences, the prefixes of $2^M$ points of Theorem~\ref{thm:K4} have base-$2$ quality parameter $t\le3$ for $M\le18$, $t=0$ at every $M=6K$; those of Theorem~\ref{thm:S4} have $t\le4$ for $M\le20$ (computations); the three- and four-dimensional Sobol' sequences have $t=1$ and $3$.

\begin{remark}[Why these bases]\label{rem:height}
Heuristically: in a Kummer frame $\coef{n}\tau^{-b}=\prod_i\binom b{n_i}$ over the base-$q$ digits $n_i$ of $n$. For $q=3$ only $b\le1$ occurs, and for $q=4$, $(1+x)^2=1+x^2$ keeps all coefficients in $\{0,1\}$, so the automata stay small; over $\F_5$ the coefficients $2$, $3$ appear, and the symmetric scrambles we screened had over $300$ response columns per coordinate at $j=3$, without positive bound.
\end{remark}