Historical context and scope

Mutually unbiased bases describe projective measurements for which a state from one basis produces the uniform outcome distribution in every other basis. This finite-dimensional form of complementarity appears in Schwinger’s unitary-operator framework (Schwinger 1960). Ivanović developed the state-determination problem and prime-dimensional constructions (Ivanović 1981); Wootters and Fields proved the statistical optimality of complete sets for state determination and constructed them in every prime-power dimension (Wootters and Fields 1989). One has \(N(d)\le d+1\); an operator-space proof and further prime-power constructions are given in (Bandyopadhyay et al. 2002). Dimension six is the first dimension outside the prime-power class.

The tensor-product construction gives three bases in \(\mathbb C^6\) (Klappenecker and Rötteler 2004, sec. 4). Zauner’s dimension-six MUB conjecture asserts that this lower bound is sharp. Its origin is traced to his 1991 diploma thesis (Zauner 1991); see also the historical account in (McNulty and Weigert 2026, sec. 2.3). His doctoral thesis states the corresponding quantum-design conjecture (Zauner 1999, sec. 3.3), later translated in (Zauner 2011). The equation \(N(6)=3\) appears explicitly as Conjecture 1 of (Klappenecker and Rötteler 2004, sec. 4).

Several complementary approaches developed the dimension-six problem. Grassl proved that the standard–Fourier pair cannot belong to four mutually unbiased bases (Grassl 2004, Theorem 2). Bengtsson and collaborators studied its unbiased vectors and the surrounding landscape of Hadamard families (Bengtsson et al. 2007). Numerical searches by Butterley and Hall (Butterley and Hall 2007) and by Brierley and Weigert (Brierley and Weigert 2008) supplied evidence for the conjecture. Brierley and Weigert also used algebraic equations to enumerate unbiased vectors for specified Hadamards (Brierley and Weigert 2009); their Section 3.4 supplies rigorous approximation bounds for exact input matrices, while their Section 4.3 explains the limitations introduced by rounding coefficients in sampled non-affine families.

The closest antecedent of the present proof is the certified discretization of Jaming, Matolcsi, Móra, Szöllősi and Weiner. They proved that the standard basis together with any member of the two-parameter Fourier family cannot be extended to four bases (Jaming et al. 2009, Theorem 1.4). Their Section 3 combines phase intervals, rigorous error bounds, subdivision, and exhaustive compatibility tests. Jaming, Matolcsi and Móra subsequently formulated an unrestricted discretization program (Jaming et al. 2010, secs. 2–4). The present proof completes an exhaustive cover of arbitrary second bases. The completion and displacement estimates described below reduce this cover to a finite search with certified error bounds.

Recent work on triples retains conjectural sufficient conditions for \(N(6)=3\) (Matolcsi et al. 2026, sec. 4). The classification preprint of Cárdenes Wuttig and Tindall concerns individual order-six Hadamard matrices and leaves their MUB compatibility unresolved (Cárdenes Wuttig and Tindall 2026, sec. VI). Our proof constructs a cover of arbitrary second bases directly. Its upper bound combines that exhaustive cover with local exclusion of two further bases and the complete execution and arithmetic contract of Theorem 58.

The covering and exclusion strategy

The second basis varies throughout the search, so the cover must retain its possible displacement while testing additional vectors. The proof first covers every second basis by balls in its real entrywise phases, then excludes two further bases uniformly throughout each ball. Figure 1 summarizes the five parts of this argument.

1. Row and column rephasings make the first row and column of \(H\) equal to one. The first two rows and columns then contain nine remaining phases. A symmetry reduction and necessary interval tests cover their possible values by finitely many seed balls (2).

2. In Stage A, write \(H\) in blocks with row and column sizes \(2+4\). The seed fixes the upper-left, upper-right, and lower-left blocks up to their phase displacements; the lower-right \(4\)-by-\(4\) block remains to be completed. At each seed center that passes the frame checks, the upper-right block and the conjugate transpose of the lower-left block have rank two, and hence two-dimensional kernels in \(\mathbb C^4\). Compressing the unknown block between these kernels gives a \(2\)-by-\(2\) matrix. The Hadamard equations bound its distance from \(\sqrt6\) times its unitary polar factor. A closed cover of \(U(2)\), the group of \(2\)-by-\(2\) unitary matrices, therefore accounts for every feasible completion. Uniform Taylor bounds either exclude a cell or place all its exact completions in certified phase balls ([sec:completion,sec:phase-cover]). The frames for these kernels remain fixed at the seed center, which need not itself be feasible.

3. In Stage B, each ball carries numerical directions approximating the tangent directions of the Hadamard equations. A verified residual identity bounds the error in representing every exact solution displacement by these directions. Covering the tangent coordinates and retaining this normal bound yields smaller balls covering all the same exact solutions (5). No manifold parametrization is required.

4. In Stage C, a phase-bin search in each final ball covers every vector unbiased to the first two bases by small vector balls. Make these vector balls the vertices of two graphs: an \(\mathcal O\) edge retains a possible orthogonal pair, and a \(\mathcal U\) edge retains a possible unbiased pair. Necessary tests remove only impossible edges. Two additional bases would require two disjoint six-cliques in \(\mathcal O\), with all \(36\) cross edges in \(\mathcal U\). The finite search excludes this pattern (6).

5. The complete execution accounts for every seed, every refined ball, and every initially unresolved record. The fallback finishes with no unresolved record (7).

The distinction between proposing a numerical object and certifying it is used throughout. A floating-point center need not be an exact Hadamard matrix. A computed small eigenspace need not parametrize a component. A numerical linear solve need not be accurate: its output is accepted only when a separate bound verifies the required inequality. Every rejection uses a necessary condition with an explicit safety margin. A failed certification or an exhausted search cap retains an unresolved region; it cannot prove nonexistence.

All interval cells may be taken closed. Their overlap, repeated phase representatives, and redundant balls or graph vertices can weaken the exclusion but do not omit a possible configuration. The arithmetic premises are stated, and the finite ranges and rounding margins are proved, in 9. The accompanying execution and build archives, identified in verification/computation/README.md, preserve the evidence for the fresh run documented in Section 7.5. This proof uses that run. The separate September 7 execution reported in the source manuscript has not been authenticated here.

The elementary lower bound

The lower bound uses only the tensor-product construction mentioned above. We give it explicitly to separate attainment of three bases from the computer-assisted exclusion of four.

A Lie-algebra consequence

An orthonormal basis \(\mathcal B\) of \(\mathbb C^6\) determines the Cartan subalgebra \(\mathfrak h_{\mathcal B}\) of traceless matrices diagonal in that basis. It is spanned by the matrices \(bb^*-I/6\) for \(b\in\mathcal B\). The Killing form on \(\mathfrak{sl}_6(\mathbb C)\) is \(K(X,Y)=12\operatorname{tr}(XY)\); two subalgebras are Killing-orthogonal when this form vanishes between them. For unit vectors \(b,c\), \[\operatorname{tr}\bigl((bb^*-I/6)(cc^*-I/6)\bigr) =|\langle b,c\rangle|^2-\frac16.\] Thus two bases are mutually unbiased exactly when their associated Cartan subalgebras are Killing-orthogonal. These algebras are closed under the standard adjoint, and the converse correspondence uses this same adjoint condition.

Equivalences and phase gauges

A common unitary maps the first member of any proposed family to the standard basis. Unbiasedness to that basis forces the entries of the second basis matrix to have modulus \(1/\sqrt6\). Thus it is \(H/\sqrt6\) for a matrix as in Definition 4; since \(H\) is square, \(HH^*=6I\) also gives \(H^*H=6I\). Every such \(H\) admits a real phase lift \(P\) with \(H=e(P)\).

The transposition argument applies to an exact Hadamard matrix. It does not assert that an approximate center supplies a unitary change of basis.

For a real \(6\)-by-\(6\) matrix \(z\), define double centering by \[ (\Pi z)_{ij} =z_{ij}-\frac16\sum_bz_{ib}-\frac16\sum_az_{aj} +\frac1{36}\sum_{a,b}z_{ab}. \tag{1}\] Its range is the horizontal subspace of matrices with every row sum and every column sum zero. We also use unwrapped dephasing, \[ D_0(P)_{ij}=P_{ij}-P_{i0}-P_{0j}+P_{00}. \tag{2}\]

Likewise, \(D_0(P)\) gives an equivalent matrix with first row and column phases zero. When a wrapped difference is used, its chosen integers define legitimate phase representatives. No argument requires a rounded decision at a half-integer to agree with a uniquely preferred nearest representative.

A symmetry arrangement for nine phases

The gap of a finite circular multiset is its largest circular gap. Equivalently, it is the greatest length of an open arc containing no point of the multiset. Points are counted with multiplicity when sorted; a repeated point contributes a zero gap. For each pair of distinct rows of \(P\), consider their six phase differences modulo one, and do the same for each pair of distinct columns.

Set \(N=112\) and \(w=1/N\). All bins are closed: \[ I_b=[b/N,(b+1)/N],\qquad u_b=(b+1/2)/N,\qquad 0\le b<N. \tag{6}\] They cover \([0,1]\), including both endpoints. Assignments at shared boundaries need not be unique. Sorted exact phases admit nondecreasing bin indices, so write the five indices for \(x_1,\ldots,x_5\) as \[b^X=(a,b,c,d,l),\qquad 0\le a\le b\le c\le d\le l<N.\] The orientation condition implies the necessary integral restriction \[ \frac aN\le x_1\le x_5-x_4\le\frac{l+1-d}{N}, \qquad a\le l-d+1. \tag{7}\]

For this index tuple choose \(s\in\{0,\ldots,4\}\) as the first minimizer of \(|2b^X_s+1-N|\). This is the rule in seeds::mk. Its selected original column is \(s+1\), its selected exact phase is \(\xi=x_{s+1}\), and the new column order is the original column zero, column \(s+1\), and the other four columns in their former order. This selection only specifies a column; it imposes no further condition on \(\xi\).

After arranging \(y\) as in (4), its five varying entries have bins \[b^Y=(b^X_s,b^Y_1,b^Y_2,b^Y_3,b^Y_4),\qquad 0\le b^Y_1\le b^Y_2\le b^Y_3\le b^Y_4<N.\] The shared entry uses precisely the same bin as in \(x\); it is not required to be ordered relative to the four tail bins.

For sorted midpoint bin indices \(q_0,\ldots,q_4\), the gap used by mk is \[\max\left\{\frac{q_0+1/2}{N}, \frac{q_1-q_0}{N},\ldots,\frac{q_4-q_3}{N}, 1-\frac{q_4+1/2}{N}\right\}.\] For a \(Y\) tuple it sorts a copy solely for this computation, preserving the stored shared-first ordering.

Vanishing-sum filters and the shared displacement

For either list, let \(u=(u_0,\ldots,u_4)\) be its five varying midpoints. Define the real two-vector \(c\) and real \(2\)-by-\(5\) matrix \(J\) by \[ c=\frac{1+\sum_{j=0}^4e(u_j)}{2\pi i},\qquad J_j=e(u_j), \tag{9}\] using realification in both definitions.

The function sumok tests (11) in the residual direction and in directions perpendicular to the five unit-exponential columns. The inequality holds for every real direction, so their numerical construction need not reproduce any prescribed exact direction. The one-sided margins for evaluating the residuals and supports are established in Section 9.

In grid units \(h=N\Delta\), write \[ E=\frac{5\pi}{4N},\qquad \|Jh+Nc\|\le E, \qquad |h_j|\le\frac12. \tag{12}\]

The function extend begins with \([-1/2,1/2]\) and intersects these constraints, using the shared column direction and directions perpendicular to the other four columns. Here \(t=s\) for \(X\) and \(t=0\) for \(Y\). It omits divisors of magnitude below \(10^{-6}\), which only removes a constraint. Numerator and endpoint margins enlarge the computed intervals, as proved in Section 9. The pair is rejected only when the two resulting intervals are strictly disjoint; a common endpoint is retained.

The enumeration in seeds::build now has an explicit interpretation. It visits every weakly increasing five-bin \(X\) tuple and applies (7), the first inequality in (8), and sumok. Separately, for every possible first bin it visits all weakly increasing four-bin \(Y\) tails and applies sumok. The program covout matches the shared bin, applies the second gap inequality, and intersects the shared displacement intervals. Every discarded exact solution would therefore violate one of the necessary conditions just proved. The numerical gap comparisons include outward slack, treated in Section 9.

Certified reuse of seed centers

The nine seed coordinates, before moving the selected column, are \[ q=(x_1,x_2,x_3,x_4,x_5,y_2,y_3,y_4,y_5)\in\mathbb R^9. \tag{15}\] For a bin pair let \(u\in\mathbb R^9\) be its rational midpoint and put \(h=N(q-u)\). Thus \(h\in[-1/2,1/2]^9\); the shared displacement is \(h_s\). Retaining \(u\) as a center would cover the entire bin with radius \(3/(2N)<0.032\). To reduce the number of centers, we instead test whether its feasible portion lies in a radius-\(0.032\) ball about a previously retained midpoint. If no such test succeeds, we retain \(u\).

Let \(J_X,J_Y,c_X,c_Y\) denote the data in (9). Define a real \(4\)-by-\(9\) matrix \(J_*\) by specifying its action: \[ J_*h=\begin{pmatrix} J_X(h_0,h_1,h_2,h_3,h_4)^T\\ J_Y(h_s,h_5,h_6,h_7,h_8)^T \end{pmatrix},\qquad p_*=\begin{pmatrix}-Nc_X\\-Nc_Y\end{pmatrix}. \tag{16}\] For feasible \(h\) we have \(J_*h=p_*+r_*\), where the two real two-vector blocks \(r_X,r_Y\) of \(r_*\) satisfy \(\|r_X\|,\|r_Y\|\le E\).

The function supdual proposes vectors \(v\) and evaluates the right side of (19). The validity of a proposal does not depend on how it was generated or on the accuracy of the heuristic linear solve. Only finite proposed components of magnitude at most \(10^4\) are used. Its evaluation replaces \(1.25\pi/N\) by the larger \(1.251\pi/N\) and adds a final support margin. Section 9 proves that the resulting bound is conservative.

Set \(R=0.032\). For a proposed previous center, testBucket first tries (18), and then, if applicable, the dual bound. It returns success only when the resulting upper bound in (17) is below the safely lowered comparison threshold for \((NR)^2\). Hence success certifies the entire feasible portion of the current bin pair, rather than just its midpoint. Distance cutoffs, bucket indices, and reach tests only decide which previous centers to try. Omitting a possible previous center cannot produce a successful coverage test.

For clarity, the shared column is counted once in (15), although its displacement enters both equations in (16). Reuse requires equality of the selected position \(s\). Moving that position to the start of the five \(X\) coordinates then applies the same coordinate permutation to the current point and the retained center, and preserves their Euclidean distance. The resulting order is the selected \(X\) entry, the other four \(X\) entries in order, and the four \(Y\) tail entries. These are precisely the nine entries of the dephased first two rows and columns used in the next stage. Centers retained earlier for the same \(X\) tuple are handled identically, with the first five components of \(k\) zero.

Seed blocks and fixed complementary frames

Fix the stored seed center, taking its binary phase coordinates as exact real numbers. After moving the shared column into the second position, write its relevant unit entries as \(a,b_0,\ldots,b_3,c_0,\ldots,c_3\), and put \[ E_0=\begin{pmatrix}1&1\\1&a\end{pmatrix},\qquad B_0=\begin{pmatrix}1&1&1&1\\b_0&b_1&b_2&b_3\end{pmatrix},\qquad (C_0)_{i,:}=(1,c_i). \tag{20}\] A feasible completion is an entrywise unit-modulus matrix \[H'=\begin{pmatrix}E'&B'\\ C'&D'\end{pmatrix},\qquad H'H'^*=H'^*H'=6I,\] with first row and first column equal to one. Its seed displacements, measured in radians, are ordered as \[s=(s_a,s_{b_0},\ldots,s_{b_3},s_{c_0},\ldots,s_{c_3})\in\mathbb R^9.\] Thus the varied entries are \(a e^{i s_a}\), \(b_j e^{i s_{b_j}}\), and \(c_i e^{i s_{c_i}}\). The shared entry occurs once in \(s\). With zero-based row-major phase indexing, these coordinates occupy \[ (7,8,9,10,11,13,19,25,31). \tag{21}\] The enlarged seed radius in cycles is denoted by \(r_s\), and \(R_s=2\pi r_s\). In the stated computation \(r_s=.0320001\). Set \(\Delta E=E'-E_0\), and define \(\Delta B,\Delta C\) similarly. To avoid confusing norms with entries of the blocks, write \[e_1=\lVert\Delta E\rVert_F,\qquad b_1'=\lVert\Delta B\rVert_F,\qquad c_1'=\lVert\Delta C\rVert_F.\] The chord bound \(|e^{ix}-1|\le |x|\) gives \[ e_1^2+(b_1')^2+(c_1')^2\le\lVert s\rVert^2\le R_s^2. \tag{22}\]

Apply Lemma 14 to \(p=(\overline b_j)_j\) and \(p=(c_i)_i\). Throughout the seed ball keep the resulting frames fixed, and write \[ G_B=B_0^*(B_0B_0^*)^{-1},\qquad G_C=C_0(C_0^*C_0)^{-1},\qquad \operatorname{ran}K_B=\ker B_0,\quad \operatorname{ran}K_C=\ker C_0^*. \tag{24}\] Here \(K_B^*K_B=K_C^*K_C=I_2\). Define \[m_B=\sigma_{\min}(B_0),\quad m_C=\sigma_{\min}(C_0),\quad m=\min(m_B,m_C)>0,\] so that \(\lVert G_B\rVert_{\rm op}=1/m_B\) and \(\lVert G_C\rVert_{\rm op}=1/m_C\). The numerical construction chooses particular coordinate vectors; the ideal frames in this argument use those same choices. The acceptance checks on rank and residual norms certify that this construction is defined. A failed frame check leaves the seed unresolved and never excludes it.

We shall use the orthogonal projections \[ P_K=K_BK_B^*,\qquad P_B=I-P_K=G_BB_0,\qquad P_C=I-K_CK_C^*=G_CC_0^*. \tag{25}\] Finally, put \[ A_0=\lVert E_0\rVert_{\rm op}=\sqrt{2+|1+a|},\qquad A_* =\min(2,A_0+R_s). \tag{26}\] Both \(A_0\) and \(\lVert E'\rVert_{\rm op}\) are at most \(A_*\). Indeed \(A_0\le2\), every entry of \(E'\) has modulus one and hence \(\lVert E'\rVert_{\rm op}\le\lVert E'\rVert_F=2\), and \(\lVert E'\rVert_{\rm op}\le A_0+e_1\le A_0+R_s\).

A unitary associated to every feasible completion

The polar decomposition associates a unitary with a nonsingular square matrix, and its nearest-unitary property in unitarily invariant norms is classical (Fan and Hoffman 1955, Theorem 1); see also (Higham 1986, Theorem 1.1 and Corollary 2.3). Here the compressed completion has an explicit positive defect. The next lemma derives the trace-defect estimate required for the finite \(U(2)\) cover.

The inequality \(q<6\) is checked using outward bounds. In the specified parameter range the stronger bound \(q<.32\) follows from the accepted frame checks and the seed radius; see Section 9. The reduction therefore assigns at least one \(V\in U(2)\) to every feasible completion of an accepted seed ball.

The unitary cells and their Taylor bounds

Fix one cell and denote its midpoint matrix by \(U\). If \(V\) is represented inside the cell, let \[ \theta=(\theta_\alpha,\theta_t,\theta_\beta,\theta_\gamma),\qquad |\theta_j|\le h:=\frac{\pi}{N_u}, \tag{32}\] be its displacement from the midpoint in radians. Denote the midpoint angular differential, applied to this displacement, by \(dU[\theta]\). All four derivatives here are with respect to radian angles, although (31) uses cycle coordinates.

For clarity about the implementation, if the entries of \(U\) are \(U_{ij}\), its alpha derivative is \(iU\), its beta derivative has diagonal entries \(iU_{00},-iU_{11}\) and zero off-diagonal entries, and its gamma derivative has off-diagonal entries \(iU_{01},-iU_{10}\) and zero diagonal entries. The \(t\) derivative differentiates the displayed sine and cosine factors. These are precisely the four angular derivatives assembled by uc::init and uc::initDeriv.

Comparison with a cell center

For the fixed seed and unitary cell define \[ D=D_{\rm span}+D_{\rm ker},\qquad D_{\rm span}=-C_0E_0^*G_B^*,\qquad D_{\rm ker}=\sqrt6 K_C U K_B^*,\qquad Z=D'-D. \tag{34}\] The symbol \(D\) henceforth denotes this comparison block, which need not be entrywise flat. It is not asserted to be the lower block of a Hadamard matrix at the seed center.

A uniform linearization remainder

Let \(E_1,B_1,C_1\) be the seed first variations: at a varied entry, multiply the center entry by \(i\) times the corresponding component of \(s\); all fixed entries have variation zero. Define the linear map \[ \begin{split} \mathcal J(s,\theta)={}& (-C_1E_0^*-C_0E_1^*-DB_1^*)G_B^*\\ &+G_C(-E_0^*B_1-C_1^*D)P_K +\sqrt6 K_CdU[\theta]K_B^*. \end{split} \tag{42}\] This is a necessary linear comparison inferred from the exact orthogonality equations. In particular it is not obtained by assuming that the fixed frames vary differentiably with the seed or that an exact completion exists at every seed center.

Here is the entrywise form used to assemble (42). For \(0\le i,j,k<4\), its shared seed coefficient is \[-c_i\overline{i a(G_B)_{j1}},\] its \(b_k\) coefficient is \[-\big[(G_C)_{i0}+(G_C)_{i1}\overline a\big]\, i b_k(P_K)_{kj} -D_{ik}\overline{i b_k(G_B)_{j1}},\] and its \(c_k\) coefficient is \[-\mathbf 1_{i=k}\,i c_k \big(\overline{(G_B)_{j0}}+\overline{a(G_B)_{j1}}\big) -(G_C)_{i1}\overline{i c_k}(D_{\rm ker})_{kj}.\] For the angular coefficients, if the entries of \(U\) are flattened in row-major order, use \[W_{ij,l}=\sqrt6(K_C)_{i,\lfloor l/2\rfloor} \overline{(K_B)_{j,l\bmod2}},\qquad 0\le l<4,\] and contract with each angular derivative of \(U\). These formulas identify the fixed and moving parts of block::setup, makeD, and makeJ.

Necessary flatness and separating inequalities

We have bounded both the total block displacement \(Z=D'-D\) by \(z\) and its remainder after the linear comparison \(\mathcal J(s,\theta)\) by \(E_r\). We now use these two bounds in the necessary equations \(|D'_{ij}|=1\): the first test uses the total displacement alone, and the second also uses its linear comparison and the seed sum equations.

For the second test define two complex constants and their linear parts by \[\begin{align*} c_X&=(1+a+\textstyle\sum_j b_j)/i,& J_Xs&=a s_a+\textstyle\sum_j b_j s_{b_j},\\ c_Y&=(1+a+\textstyle\sum_i c_i)/i,& J_Ys&=a s_a+\textstyle\sum_i c_i s_{c_i}. \end{align*}\] The corresponding exact row and column sums vanish. Taylor’s formula therefore gives \(c_X+J_Xs+\rho_X=0\) and \(c_Y+J_Ys+\rho_Y=0\), with \[ |\rho_X|\le\frac12R_s^2,\qquad |\rho_Y|\le\frac12R_s^2. \tag{46}\] Take real and imaginary parts of these two equations, in that order. Append the following sixteen real constants and linear forms: \[ c_{ij}=\frac{|D_{ij}|^2-1}{2},\qquad J_{ij}(s,\theta) =\operatorname{Re}\big(\overline{D_{ij}}\mathcal J_{ij}(s,\theta)\big). \tag{47}\] Denote the resulting real constant vector by \(c_{\rm all}\in\mathbb R^{20}\) and the real linear matrix by \(J_{\rm all}\in\mathbb R^{20\times13}\), with its first nine columns corresponding to \(s\) and its last four to \(\theta\).

The implementation stacks exactly these twenty equations in eq. The routine trial::pass proposes directions by regularized linear solves and weight updates. It excludes only when trial::certificate verifies the final inequality. That routine checks finiteness, divides by the largest absolute coordinate, and treats the resulting stored coefficients as the direction. It uses the negative part of the flat weights, as required by (48). No accuracy or convergence assertion about the proposing solves is needed. The used Stage A path is Asearch::testA; the auxiliary Usearch::test and scalar routines do not supply additional exclusion tests for this run. The actual norm and directional comparisons include the margins proved in Section 9.

Finite recursion and unresolved cells

In the stated invocation the base grid is \(N_u=16\). Retained cells are split to \(N_u=32\) and then \(64\) by replacing every bin index \(b_j\) with both \(2b_j\) and \(2b_j+1\). At the first level only the norm test is needed. At \(64\) and deeper, every unexcluded cell is offered to the phase-ball coverage routine; unsuccessful coverage causes all sixteen children to be processed with the same seed and the same fixed frames, using the new value of \(h\). Subdivision is allowed through \(N_u=512\).

A coverage or snapping failure does not exclude a cell. A live cell at the depth cap increments the unresolved count. Exceeding the deeper-node cap of \(1{,}000{,}000\) sets the give-up flag and increments that count; later short returns under that flag cannot restore successful status. A failed frame construction is recorded as a failed seed. The driver records every seed with unresolved cells and returns failure if any seed failed. Thus a negative or global-coverage conclusion requires successful processing of all prescribed seed indices, including all shards, with no failed seed or unresolved cell. Retaining some valid phase balls from an unsuccessful seed does not certify the unprocessed remainder. These conditions are part of the computational obligation, not consequences of the local inequalities alone.

Residual and Root certificates

For a real phase matrix \(P\), define \(F(P)\in\mathbb C^{15}\) by \[ F_{ij}(P)=\frac{1}{2\pi i}\sum_{g=0}^{5}e(P_{ig}-P_{jg}), \qquad 0\leq j<i\leq5. \tag{49}\] Edges are ordered by increasing \(i\), then increasing \(j\); a complex coordinate is stored as its real part followed by its imaginary part. We also regard \(F(P)\) as a real \(30\)-vector. Since every entry of \(e(P)\) has modulus one, \(F(P)=0\) is equivalent to the row Hadamard conditions, and hence to all the Hadamard conditions. Its real derivative \(L_P:\mathbb R^{36}\longrightarrow\mathbb R^{30}\), in complex notation, is \[ (L_Px)_{ij}=\sum_{g=0}^{5}e(P_{ig}-P_{jg})(x_{ig}-x_{jg}). \tag{50}\] The factor \(2\pi i\) from differentiation cancels the denominator in (49). These are the residual and full derivative in buildH::gen, in patchx.cpp.

The first two displacement bounds explain how the certificate will be used. For such a \(\delta\), if \(s_0\geq\|\delta\|\) and \(t_0\geq\|T^*\delta\|\), then nonnegativity of the coefficients of \(n_P\) gives \[\|\delta\|\leq \left(n_P(s_0)^2+(1+\mathtt{ort})t_0^2\right)^{1/2}.\] For a retained completion cell we shall bound both the full displacement and its tangent coordinates. The displayed bound can then improve the radius that covers all exact completions in the cell. The difference bound will compare displacements from two centers during refinement.

Constructing Root certificates

The construction uses an auxiliary real map \(M:\mathbb R^{30}\longrightarrow\mathbb R^{36}\) to turn the residual equation into a bound on \((I-TT^*)\delta\). This map is used only to establish the Root assertions and is not serialized. We first control the nonlinear remainder after applying \(M\).

The use of a numerical factorization followed by a checked Gram defect is a standard device in verified matrix-norm estimation; compare (Rump 2011). The bounds here are derived from the displayed residual identities and the source-specific arithmetic estimates, including the error in the proposed tangent frame.

Transport and alignment of phase balls

Write \[D_0(P)_{ij}=P_{ij}-P_{i0}-P_{0j}+P_{00}.\] For any two real centers \(P,Q\) and any integer matrix \(N\), \[ d=\Pi(D_0(P)-D_0(Q)-N) \quad\Longrightarrow\quad e(Q+d)\text{ is phase-equivalent to }e(P). \tag{65}\] Indeed \(\Pi D_0(P)=\Pi P\); subtracting \(\Pi\) from the identity operator leaves a matrix constant on rows plus a matrix constant on columns. Thus the difference between \(Q+d\) and \(P-N\) is such a rephasing. For every horizontal \(\delta\), the same fixed alignment makes \(e(Q+d+\delta)\) equivalent to \(e(P+\delta)\). This is why a particular choice of integers suffices: no optimality of the wraps is needed. The source’s rounded dephase and wrap operations determine these integer choices, and Section 9 bounds their remaining arithmetic error.

Phase displacements for a retained completion cell

Use the notation of Section 3. In particular \(D\) is the ideal comparison block at the fixed seed and unitary-cell center, \(D'\) is the lower-right block of a feasible exact flat matrix, and \(Z=D'-D\). The certified bounds and linearization are \[\|Z\|_F\leq z,\qquad \|Z-\mathcal J(s,\theta)\|_F\leq E_r,\qquad \|s\|\leq R_s,\quad |\theta_a|\leq h\quad(1\leq a\leq4),\] as in (38), (42), and (43). Here \(s\in\mathbb R^9\) and \(\theta\in\mathbb R^4\) are in radians. Denote by \(\mathcal I_s\) the nine seed positions, whose row-major indices are \[(7,8,9,10,11,13,19,25,31),\] and by \(\mathcal I_D\) the \(16\) lower-right positions \((i,j)\) with \(2\leq i,j\leq5\). The first row and column have zero raw displacement.

The source’s Candidate::prep only attempts this argument when its direction and magnitude checks pass. It uses the stored flat sum \(\mathtt{sum}\) and sets \[\mathtt{slack} =\max(0,\mathtt z^2-\mathtt{sum}+10^{-5})+10^{-10}, \qquad q_d=\mathtt{slack}/\mathtt{mi}+10^{-8}.\] The subtraction \(10^{-6}\) from each computed magnitude gives \(\mathtt{mi}\) and the upper reciprocal \(\mathtt{invmag}_j=1/(\mathtt m_j-10^{-6})+10^{-9}\). The ratio has \(10^{-7}\) added and the final arc quantities each have \(10^{-8}\) added. As proved in Section 9, these numbers have the one-sided properties of Lemma 32 for the ideal comparison block. Failure of any check means failure to cover this cell by this route, not an exclusion of the cell.

Direct and tangent bounds for a cell

Fix a certified Root \(P,T\). Let \(N\) incorporate the particular integer choices made by Root::finish and Candidate::delta, and define the ideal horizontal alignment \[ \Delta=\Pi(P_0-D_0(P)-N). \tag{73}\] By (65), every exact feasible matrix in the cell has an equivalent representation \(e(P+\delta)\), with horizontal \[ \delta=\Delta+\Pi\left(\epsilon+\frac{u}{2\pi}\right). \tag{74}\] The equivalence preserves the extension problem. The computed delta array approximates the particular ideal \(\Delta\); its rounding error is included in the estimates below.

The source’s covercompute::value computes these supports and uses their minimum, with \(+.0001\) before division by \(\pi\). Its \(\mathtt{d2}\) bounds \((R_s^2+\mathtt{arc}^2)/(2\pi)^2\), with \(10^{-8}\) added, and \[\mathtt{s0} =\sqrt{\mathtt{nd}+\mathtt{d2} +(\mathtt{supp}+.0001)/\pi}+.00001.\] Section 9 proves this is an upper bound in (77): it includes the projection error in \(\mathtt{nd}\), support-coefficient error, and \(\epsilon\). An early successful return based solely on this bound is valid.

For a sharper bound put \(\eta=T^*\delta\). The expression obtained by temporarily omitting projection and center correction, in radians, is \[2\pi T^*\Delta+T^*u.\] The total omission has the explicit bound \[ \left\|2\pi\eta-(2\pi T^*\Delta+T^*u)\right\| \leq \mathtt{hor}\sqrt{R_s^2+\mathtt{arc}^2} +2\pi\sqrt{1+\mathtt{ort}}\,\|\epsilon\|. \tag{78}\] Indeed \(T^*(I-\Pi)=((I-\Pi)T)^*\), and \(\|T^*\Pi\epsilon\|\leq\|T\|\|\epsilon\|\).

We next enclose the sum of two linear images of balls by one ellipsoid. This is a standard outer-sum construction in ellipsoidal calculus; see (Kurzhanskiy and Varaiya 2006, sec. 2.2.2, equation (2.16)). The support-function proof below also covers singular shape matrices.

Partition \(X=(X_s,X_\theta)\), and let \(T_s,T_D\) denote the rows of \(T\) restricted to the indicated position sets. From the angle box, \(2\pi T^*\Delta+hT^*X_\theta[-1,1]^4\) is the convex hull of the \(16\) offsets \[ U_\sigma=2\pi T^*\Delta+ h\sum_{a=1}^{4}\sigma_a T^*X_{\theta,a}, \qquad \sigma_a\in\{-1,1\}. \tag{79}\] By Lemma 35 with \(\beta=.45\), the sum of the seed and \(e_D\) contributions to \(T^*u\) lies in an ellipsoid whenever \[ G_{\rm lin}\succeq 1.45R_s^2(T^*X_s)(T^*X_s)^* +(1+1/.45)E_r^2T_D^*T_D. \tag{80}\] The remaining sine error has norm at most \[\left(\max_{j\in\mathcal I_D}\|T_{j,:}\|\right) \mathtt{arc}^3/6.\] There is also a bound using the raw seed and weighted angle balls, with a single offset \(U_0=2\pi T^*\Delta\): \[ G_{\rm dir}\succeq 1.8R_s^2T_s^*T_s+ (1+1/.8)\mathtt{weighted}^2 T_D^*\operatorname{diag}(1/m_j)T_D. \tag{81}\] This is Lemma 35 with \(\beta=.8\). It has no sine-error term because it bounds \(d\) directly.

Let \(\mathcal E(G;\{U_\sigma\})\) denote any certified upper bound obtained from Lemma 36. The preceding arguments give either of the tangent bounds \[\begin{align*} \|T^*\delta\| \leq{}& \frac{\mathcal E(G_{\rm lin};\{U_\sigma\})+ \max_{j\in\mathcal I_D}\|T_{j,:}\|\,\mathtt{arc}^3/6+ \mathtt{hor}\sqrt{R_s^2+\mathtt{arc}^2}}{2\pi} +\sqrt{1+\mathtt{ort}}\|\epsilon\|, \tag{83}\\ \|T^*\delta\| \leq{}& \frac{\mathcal E(G_{\rm dir};\{U_0\})+ \mathtt{hor}\sqrt{R_s^2+\mathtt{arc}^2}}{2\pi} +\sqrt{1+\mathtt{ort}}\|\epsilon\|. \tag{84}\end{align*}\]

Bootstrap and local coverage

The source’s bootstrap uses at most \(30\) updates. It inflates its tangent input by \(.00002\) and its initial radius by \(10^{-6}\), then evaluates (86) with \(10^{-8}\) added at each attempted update. The positive-expression error bounds of Section 9 make each update an upper. When \(k=0\), the mathematical tangent norm is zero; the source’s small positive tangent input is harmless.

Scale failures in ell return \(100\), which makes that tangent path fail bootstrap’s \(t<10\) guard. Its failure sentinel is \(10\). These values cannot pass the local target \(.103\); they are not certificates. The other guard requires \(0\leq\mathtt{init}<3\) and \(\mathtt C<20\). A direct valid \(\mathtt{s0}\) can still establish coverage without either ellipsoid path.

local::test returns success only after a certified covercompute bound for a specific Root fits the target with its final margins. It grows that Root’s recorded radius to cover the bound, adding \(10^{-8}\). Selecting only a few nearby Roots by a heuristic score cannot invalidate this implication. If those fail, snapping merely proposes a new center, which must pass buildH::patch and the same covering computation. Failed snapping or failed coverage does not discard the completion cell: the completion search subdivides it, or records an unresolved seed if its depth or node limit is reached, as described in Section 3.

Merging the global atlas

The implementation in atlas.cpp uses mapH for \(\Phi\). Its two index arrays are genuine permutations. To see this directly in variants, the leading two row indices are distinct and complement supplies precisely the other four. The six column labels remain attached to six distinct integers when their phase keys are sorted and cyclically reordered. The later tail sort and rotation only permute the four remaining row labels. With the transpose flag the lookup is \(6\,\mathtt{col}[j]+\mathtt{row}[i]\), rather than \(6\,\mathtt{row}[i]+\mathtt{col}[j]\); either lookup is a bijection of all \(36\) entries. The sign flag multiplies every entry, and every column of \(T\), by the same sign.

For a finite certified center, canonicalMap obtains at least one callback, so it does not use an uninitialized or degenerate index choice. In each finite pivot list a largest gap is attained and is admitted by the nonnegative tolerance. A list attaining the smallest such largest gap is admitted by the next comparison. Among its five tail scores a maximum is attained and is admitted by the final comparison. The first resulting callback initializes the chosen map. Ties and repeated phase values do not alter the distinct attached labels. The signature used to choose among these maps need not be a canonical invariant.

Atlas::find computes an explicit wrapped dephased difference, projects it, and evaluates its norm. On a successful return it adds \(10^{-7}\) to the computed norm, exceeding the dephasing/projection errors certified in Section 9. Atlas::add then grows the selected radius to at least the incoming radius plus this distance, with another \(10^{-8}\) added and a separate \(2\cdot10^{-8}\)-margin comparison to the cap. This is Lemma 39. It remains valid when an alternative map found by variants supplied the distance; only existence of that allowed map is needed to establish the merge.

If no merge is certified, the source inserts the transformed Root and its original local radius. The hash buckets, pivot selection, and early raw-distance cuts only reduce the opportunities to merge; none removes an input Record. The A atlas uses radius cap \(.125\). Its size cap aborts rather than certifying a discarded Record.

A certified relation between two centers

For the Root at \(P\), denote its stored tangent matrix by \(T:\mathbb R^k\longrightarrow\mathbb R^{36}\) and put \[ \begin{split} o_P&=\mathtt{ort}_P,\qquad \alpha_P=\mathtt{id}_P,\qquad \gamma_P=\mathtt C_P,\\ \mu_P&=\mathtt{mnorm}_P,\qquad \varepsilon_P=\mathtt{froot}_P,\qquad n_P(s)=\mathtt{n0}_P+\alpha_Ps+\gamma_Ps^2. \end{split} \tag{88}\] All these constants are nonnegative. We use the same notation, with subscript \(Q\), for a second certified Root with center \(Q\) and tangent matrix \(S:\mathbb R^{k_Q}\longrightarrow\mathbb R^{36}\). In particular, \[ \|T^*T-I\|\leq o_P, \qquad \|S^*S-I\|\leq o_Q, \qquad \|F(Q)\|\leq\varepsilon_Q. \tag{89}\] We will apply the normal and difference inequalities (53) and (55).

The following elementary identity explains why approximate, rather than exact, orthogonality is sufficient throughout the construction.

Let \(D_0\) be the unwrapped dephasing operator, \[(D_0X)_{ij}=X_{ij}-X_{i0}-X_{0j}+X_{00}.\] Choose any integer matrix \(N\) and define \[ d_q=\Pi\bigl(D_0Q-D_0P-N\bigr),\qquad \eta_q=T^*d_q,\qquad n_q=\|A d_q\|. \tag{91}\] The implementation chooses \(N\) by wrapping differences of cached dephased entries. The chosen lift need not minimize any distance. Indeed, \(D_0X-X\in\ker\Pi\), so \[Q-P-d_q\in N+\ker\Pi.\] Vectors in \(\ker\Pi\) are row and column rephasings. Consequently \(P+d_q\) and \(Q\) differ only by integer phases and rephasings.

Fix a parent radius \(R\) and an exact solution displacement \(\delta\in\mathcal V\) with \(\|\delta\|\leq R\). Set \[ \eta=T^*\delta,\qquad h'=\delta-d_q,\qquad d=\|h'\|,\qquad \xi=T^*h'=\eta-\eta_q,\qquad \nu=Ah'. \tag{92}\] Both \(d_q\) and \(h'\) are horizontal. Moreover \(Q+h'\) is equivalent by the same rephasing to \(P+\delta\), and therefore is exact. Thus the Root estimates at both centers apply to this one solution.

The coefficient \(\sigma\) has a direct small-matrix certificate. With \(W=(AS_h)^*\), its row Gram is \[ G=WW^*=S_h^*A^2S_h, \qquad \|S_h^*A\|^2=\|G\|. \tag{99}\] The code constructs these rows by projecting each child tangent column and subtracting its components against the parent columns, in that order. A certified upper bound for the norm of \(G\), followed by a square root, gives (94). For any exact real symmetric \(G\), either of the quantities \[\max_i\sum_j|G_{ij}|, \qquad \sqrt{\|G^2\|_F}\] bounds \(\|G\|\): the first is the symmetric absolute-row bound, while \(\|G\|^2=\|G^2\|\leq\|G^2\|_F\) proves the second. The routine spectralUpper uses their minimum with margins for arithmetic and Gram perturbation, detailed in Section 9. When \(k_Q=0\), the operator is zero and the code sets \(\sigma=0\).

Distance iteration and the searched tangent radius

The relation estimates yield a useful upper iteration without requiring either contraction or a fixed-point theorem. For fixed \(t\), write \[ \begin{split} z&=\sqrt{1+o_P}\,t,\\ v(b)&=\min\{v_0,(1+o_P)b,\lambda b+e_0\},\\ \psi_P(b)&=\sqrt{z^2+v(b)^2},\\ \psi_Q(b)&= \sqrt{(1+o_Q)(\beta t+\sigma v(b))^2+n_Q(b)^2}. \end{split} \tag{100}\] Start at \[ b_0=\min\{D,\sqrt{z^2+v_0^2}\} \tag{101}\] and replace \(b_j\) by \[ b_{j+1}=\min\{b_j,\psi_P(b_j),\psi_Q(b_j)\}. \tag{102}\]

The routine relationB::eval implements this argument with at most 30 attempted improvements. It accepts \(0\leq t\leq2\) and otherwise returns the non-success sentinel \(10\), which exceeds every radius used here. On the accepted path it first enlarges \(t\) by \(2\cdot10^{-8}\), adds \(10^{-9}\) to the parent tangent factor, and uses \(10^{-8}\)-scale enlargements in the initial distance, normal, child-tangent and updated distance bounds. A proposed value that does not improve the current upper bound ends the iteration. Section 9 verifies these enlargements, the bounds computed in init, and the final \(10^{-8}\) addition against the separate binary64 operations. Denote the resulting computed function by \(\widehat D(t)\). Its required semantic property is the conclusion of Lemma 43: \[ \|\eta-\eta_q\|\leq t \quad\Longrightarrow\quad \|\delta-d_q\|\leq\widehat D(t) \qquad(0\leq t\leq2). \tag{103}\] The proof of this property consists of the preceding induction plus the explicit arithmetic bounds; the numerical snapping or eigen-iterations are not premises of that induction.

There are two ways to use (103). One may evaluate it at the farthest tangent distance of a particular box. Alternatively, for a queried sphere radius \(0\leq a\leq .126\), init searches for a useful tangent-distance threshold \(\rho\). The search begins with \(\ell=0\) and \(u=1.01a\), rejects if \(\widehat D(0)>a-10^{-7}\), and makes 25 midpoint trials. A trial \(m\) replaces \(\ell\) precisely when \[ \widehat D(m)<a-2\cdot10^{-7}; \tag{104}\] otherwise it replaces \(u\). Finally the code sets \[ \rho=\max(0,\ell-10^{-8}) \tag{105}\] and reports a usable relation only if \(\rho>10^{-7}\).

For a previously completed parent used as a blocker, \(a\) is its fixed input radius and this lemma suffices. For an atlas child, the search uses the allowed cap \(a=\tau\), not merely its current radius. When boxes are assigned to that child, the code evaluates \(\widehat D\) again at an upper tangent distance for those boxes and grows the stored radius to that certified distance, with an additional margin. It checks both that the tangent argument is at most \(\rho\) and that the new radius is at most \(\tau\). Failure of either check aborts. Thus even an unfavorable rounded reevaluation cannot silently assign a box to a sphere too small to contain it.

An exhaustive grid in tangent coordinates

For every solution in the parent record, \[ \|\eta\|=\|T^*\delta\| \leq\sqrt{1+o_P}\,R=:E_P. \tag{106}\] Let \(w>0\) be the stored refinement width, regarded as an exact real number. The code forms an inflated upper bound \(E\) for \(E_P\) by adding \(10^{-7}\) to the computed right side of (106), and chooses \[L=\left\lceil E/w+0.500001\right\rceil, \qquad n=2L+1,\] with the stated rounded evaluation. The error bounds in Section 9 ensure that the resulting outer endpoints \(\pm(L+1/2)w\) contain \([-E_P,E_P]\).

For \(u\in\mathbb R^k\) and \(h\geq0\), write \[ B(u,h)=\prod_{a=1}^k[u_a-h,u_a+h]. \tag{107}\] The base boxes have \(u_a=b_aw\), \(-L\leq b_a\leq L\), and \(h=w/2\). Their union contains \([-E_P,E_P]^k\), so every tangent vector in (106) belongs to at least one base box. All intervals are closed; grid boundaries are included.

The minimum squared distance of a box from the origin is \[ \operatorname{dist}(0,B(u,h))^2 =\sum_{a=1}^k\max(0,|u_a|-h)^2. \tag{108}\] The routine outside uses a lower version of this expression, subtracting \(10^{-8}\) inside each nonnegative part, and compares with the inflated \(E^2\). Hence an accepted outside test means that the box cannot contain the tangent vector of a parent solution. Stored centers are approximations to the exact multiples of \(w\); repeated subdivision centers are interpreted as exact dyadic offsets from this same grid. The coordinate and arithmetic errors, bounded in Section 9, are covered by these margins.

Subdivision is exhaustive because \[ B(u,h)=\bigcup_{\epsilon\in\{-1,1\}^k} B(u+\epsilon h/2,h/2). \tag{109}\] The code visits all \(2^k\) children if they need to be examined; their common boundaries remain covered. When \(k=0\), the empty product (107) is the single point of \(\mathbb R^0\), so there is one base box and no subdivision is needed or permitted.

The routine corner adds \(10^{-8}\) after the computed norm to obtain such an upper \(t_B\). The multi-box routine markRec uses the same geometric fact on entire base boxes. At each coordinate it enlarges \(|b_aw-\eta_{q,a}|+w/2\) by \(10^{-8}\), accumulates its square, and keeps a branch only while the partial sum is at most \((\rho-5\cdot10^{-8})^2\). After a complete box is marked, the bound used for radius growth is the accumulated norm plus \(2\cdot10^{-8}\), or the maximum of these bounds when several boxes are marked. The coordinate inflations make this a true farthest-distance upper, while the gap between \(5\cdot10^{-8}\) and \(2\cdot10^{-8}\) keeps it below \(\rho\) after rounding. At \(k=0\) the marked bound is \(2\cdot10^{-8}\), also smaller than every usable \(\rho\). The detailed error comparison is given in Section 9.

In particular, a relation discovered while solving a proper subbox does not justify marking its base box merely because that subbox is covered. A mark is made only after the independent whole-base-box test just described. Integer coordinate ranges and hash neighborhoods only limit which marking or reuse attempts are made. Any unmarked box remains in the ordinary exhaustive traversal.

Assignments, symmetry maps, and radius growth

Let \(\tau\) be the common cap on child radii. The atlas stores a list of certified Roots \(Q_i\) with current radii \(r_i\leq\tau\). Its centers, tangent columns and certificate constants remain fixed after insertion; only \(r_i\) may grow.

For a live box, the program may propose a new center by snapping a matrix near \(P+Tu\). This is only a method of proposing a Root. It does not assert that \(P+Tu\) is exact, that snapping converges, or that the tangent coordinates describe a smooth locus. A proposal must pass the independent Root certificate and the parent–child relation test. If \(t_B\) is the box’s corner bound, the direct path uses \(r=\widehat D(t_B)+2\cdot10^{-8}\) and requires \(r<\tau-10^{-7}\) before assignment.

The function assign implements this triangle argument. For a merge it requires \(r+\ell+2\cdot10^{-8}<\tau\) and grows the old radius to the maximum of its present value and \(r+\ell+10^{-8}\). These margins are certified in Section 9. If no merge succeeds, it inserts the canonical transformed Root with radius \(r\). The returned map is the one used in the successful merge, or the canonical map in the insertion case; no assertion that the search found the nearest atlas center is needed.

For subsequent reuse, inverseTransform pulls the selected atlas Root \(Z\) back to \(\Phi^{-1}Z\). This is a signed permutation of its stored phase and tangent coefficients, with its constants unchanged, as justified by Lemma 31. The pulled-back Root and \(Z\) have isometric solution spheres. A fresh relation to \(\Phi^{-1}Z\) may therefore grow the radius stored at \(Z\). Any integer or rephasing alignment needed for that fresh relation is chosen anew in (91). A failure of this optional addNear step cannot invalidate the already established direct assignment.

Preloading also permits a map to be applied to the parent. This does not change the coordinates labeling its boxes. Indeed, for \(V=\Phi P\), the transported tangent matrix and displacement satisfy \[ (\Phi T)^*(\Phi\delta)=T^*\delta=\eta. \tag{111}\] Thus a relation from the parent Root at \(V\) to a stored child or blocker can be used on the same grid indices. The represented matrices change only within their permitted equivalence classes. Trying a limited collection of maps, omitting hash neighbors, or applying an early distance cutoff can only omit possible reuse certificates; none of these operations declares a box covered by itself.

Successful parents and the blocker induction

A blocker is an earlier input parent whose entire refinement has succeeded. It is queried at its original fixed radius. In contrast, an atlas child is queried directly as a certified-center sphere and its radius is grown when needed. This distinction is important: a child created during an unfinished parent search can already be reused, whereas that unfinished parent cannot be used as a blocker.

This proof involves two finite inductions: one on subdivision depth and one on the order of completed parents. It does not infer coverage of a parent from children that merely assume coverage of that same parent. Moreover, later radius growth cannot invalidate an earlier certificate, because centers and Root constants are immutable and the corresponding solution sets only enlarge.

Batch files and finite failure conditions

Batching writes appended atlas Roots in their insertion order, in groups of at most 256. The radius written for each Root is the common cap \(\tau\), rather than its current achieved radius. If a Root at index \(i\) is emitted before the run ends, every later state satisfies \[ r_i\leq\tau, \qquad\mathcal S(Q_i,r_i)\subseteq\mathcal S(Q_i,\tau), \tag{113}\] with exactly the same center, tangent columns and certificate constants as in its batch. No future merge changes these data. At successful completion, the final partial batch and the count marker account for every appended index. Consequently replacing the child union in (112) by the union of all batch spheres at radius \(\tau\) is valid.

Each batch is completed under a temporary filename before atomic rename. Downstream computation may read these completed files while Stage B continues, but the final conclusion still requires the complete batch collection and the final Stage B failure checks. The existence of an intermediate batch, or even a count marker without the exit and bad-list checks, is not a certificate that all parents were covered. The exact execution protocol is specified in Section 7.

For clarity, the implementation uses the following finite limits. Input radii satisfy \(0\leq R\leq0.126\), the child cap and width satisfy \[0.0001\leq\tau\leq0.126, \qquad 0.0001\leq w\leq0.05, \qquad 0\leq k\leq10.\] The normal constants are nonnegative and are checked against \[\gamma_P<20,\quad \mathtt{n0}_P,\varepsilon_P<10^{-6},\quad \alpha_P<10^{-4},\quad o_P,\mathtt{hor}_P<10^{-5},\quad \mu_P<2.\] Stored phase entries have magnitude at most \(4\), and stored tangent entries at most \(1.01\). These range checks accompany genuine Root certificates; the range checks alone do not establish those certificates. A prospective Root with more than ten tangent columns is rejected, not truncated.

The base grid is limited to \(50{,}000{,}000\) boxes, subdivision depth is at most six, and the atlas is limited to \(2{,}000{,}000\) Roots. A single Record file is limited to \(2{,}000{,}000\) records and the combined input to \(8{,}000{,}000\). The grid product is checked before multiplication past its limit. Within the admitted ranges one has \(L\leq1262\); the mixed-radix indices fit the stated integer types, and every split uses at most \(2^{10}\) children. The integer and floating-point bounds are recorded in Section 9.

Exceeding the grid limit fails the parent. An unresolved cell at the depth limit, or an unresolved cell with \(k=0\), also fails it. Invalid input, impossible radius updates, exhausted atlas capacity and file errors abort the run. An unsuccessful proposal or relation can lead to subdivision or failure, but never directly to a discard. In particular, the clipped alignment tests in relationB::init only decline a relation: their chosen cut is at most \(0.249\) in the direct-proposal path and at most \(0.23\) in ordinary reuse. They are not exclusions of parent solutions.

The invocation parameters used for the three prescribed refinement passes are respectively \[(\tau,w)=(0.07,0.013),\qquad (0.016,0.005),\qquad (0.011,0.0038).\] The second pass uses batching; the third is applied to the records retained by the first exclusion pass. These choices affect whether the finite search succeeds, but not Proposition 47. The proposition is an algorithmic implication and does not assume any claimed run counts, hashes, or generated data. Establishing that its successful-completion hypothesis was met for the required records is a separate execution obligation, addressed in Section 7.

The common Hadamard displacement

Fix a Record with center \(P\in\mathbb R^{6\times6}\), radius \(0\le r\le .03\), and real tangent matrix \(T\in\mathbb R^{36\times k}\), where \(0\le k\le10\). Recall \(e(t)=\exp(2\pi i t)\), and write \(A=e(P)\) entrywise. The root certificates of Section 4 supply \[ \|T^*T-I\|\le\omega,\qquad \|F(P)\|\le f_0<10^{-6},\qquad 0\le\omega<10^{-5}, \tag{114}\] where \[F_{ij}(P)=\frac{1}{2\pi i}\sum_g e(P_{ig}-P_{jg}),\qquad i>j.\] For every horizontal \(\delta\) with \(\|\delta\|\le r\) such that \(e(P+\delta)\) is Hadamard, those certificates also give \[ \eta=T^*\delta,\quad \nu=\delta-T\eta,\qquad \|\eta\|\le r_H:=\sqrt{1+\omega}\,r,\qquad \|\nu\|\le n:=n_0+\iota r+\Gamma r^2. \tag{115}\] Here \(\omega,n_0,\iota,\Gamma\) are respectively the stored certificate constants ort, n0, id, and C. The admitted ranges include \(0\le n_0<10^{-6}\), \(0\le\iota<10^{-4}\), and \(0\le\Gamma<20\). The tangent bound in (115) follows already from (114); the normal bound is the certified root estimate. In particular, no exact orthonormality of the stored columns of \(T\) is assumed.

Throughout this section the first two bases are the coordinate basis and the columns of \(e(P+\delta)/\sqrt6\). If further bases exist, they share this one displacement \(\delta\) and hence this one \(\eta\). Each vector unbiased to the coordinate basis is of the form \(e(\beta)/\sqrt6\). Its global phase may be chosen so that \(\beta_0=0\), and its other five phases may then be lifted to \([0,1]\). Further changes of a vector’s global phase, made independently for different vectors below, do not change the common Hadamard displacement.

The single-vector sums use a uniform operator bound. The identity \[\|AA^*-6I\|_F=2\pi\sqrt2\,\|F(P)\|\] and (114) imply \[ \|A/\sqrt6\|_{\mathrm{op}} \le \sqrt{1+\frac{2\pi\sqrt2}{6}f_0}<K, \qquad K:=1.00001. \tag{116}\]

Closed phase bins and single-vector inequalities

At resolution \(M\), the five variable phases are covered by the closed intervals \([b/M,(b+1)/M]\), \(0\le b<M\). The phase \(1\) represents the same point as \(0\), so this includes every torus boundary. Let \(u\) be a bin midpoint, with \(u_0=0\), and let \[a=\frac1{2M},\qquad d_0=0,\quad |d_j|\le a\ (j>0),\qquad x=d-\frac16\Bigl(\sum_jd_j\Bigr)\mathbf1.\] Up to global phase the vector in this bin has phases \(u+x\).

For a center \(u\), index the Hadamard columns by \(i\) and vector coordinates by \(j\), and define \[ q_{ji}=\frac{e(u_j-P_{ji})}{\sqrt6},\qquad S_i=\sum_jq_{ji},\qquad S'_i=\sum_jq_{ji}e(x_j-\delta_{ji}). \tag{118}\] The necessary unbiasedness equations are \(|S'_i|=1\) for every \(i\). The map \(Qw=(\sum_jq_{ji}w_j)_i\) has the same operator norm as \(A/\sqrt6\): conjugation, transposition, and multiplication by diagonal unitaries preserve the relevant norm. Thus (116) also bounds \(Q\).

For the sharper tests introduce real arrays \[ c_i=\frac{|S_i|^2-1}{4\pi},\qquad J_{ij}=-\operatorname{Im}(\overline{S_i}q_{ji}),\qquad B_{ik}=\sum_j J_{ij}T_{(j,i),k}. \tag{121}\] In particular \(\sum_jJ_{ij}=0\). For \(y\in\mathbb R^6\) put \[G_y:=\max_j\left|\sum_i y_i\overline{S_i}q_{ji}\right|, \qquad N_y:=\left(\sum_{i,j}y_i^2J_{ij}^2\right)^{1/2}.\] The product \(S\circ y\) denotes componentwise multiplication.

There is also a useful scalar test before the tangent decomposition. Set \(S_{\max}=\max_i|S_i|\), and for a bin write \(X=X_M\), \(L=L_M\), \(I=I_M\). Unbiasedness requires \[ |c_i|\le a\sum_{j>0}|J_{ij}|+r\|J_{i,:}\|+\rho, \tag{125}\] where \[\begin{align*} \rho=\min\Bigl\{& \pi\bigl[(KX+r)^2+ S_{\max}\bigl(KIX+(2Xr+r^2)/\sqrt6\bigr)\bigr],\\ &\pi\bigl[(L/\sqrt6+r)^2+ S_{\max}(X+r)^2/\sqrt6\bigr]\Bigr\}. \end{align*}\] The first remainder bound follows from the proof of Lemma 51 with a coordinate direction and without decomposing \(\delta\). For the second, use the scalar increment bound in (119) and apply the second-order exponential bound directly to \(x-\delta_{:,i}\), whose norm is at most \(X+r\). The full Hadamard linear term is supported by \(r\|J_{i,:}\|\), so no normal-error term is added in (125).

The routine Layer::test applies (120), (125), and then (124) for proposed directions \(y\). In the last test it forms \(J^*y\) and the real companion sums \(\sum_i y_i\operatorname{Re}(\overline{S_i}q_{ji})\). The Euclidean norm of this pair of real sums is exactly the coefficient magnitude defining \(G_y\). Directions may be proposed by an inexact linear solve: the inequality holds for every real \(y\), so the proposal method is immaterial. The implementation checks that its proposal is finite with maximum absolute entry strictly between \(10^{-100}\) and \(10^{100}\), then normalizes by that maximum. The resulting stored coefficients themselves are the test direction.

From bins to closed vector balls

The initial resolution is \(M=12\). Every bin is tested, and every retained bin is split into all \(2^5=32\) children at each doubling \(12\to24\to48\to96\). On one coordinate the child indices are \(2b\) and \(2b+1\), whose closed intervals cover the parent interval exactly. An actual vector therefore follows at least one surviving bin path, including when a phase lies on a bin or torus boundary. Exceeding the cap of \(2{,}000{,}000\) retained bins is an unresolved outcome, never an exclusion.

For \(v\in\mathbb R^6\) and \(s\ge0\), define the closed vector ball \[ \mathcal B_{\mathrm{vec}}(v,s)= \left\{\frac{\lambda e(v+x)}{\sqrt6}: |\lambda|=1,\ x\in\mathbb R^6,\ \sum_jx_j=0,\ \|x\|\le s\right\}. \tag{126}\] The retained final bins are compressed into balls of this form. The required covering property does not depend on the quality of the clustering heuristic.

For the specified invocation, the heuristic radius parameter is \(.042\) and there are two assignment iterations. With \(w=1/M\) the candidate threshold is \((.042-1.11w)^2\), and the coordinate cutoff is the square root of twice that threshold plus \(10^{-10}\). These constants affect only the choice of assignments; the proof is the final radius update in Lemma 52. In particular it does not assume that the selected wrapped lift minimizes torus distance.

Necessary edge tests

Take two distinct balls with centers \(u,v\) and radii \(s_u,s_v<.1\). For actual representatives with displacements \(x_u,x_v\) as in (126), set \[ Q_j=e(u_j-v_j),\quad S=\sum_jQ_j,\quad z=x_u-x_v,\quad r_e=s_u+s_v, \qquad \|z\|\le r_e. \tag{127}\] The actual unscaled inner product is, up to conjugation and global phase, \(S' =\sum_j Q_je(z_j)\). Since \(|S'-S|\le2\pi\sqrt6\,r_e\), necessary direct tests for orthogonality (\(\mathcal O\)) and unbiasedness (\(\mathcal U\)) are \[ \frac{|S|}{2\pi\sqrt6}\le r_e\quad(\mathcal O),\qquad \frac{\bigl||S|/\sqrt6-1\bigr|}{2\pi}\le r_e\quad(\mathcal U). \tag{128}\] Define the real matrix \(D_{\mathcal O}\in\mathbb R^{2\times6}\) and the row \(D_{\mathcal U}\in\mathbb R^{1\times6}\) by \[ (D_{\mathcal O})_{:,j}= \begin{pmatrix}-\operatorname{Im}Q_j\\ \operatorname{Re}Q_j\end{pmatrix}, \qquad (D_{\mathcal U})_j= \frac{\operatorname{Re}S\,(D_{\mathcal O})_{1j} +\operatorname{Im}S\,(D_{\mathcal O})_{2j}}6. \tag{129}\]

The joint test with one tangent variable

For each ball \(t=0,1\), form \(c^t,J^t,B^t,S^t\) from (118) and (121) at its actual center. Write its radius as \(s_t\) and let \[\begin{align*} \mathcal E_t^{\mathrm{ball}}(y):={}&n \left(\sum_{i,j}y_i^2(J^t_{ij})^2\right)^{1/2}\\ &+\pi\Biggl[ \|y\|_\infty(Ks_t+r)^2 +s_t^2\max_j\left|\sum_i y_i\overline{S_i^t}q^t_{ji}\right| +\frac{2}{\sqrt6}\|S^t\circ y\|s_tr +\frac1{\sqrt6}\|S^t\circ y\|_\infty r^2\Biggr]. \tag{134}\end{align*}\] This is the estimate proved in Lemma 51, using \(X=s_t\) and only the first pure-\(x\) remainder bound. In particular, it is valid on the whole closed Euclidean vector ball.

For an edge type \(E\in\{\mathcal O,\mathcal U\}\), write \(\ell=2\) or \(1\), respectively, and use \(D_E,q_E,E_E\) from Lemma 54.

This is the comparison implemented by graph::joint. It first calls single::support with a zero vector-displacement coefficient array for each ball, and only afterwards adds the edge derivatives. Thus the maximum coefficient in (134) is formed from the pure single-vector remainder; it cannot be decreased by cancellation with an edge coefficient. The tangent coefficient array, in contrast, is shared and accumulates both \(-(B^t)^*y_t\) contributions before its norm is taken. As with the single-vector test, the linear solve and its weights only propose normalized directions; validity depends solely on (135) for the proposed direction.

The inequalities just proved are necessary in exact real arithmetic. In the implementation, each rejection is a strict violation of an outward-enlarged bound; equalities and unresolved comparisons retain the candidate. Sections 9.10 and 9.11 certify these comparisons, whose margins are listed in Section 6.7 below. Thus every genuine pair retains its required relation when the tests are evaluated numerically.

Exact graph exclusion

Make one vertex for each retained ball. Join two distinct vertices by an \(\mathcal O\) edge if their orthogonality type has not been excluded by its direct and joint tests. Define \(\mathcal U\) edges similarly for unbiasedness. Both graphs are undirected and have no self-loops. Every genuine pair retains its corresponding edge by the preceding lemmas. Extra edges are harmless: retained pairwise possibilities need not have a simultaneous realization.

By Lemmas 52 and 53, two additional mutually unbiased orthonormal bases would give disjoint vertex sets \(A,B\) satisfying \[ |A|=|B|=6,\qquad A,B\text{ are $\mathcal O$-cliques},\qquad A\times B\subseteq E(\mathcal U). \tag{136}\] The following finite search tests this necessary configuration.

Figure 2 displays the required pattern. Every edge means that its necessary tests survived; the search asks whether even these permissive graphs contain the pattern.

The graph has at most \(2048\) vertices and is represented by \(32\) unsigned 64-bit words per adjacency set. Only valid vertex indices are inserted, all unused bits are zero, and intersections and cardinalities are exact integer operations. A least-set-bit operation is called only on a nonempty set. Thus the finite-set operations in the preceding proof are the operations performed by the code. The specified search uses mode \(1\) and a cap of \(5{,}000{,}000\) steps.

Conservative arithmetic and invocation

We finish by specifying the outward replacements and comparison margins that connect the necessary inequalities to the implemented certificate. Their arithmetic justification is in Sections 9.10 and 9.11.

For a bin the source forms its halfwidth with a \(10^{-12}\) increase, then increases each of \(X_M,L_M,I_M\) by a further \(10^{-12}\) after the indicated multiplication. The stored tangent and normal bounds are formed as \[\widehat r_H=\sqrt{1+\omega}\,r+10^{-9},\qquad \widehat n=n_0+\iota r+\Gamma r^2+10^{-9}.\] The upper scalar squared-magnitude threshold in (120) is increased by \(2\cdot10^{-7}\), and its lower threshold, when \(\tau<1\), is decreased by that amount. The combined squared-distance threshold, the right side of (125), and the right side of (124) each receive a \(2\cdot10^{-7}\) comparison allowance.

For a pair, the radius sum is increased by \(10^{-10}\). The distance tests (128) permit a further \(2\cdot10^{-7}\) on that radius. Both edge residual bounds \(E_{\mathcal O}\) and \(E_{\mathcal U}\) are increased by \(2\cdot10^{-8}\); the direct comparisons (132) and (133) receive another \(2\cdot10^{-7}\). The right side of the joint comparison (135) receives \(3\cdot10^{-7}\). Cluster assignment radii include the \(10^{-9}\) allowance already described in Lemma 52.

The bounds \(|P_{ij}|\le4\) and \(|v_j|\le2\) keep all trigonometric arguments used here within the guarded range of expair. The proof of Section 9 includes the errors in these arguments, in \(q,S,c,J,B\), in the short weighted sums and norms, and in the positive support expressions. Inexact solution of the proposal systems supplies no separate assumption.

For clarity, the invocation parameters used for this certificate are 12 4 1 .042 1 1 5000000: initial resolution \(12\), four bin layers, one proposed bin direction, clustering parameter \(.042\), one proposed joint direction, graph mode \(1\), and the stated graph work cap. The two Lloyd iterations are the fixed default. The conclusion of Proposition 57 is conditional on a completed negative result for the individual Record; no collection of unexecuted tests is itself such a result.

Programs, records, and machine arithmetic

The accompanying verification/code/ directory contains the seven unchanged source files seed.cpp, covout.cpp, ub.cpp, patchx.cpp, atlas.cpp, stageB.cpp, and stageC.cpp. Their byte lengths and full SHA-256 digests are listed in verification/code/extraction.json. The source hashes were checked before the recorded run, and the packaged copies match those same bytes. Only four translation units are built as entry points:

The other files are included through the macros in these translation units. Their standalone sample drivers are not executed. In particular, A uses Asearch, and C uses graph search mode 1.

A serialized Record contains a certified Root and a radius \(r\). Its interpretation is the set of exact Hadamard solutions represented, up to the equivalences of Section 2, by \(e(p+h)\) with horizontal \(h\) and \(\|h\|\le r\). The stored \(p\) need not itself be an exact solution. The Root data justify the normal-displacement inequalities on this set; their construction is part of Section 4.

The binary format is explicit. A file begins with an eight-byte unsigned record count. Each record consists, in order, of a four-byte signed integer \(k\), 36 binary64 entries of \(p\), \(k\) rows of 36 binary64 entries of \(T\), and the eight binary64 values \[C,\ n_0,\ \mathrm{id},\ \mathrm{ort},\ \mathrm{hor},\ \mathrm{mnorm},\ \mathrm{froot},\ r.\] Thus a record occupies \(356+288k\) bytes, and a valid zero-count file is exactly eight bytes. The platform is little endian. No phase data are converted to decimal between stages. The evidence checks parse every record, validate finite bounded fields, and require the declared count to reach the exact end of file. They also check that every saved C failure is an unchanged, ordered subsequence of its assigned inputs.

The recorded platform was x86-64, Intel Xeon Platinum 8573C, Ubuntu GCC 13.3.0, and glibc 2.39. The builds, prepared on the same UTC date before the run, were

g++ -O3 -march=native -ffp-contract=off covout.cpp -o covrun
g++ -std=gnu++17 -O3 -march=native -ffp-contract=off atlas.cpp -o arun
g++ -std=gnu++17 -O3 -march=native -ffp-contract=off stageB.cpp -o brun
g++ -std=gnu++17 -O3 -march=native -ffp-contract=off stageC.cpp -o crun

The first command used this compiler’s default GNU C++17 dialect. The arithmetic assumptions are binary64, round to nearest, separate operations without contraction or fast-math reassociation, correctly rounded binary64 square root, masked floating-point exceptions, and neither flush-to-zero nor denormals-are-zero. Separate probes compiled with the cover and A/B/C flag sets both passed and recorded FLT_EVAL_METHOD=0, 32-bit int, 64-bit size_t, 64-bit uint64_t equal to unsigned long, eight-bit bytes, and MXCSR 0x1f80. Both probes recorded nearest rounding on entry and during the check, and passed the square-root and gradual-underflow samples. These probes and the program checks provide limited evidence for the stated platform conditions, not a proof of all primitive-operation or compiler semantics. Those semantics remain assumptions; Appendix 9 supplies the numerical bounds under them. The retained build/build-manifest.json identifies the exact sources, binaries, compiler commands, probe outputs, and arithmetic evidence.

One additional code-generation condition is needed by coverSeeds::run: both pow(…,2) expressions must be lowered to the binary64 multiplications analyzed in Appendix 9. For the actual covrun, inspection of the saved disassembly finds the scale multiplication, its square, subtraction, square root, addition, and second square at hexadecimal addresses 6035, 6039, 603d, 605c, 606d, and 608b, respectively. There is no dynamic pow symbol. Absence of that symbol alone would not establish the required instruction sequence. The recorded binary is identified by its full SHA-256 digest, so this check applies to that build. The specified lowerings address only this code-generation condition, not the full arithmetic model itself. A new build requires this check again. Its binary hash, like any native build hash, need not equal that of the recorded binary.

Specified finite control flow

All invocations use the C numeric locale and fresh output paths. The cover is run to normal completion before A reads its output. A uses all four parts \(i=0,1,2,3\) with parts=4; part \(i\) processes exactly the center indices congruent to \(i\) modulo 4. Its constants are seed radius .0320001, local target .103, global target .125, levels=3, iters=2, and first=1.

The following are the program invocations, with \(i\) and \(j\) standing for the indicated shard and batch indices. The accompanying verification/code/proof_run.py runner was used in this execution and performs the validation between stages; this display only specifies the program arguments. A separate bounded supervisor retained the runner’s exit and process-cleanup record.

export LC_ALL=C
./covrun centers.txt
./arun centers.txt i 4 coarsei.bin badi.txt
./brun .07 .013 mid.bin midbad.bin - \
  coarse0.bin coarse1.bin coarse2.bin coarse3.bin
./brun .016 .005 fine.bin finebad.bin batches/f mid.bin
./crun 12 4 1 .042 1 1 5000000 0 1 \
  batches/badj.bin batches/fj.bin
./brun .011 .0038 fb1.bin fb1bad.bin - ALL_NONEMPTY_C_BAD_FILES
./crun 12 4 1 .042 1 1 5000000 i 4 fb1cbadi.bin fb1.bin

There is one initial C invocation for every batch named by the completed batches/fdone.txt marker. In C the first seven parameters mean initial grid \(12\), four layers, one linear-support iteration, proposed cluster radius \(.042\), detail 1, graph mode 1, and graph-step cap \(5{,}000{,}000\). Thus the single-vector grids are \(12,24,48,96\). The unchanged default number of clustering passes is two.

The mid and fine B invocations are sequential. A batching B invocation writes consecutive groups of at most 256 atlas records, replacing each batch radius by its target \(.016\), and atomically renames each completed batch. The checked concatenation of all batch records equals fine.bin, except for that radius replacement. Every original fine radius is at most \(.016\), so the replacement enlarges the represented sets. The completion marker agrees with both the number of batches and the sum of their record counts. The recorded run waited for B fine to finish before starting C; it used up to sixteen independent C workers. Concurrency changes scheduling only: workers have distinct output files and do not share mutable search state.

For every initial C process, the normal status is 0 exactly when its saved bad count is zero, and 1 exactly when that count is positive. The four reported failure categories—uncapped graph candidate, graph-step cap, bin overflow, and clustering failure—sum to that bad count. None of them is an exclusion. Every nonempty-count bad file is passed to B fallback in C-locale filename order, including failures whose locations differ from those in another run. Final C uses all four modulo-4 parts of the fallback output. If initial C has no bad records, fallback and final C are unnecessary; that shortcut was not used in the recorded run.

The required terminal conditions are:

1. successful builds, a normally completed cover, and a complete center file;

2. four A exits 0, all assigned centers processed, terminal failedBalls=0, and four empty bad text files;

3. both B exits 0, all input parents processed, agreement of logged and saved output counts, and zero-count B bad files;

4. every initial C batch processed exactly once with consistent exit, done count, bad count, and saved records;

5. every initial C bad record included in fallback, fallback exit 0 with all parents processed and zero saved failures, and four final C exits 0 with total done equal to the fallback count and zero saved failures.

Missing files, truncated data, an unexpected exit, resource exhaustion, an unresolved A or B parent, or a final C bad record prevent acceptance. Recoverable search diagnostics are distinguished from these terminal conditions. For example, A’s ownfail counts unsuccessful proposals of a local Root cover that are followed by subdivision. A0 reported such a diagnostic in this run; its terminal unresolved count was nevertheless zero.

Finite bounds and conservative stopping

The control flow has explicit finite bounds. Before filtering, the nondecreasing five-bin lists for the seed cover number at most \[\binom{116}{5}=160{,}389{,}488,\] and for any fixed shared bin the four ordered tail bins number at most \[\binom{115}{4}=6{,}913{,}340.\] The former bound is below the signed 32-bit limit. Pair traversals use range loops and 64-bit counters. All bin differences lie between \(-111\) and \(111\); their nine-coordinate square sum is at most \(9\cdot111^2\), so the integer distance and bucket arithmetic fit the stated types. The stored five-coordinate differences also fit the signed eight-bit type used by the cover.

A retains nonfinal unitary grid lists only through grid 32; the grid 64 has at most \(64^4/8=2{,}097{,}152\) cell tests per seed. Further tests are bounded by the \(1{,}000{,}000\) extra-node cap, and the deepest grid is 512. Reaching the cap or reaching the deepest grid without a certificate records an unresolved seed. Trial-direction and Root proposal failures can lose an opportunity to cover a cell, but cannot make an uncovered cell successful. The local candidate list uses topK=4 in an array of size 8.

The Root dimension is at most \(k=10\). Atlas sizes and individual record file counts are capped at \(2{,}000{,}000\), and concatenated B/C input counts at \(8{,}000{,}000\). For B the validated widths and radii give \(L\le1262\) and hence axis indices at most 2524; the product grid is checked against \(50{,}000{,}000\) before multiplication. Mixed-radix strides and marks therefore fit the stated index types. Each unresolved box is split to depth at most six, and the \(2^k\) child masks fit an integer. Only successfully completed parents are inserted into B’s list of earlier covered parents. A grid-cap rejection is a parent failure, not a completed parent.

C retains at most \(2{,}000{,}000\) phase bins. The first grid has \(12^5=248{,}832\) cells; a later grid tests at most 32 children per retained bin. Clustering permits at most 2048 balls. Its graph bitsets have 32 words of 64 bits, and all members have indices below the current node count. Word shifts are unsigned. The graph pair counts fit an integer, and the joint test has at most 14 rows. Recursive clique search decreases the requested clique size or removes a candidate; the step cap supplies an additional bound. A cap sets the conservative candidate/give-up flag and saves the record. It does not return a negative certificate. Consequently no finite resource cap in the specified run can establish nonexistence by silently dropping a region.

The finite-execution implication

The completed execution

The execution began at 03:10:26 and completed at 04:24:56 on 4 October 2026 (UTC). Both the runner and its supervisor exited 0; the supervisor recorded no cleanup or finalization errors, no remaining children, and unchanged input hashes. The execution evidence includes the raw command and stream records, exact file contents, record provenance, batch concatenation, actual fallback inputs, and final modulo partition. Together with the validation records, these account for all 100 native invocations and show no final unresolved records. They document the finite execution, not an automatic verification of the geometric or arithmetic lemmas.

Table 1 records this computation. All four A shards exited 0, with empty bad text files. Each B invocation exited 0 with an eight-byte zero-count bad file. Initial C had 73 exits 0 and 15 exits 1, all accounted for by saved failures. All final C shards exited 0 with eight-byte zero-count bad files.

The nonzero initial C failure files, in the actual order supplied to B fallback, were

bad10.bin bad3.bin bad4.bin bad5.bin bad52.bin bad53.bin
bad55.bin bad56.bin bad6.bin bad7.bin bad78.bin bad79.bin
bad8.bin bad80.bin bad84.bin

They contain all 163 unresolved records. There were no initial bin overflows, clustering failures, or uncapped graph candidates. There were no final failures of any category. Thus all 100 program invocations in the full pipeline are accounted for: one cover, four A processes, two B refinements, 88 initial C processes, one B fallback, and four final C processes. The fifteen initial C exits 1 are resolved by that fallback chain. No rejection threshold, graph cap, refinement width, or mathematical source file was altered, and no additional refinement level was inserted.

For scale, the wrapper-measured stage wall times, including polling and validation, were 621.59 seconds for the cover, 2020.32 seconds for the four parallel A shards, 1071.49 and 407.45 seconds for B mid and B fine, and 300.23, 8.12, and 36.27 seconds for initial C, fallback B, and final C. The outer supervisor measured 4470.33 seconds for the complete pipeline. These are observations on this platform, not native CPU times or running-time guarantees. No stage hit its wall deadline, and no retry or resource-limit increase was used.

The execution archive identified by verification/computation/README.md preserves the numerical data and records of this complete run, with internal path and host fields redacted: all sources and binaries, center and record files, all 88 input batches and their C bad files, fallback data, all final bad files, stdout and stderr, commands, exits, platform information, and validation records. In the execution archive, full-run-01/pipeline/status.json is the whole-run record; *.stage.json files describe stages and individual *.status.json files describe child processes. The outer record is full-run-01/run.json. verification/REPRODUCE.md gives rebuild and execution instructions. Archived native binaries document this run; they are not a portability claim.

The proof here uses only this newly completed chain and the values in Tables 1 and 2. The complete evidence packet for the execution reported on 7 September 2026 was not recovered. Although the new principal data hashes and stage counts agree with those reported for that run, this agreement does not authenticate the earlier execution. Neither its reported results nor earlier timed or sampled diagnostics substitute for any stage of the new full run.

Arithmetic premises and elementary estimates

The primitive-operation model is the binary64 specification of IEEE 754 (IEEE 2019, secs. 3.4, 3.6, 4.3, 5.4.1 and 7.5). The accumulation estimates use the usual product-of-rounding-factors argument (Higham 2002, sec. 2.12 and Lemma 3.1), with the explicit additive underflow allowance retained below.

The arithmetic premises are separate, correctly rounded binary64 addition, subtraction, multiplication, division, and square root in round-to-nearest mode, with binary64 evaluation of intermediate results. The build uses -ffp-contract=off, and does not use fast-math or reassociation that changes these operations. Subnormal numbers are not flushed to zero, and denormal inputs are not treated as zero. Floating exceptions are masked, so an unsuccessful heuristic calculation can produce an infinity or NaN and be rejected by its subsequent checks. The relevant integer types, numeric locale, and file representation are specified in Section 7.

The function environment sets and checks nearest rounding and checks the binary64 properties of double. The A/B/C entry points also inspect MXCSR, rejecting a non-nearest mode, DAZ, FTZ, or unmasked exceptions. The same no-DAZ/no-FTZ environment is required for covout, although its entry point does not itself inspect those bits. The default-nearest premise also applies to constants and the global basis constructed before main. These are explicit arithmetic premises, not a claim that a source-level static assertion formally verifies every compiler transformation. The recorded build checks and their limits are described in Section 7.

The functions nearbyint and floor choose integers at finite bounded arguments. The particular integer chosen at a boundary is permissible wherever the proof subsequently uses that integer lift. No accuracy premise is imposed on atan2: Candidate checks the unit exponential of the phase it proposes. Decimal literals are either used as exact stored parameters, or allowed a relative translation error of at most \(5\cdot10^{-16}\) when compared with a displayed decimal.

Put \[ u=2\cdot10^{-16},\qquad \tau=10^{-300},\qquad \gamma_m=2.1\cdot10^{-16}(m+1). \tag{137}\] For a correctly rounded basic operation with finite exact result \(z\) at the scales below, \[ |\operatorname{fl}(z)-z|\le u|z|+\tau. \tag{138}\] The true binary64 relative unit roundoff is smaller than \(u\), and the additive allowance is much larger than half the least positive subnormal. Overflows are excluded for the certificate evaluations by the scale bounds proved below; they need not be excluded in an untrusted solve.

For exact stored complex numbers, the explicit source operations obey \[\begin{align*} |\operatorname{fl}(z+w)-(z+w)| &\le u(|z|+|w|)+2\tau,\tag{141}\\ |\operatorname{fl}(zw)-zw| &\le 10^{-15}|z||w|+8\tau. \tag{142}\end{align*}\] For the latter, each real component uses two real products and an addition or subtraction. Its error is bounded by \((2u+u^2)\) times the sum of the two absolute products, plus the additive allowance. Cauchy’s inequality bounds each such sum by \(|z||w|\), and \(\sqrt2(2u+u^2)<10^{-15}\). Real scaling and division are componentwise instances of (138). Squared moduli also satisfy the useful perturbation bound \[ \big||z+e|^2-|z|^2\big|\le2|z||e|+|e|^2, \tag{143}\] before their own multiplication/addition errors.

The additive underflow terms can be retained throughout these inequalities. The norm allowance \(10^{-140}\) is deliberately loose. All subsequent certified divisions have the explicit lower bounds given below; in particular the residual test divides only by a gap of order \(10^{-6}\) or larger. Its norm factors and scale are at most the displayed \(10^8\)–\(10^{11}\) scales, so its propagated additive terms remain below \(10^{-120}\). The second square root in the spectral estimate is handled separately by an absolute term of order \(10^{-69}\). That term is covered there before the result is reused. Other normalizations have denominators bounded below by \(.148\), \(.45\), or larger. At each iterative upper-bound update the new local error is absorbed by its own positive margin. There is therefore no unchecked chain of ill-conditioned divisions propagating a subnormal error: all such additive contributions are below \(10^{-50}\) when they are absorbed in the strict budgets below.

Pi and unit exponentials

The source literal 0x1.921fb54442d18p+1 represents the binary rational \[\widehat\pi=\frac{884279719003555}{281474976710656}.\] Here is an exact certificate for its error. Write \[A(x,n)=\sum_{j=0}^{n-1}\frac{(-1)^j x^{2j+1}}{2j+1},\qquad s=16A(1/5,12)-4A(1/239,4).\] If \(t=\arctan(1/5)\), then \(\tan(2t)=5/12\) and \(\tan(4t)=120/119\); subtracting \(\arctan(1/239)\) gives tangent \(1\) in \((0,\pi/2)\). This proves Machin’s identity \(\pi=16\arctan(1/5)-4\arctan(1/239)\). The alternating-series remainder gives \[|s-\pi|\le \frac{16}{25\,5^{25}}+\frac{4}{9\,239^9}.\] Exact rational arithmetic gives \[ \widehat\pi-s= \frac{-1204334632739641172855772829555432415587} {10003273510806667494906565283020800000000000000000000000}. \tag{144}\] Adding the displayed rational remainder bounds and comparing integers proves \[ |\widehat\pi-\pi|<1.225418\cdot10^{-16}<2\cdot10^{-16}. \tag{145}\]

The range-reduction argument uses Sterbenz’s exact-subtraction lemma (Sterbenz 1974); a statement including gradual underflow is given in (Higham 2002, Theorem 2.5 and the following discussion). The polynomial and argument-error estimates are proved here for the particular degree-\(18/19\) implementation.

All relied-on arguments satisfy the range condition. Seed and dyadic unitary phases are bounded near \([0,1]\); gen checks \(|p_j|\le4\); Candidate checks \(|P_j|\le.51\) before its exponential; C validates \(|p_j|\le4\) and checks ball phases of magnitude at most two. The largest C difference has magnitude at most six. The constants \(\sqrt6\) and its reciprocal are formed by the indicated square root and division; \(2\cdot10^{-15}\) is an ample absolute error bound for each.

Seed filtering and seed-ball reuse

Here \(n=112\) and the stored \(w\) approximates \(1/n\). Midpoint-gap calculations contain only small integer arithmetic and a few products/subtractions; (138) bounds their total error, including the comparison threshold, by \(10^{-14}\). Their slack is \(10^{-8}\). The orientation filter is integral.

For a list of five varying phases, the computed residual \(c\) in sumok has component error below \(2\cdot10^{-13}\). Indeed its five exponential errors, after division by \(2\pi\), total less than \(4.8\cdot10^{-14}\) in complex modulus, and the divisions, additions, and constant error cost less than \(3\cdot10^{-15}\). The sharper componentwise bound \(1.1\cdot10^{-13}\) will also be useful. Each test direction is regarded as an exact stored pair; its norm is less than \(1.1\). The five column perturbations, the residual perturbation, and ordinary arithmetic in chk cost together less than \(10^{-11}\). Its remainder coefficient approximates \(5\pi/(4n^2)\) within \(10^{-15}\). The actual \(10^{-8}\) comparison addition therefore preserves every feasible list.

For extend, the stored direction has norm at most \(1.01\). Let \(v\), \(a\), and \(r\) denote its stored directional residual in grid units, shared coefficient, and support before inflation. Their errors satisfy \[ |\Delta v|<3.3\cdot10^{-11},\qquad |\Delta a|<10^{-13},\qquad |\Delta r|<10^{-12}. \tag{147}\] For the first bound, multiply the sharpened residual bound by \(112\) and by a direction of norm at most \(1.01\), and include a two-term dot and one multiplication. The other two follow from (146), four absolute support terms, and a two-component norm. If \(|d_s|\le1/2\) is feasible, these estimates give \[|v+a d_s|\le r+3.3\cdot10^{-11} +\tfrac12\cdot10^{-13}+10^{-12}+\text{rounding}.\] The source adds \(10^{-7}\) to \(r\) before dividing by \(|a|\). It skips \(|a|<10^{-6}\); at an accepted divisor \(|a|>.999\cdot10^{-6}\), allowing literal translation. The midpoint quotient has magnitude below \(1.2\cdot10^8\) and the radius quotient below \(3\cdot10^6\): the residual has magnitude below 112, and the support before division is below three. Their divisions and endpoint additions can move an endpoint by less than \(10^{-7}\). The extra \(10^{-5}\) on each endpoint is therefore sufficient. Intersecting these outward intervals retains the true shared value.

In supdual, all proposed entries are checked by \(|v_a|\le10^4\), with a negated comparison that also rejects NaN. They are then exact stored test coefficients. The four right-hand side errors against \(-nc\) are below \(3\cdot10^{-11}\) each. The signed term consequently has input error at most \[2\sum_{a=1}^4 |v_a|\,3\cdot10^{-11} \le2.4\cdot10^{-6}<2.5\cdot10^{-6}.\] Its absolute term sum is below \(10^7\), so its arithmetic error is below \(10^{-7}\). Each of the nine row-dot residuals has error below \(4\cdot10^{-9}\): its four input contributions are at most \(4\cdot10^4\varepsilon_{\exp}\), and its short dot costs less than \(10^{-10}\). Each pair norm has error below \(10^{-10}\) by (140). The remainder coefficient uses \(1.251\) instead of \(1.25\), which leaves positive slack after its own rounding. The final absolute scale is below \(2\cdot10^7\). Summing these contributions shows that the ideal support expression is at most the computed proposal plus \(10^{-4}\). The actual addition is \(.01\). If no usable proposal improves the initial \(10^{10}\) bound, that initial bound already exceeds the trivial support.

Integer differences lie in \([-111,111]\), including those stored in int8_t; all their squared/absolute sums are exact and small. The comparison radius is \[\texttt{RN2}=\operatorname{fl}((\operatorname{fl}(.032\cdot112))^2) -.0001\] with the source’s indicated operation ordering. The total possible error before the subtraction is below \(10^{-12}\), so this is smaller than the ideal \((.032\cdot112)^2\). This reasoning requires the pow(x,2) calls in covout to be lowered to binary64 multiplication, as checked for the fresh build documented in Section 7. It is not a claim about an arbitrary library implementation of pow. The other square-power value \(T\), bucket reach, and integer cuts only select reuse attempts; missing an attempt does not discard the current bin pair. A newly inserted midpoint needs radius only \(1.5/112<.032\). Finally, the nine division-rounded seed phases differ from their rational midpoints in norm by less than \(10^{-14}\), which is absorbed when the A seed radius is increased to \(.0320001\).

Frames, comparison blocks, and A exclusion tests

All ideal quantities in this subsection use exact unit exponentials at the specified centers, and the same coordinate indices selected by the code. We never need the selected coordinate to maximize the ideal projection score.

For frame, the four-term sum \(S\) has error below \(2.5\cdot10^{-13}\); its squared modulus has error below \(2.2\cdot10^{-12}\) by (143), and its modulus below \(2.6\cdot10^{-13}\) by (140). If the stored \(m=\sqrt{4-|S|}\) passes \(m>1.25\), the ideal \(m>1.24\). Using \(|\sqrt a-\sqrt b|=|a-b|/(\sqrt a+\sqrt b)\) at these lower bounds gives errors below \(3\cdot10^{-13}\) in \(m\) and \(\mathrm{top}=\sqrt{4+|S|}\). In particular \(16-|S|^2>6.1\); its error is below \(2.3\cdot10^{-12}\), so its reciprocal has error below \(7\cdot10^{-14}\). The two pseudoinverse numerators have modulus at most eight and error below \(5.1\cdot10^{-13}\). For example the row-times-\(\overline S\) product contributes at most the row error times \(|S|\), plus the \(S\) error, plus (142). Division/scaling then gives \[ |\Delta G_{ij}|<10^{-12},\qquad |G_{ij}^{\rm ideal}|<.81, \tag{148}\] the second inequality following from the lower singular bound.

The first constant basis column is exact. The next column has numerator error below \(1.3\cdot10^{-13}\) and denominator \(\sqrt{4-|S|^2/4}>1.5\) with error below \(2\cdot10^{-13}\). Its ideal entries have modulus at most one, so the quotient error is below \(4\cdot10^{-13}\). For each of the remaining two columns, use the actual selected coordinate projection \(q\). In the first such projection the earlier two products give entry error below \(9\cdot10^{-13}\), and its norm error is below \(2\cdot10^{-12}\). The accepted computed norm is greater than \(.449999\), so the ideal projection is nonzero and normalization gives entry error below \(7\cdot10^{-12}\). In the last projection the extra column-product error gives entry error below \(1.6\cdot10^{-11}\) and norm error below \(3.5\cdot10^{-11}\). The same denominator check gives entry error below \(1.2\cdot10^{-10}\). This argument inductively constructs the ideal orthonormal complements with the selected coordinates. The two-product kernel projector has entry error below \(3\cdot10^{-10}\); multiplying two complement entries and \(\sqrt6\) gives a W entry error below \(8\cdot10^{-10}\).

The following table records the rest of the propagation, with the source array names. Its errors include ordinary operation rounding.

To verify the larger entries, each base factor \(1+c_i\overline a\) has error below \(1.3\cdot10^{-13}\); its multiplication by G and the two-term sum give the listed base bound. The larger fixed term uses the projector error times a factor at most \(1.62\), plus a G/unit combination with error below \(3\cdot10^{-12}\), leaving room inside \(2\cdot10^{-9}\). Four W products cost less than \(4(8\cdot10^{-10})\) plus the unitary and base errors, below \(4\cdot10^{-9}\). The ideal K entry is at most \(\sqrt6\), and the block operator estimate of Section 3 gives \[\|D\|\le\max\{\sqrt6,\|C_0\|A_0/m_B\}<4.6.\] Each seed derivative has modulus at most \(1.62+.81\cdot4.6<6\); the individual angular derivatives before the complement/\(\sqrt6\) factors have operator norm at most one. Fixed error, moving-block error times \(.81\), and coefficient error times \(4.6\) fit inside \(10^{-8}\). The flat dot error is then less than \(6(4\cdot10^{-9})+4.6(10^{-8})\) plus a short-dot rounding error, below \(10^{-7}\). Finally, each \(||D_j|-1|\le3.6\); the 16 squared deviations have total error below \(10^{-6}\). The direct A flat-norm test adds \(10^{-5}\) to its threshold.

Root certificates and normal-displacement constants

This subsection verifies the numerical premises of the Root inequalities in Section 4. It concerns only successful patch calls. The stored center \(P\) is exact for these calculations; gen rejects \(|P_j|>4\) or a nonfinite phase. Each ideal row-edge product is a product of unit exponentials, so its computed error is below \(2\varepsilon_{\exp}+10^{-15}(1+\varepsilon_{\exp})^2 <1.3\cdot10^{-13}\). The six-term edge sum has error below \(8\cdot10^{-13}\). Across the 15 complex edges, division by \(2\pi\) gives vector error less than \[\frac{\sqrt{15}\,8\cdot10^{-13}}{2\pi}<5\cdot10^{-13}.\] The squared-modulus, scaling, sum, and final root add less than \(10^{-13}\) at the bounded unit-sum scale. Thus \(\sqrt{\texttt{val}}\) approximates \(\|F(P)\|\) within \(10^{-12}\). The accepted value satisfies \(\texttt{val}<10^{-18}\), and the stored \(\mathtt{froot}=\sqrt{\texttt{val}}+10^{-9}\) is an upper bound.

Integer lifts, dephasing, and sphere distances

For \(|p_j|\le4\), the three operations in unwrapped dephasing \(p_{ij}-p_{i0}-p_{0j}+p_{00}\) have entry error below \(8\cdot10^{-15}\); their intermediate magnitudes are at most 8, 12, and 16. Subtracting the integer selected by nearbyint gives error below \(10^{-14}\) against the exact dephase minus that same integer. A wrapped difference of two such arrays has error below \(3\cdot10^{-14}\) per entry against the ideal difference with the combined selected integers. The one-sided Candidate version, whose other array is already a stored dephased phase, has the same bound. These comparisons do not assume identical rounding choices for an independently formed ideal phase.

For a stored wrapped array, \(|z_j|\le1/2\). Its row and column sums have error below \(4\cdot10^{-15}\), and its length-36 grand sum below \(1.4\cdot10^{-13}\). Dividing by 6 or 36 and combining the means gives projection-operation error below \(10^{-14}\) per component. Projection contracts the prior input error. Consequently the computed projected difference has Frobenius error below \(10^{-11}\). All distance-square and norm errors at the successful cutoffs below are negligible compared with \(10^{-7}\).

Thus Atlas::find’s returned \(\sqrt s+10^{-7}\) is an upper distance for the selected ideal projected lift. A merge uses radius \(r+\text{distance}+10^{-8}\) and checks a cap with \(2\cdot10^{-8}\) slack. Its sum-rounding error is below \(10^{-14}\). The same arithmetic applies to assign and to the local sphere-radius additions. Searching only some buckets or transforms may miss a merge; it cannot certify a merge that fails these tests.

Candidate conversion and ellipsoidal coverage

The coverage estimates here are needed only after successful Candidate preparation, at final unitary-grid levels \(N_u\ge64\). Let \(m_j=|D_j|\) denote an ideal comparison-block magnitude. The stored magnitude test \(\sqrt{\texttt{mag}_j}>.15\) implies \(m_j>.14999998\). Normalizing D by its computed magnitude has unit-direction error below \[\frac{2\cdot4\cdot10^{-9}}{.14999998} +\text{norm/division rounding}<5.5\cdot10^{-8}.\] Candidate additionally checks a computed chord smaller than \(10^{-7}\) between this normalized value and the exponential of its proposed phase. With (146), the true unit chord error is less than \(1.56\cdot10^{-7}\). If a circular phase distance in cycles is \(v\in[0,1/2]\), its chord is \(2\sin(\pi v)\ge4v\). Across 16 entries the phase-center correction therefore has norm below \(1.56\cdot10^{-7}\), and in particular below the \(2\cdot10^{-6}\) allowance used in Section 4. The nine seed entries use exact stored seed centers and an exact integer subtraction.

For the D-position coefficients X, the normalized-direction error times the Jacobian bound six, plus the \(10^{-8}\) Jacobian error and short-dot rounding, is below \(10^{-6}\) per entry. The other used X entries are exact. The \(\mathtt{mi}\) subtraction of \(10^{-6}\) therefore gives a positive magnitude lower bound greater than \(.148\), and \(\mathtt{invmag}_j=1/(\widehat m_j-10^{-6})+10^{-9}\) is an upper bound for \(1/m_j\), below \(6.8\).

The flat-sum error is below \(10^{-6}\), so the \(10^{-5}\) addition in slack, followed by its additional \(10^{-10}\), gives the required nonnegative weighted chord-square upper bound. In the passed branch \(q<3.8\) and \(1-q/4>.049\). The arithmetic in dividing slack by mi has error below \(10^{-12}\): slack\(<4.1\) and the denominator is above \(.148\). The ratio \((1-q/4)^{-1/2}\) has error below \(10^{-12}\) before its \(10^{-7}\) addition; the denominator lower bound bounds the derivative, and \(q/4\) is a binary scaling. The remaining positive products/roots, and the division by \((2\pi)^2\) in d2, each have error below \(10^{-12}\) before their \(10^{-8}\) additions. In particular the stored quantities are upper bounds with \[ \mathtt{arc}<8.8,\qquad \mathtt{weighted}<10, \qquad \mathtt{invmag}_j<6.8. \tag{154}\]

The spectral and inverse-quadratic-form bounds

The ell guard checks symmetry and \(|G_{ij}|\le10\), and checks each offset component to have magnitude at most ten. Its invalid return value 100 cannot certify a cell: after conversion to cycles it exceeds 10, so the associated bootstrap path returns its nonsuccess sentinel. A different valid bound may still succeed. For valid data the initial triangle bound is \(\sqrt{\mathtt{mx}}+\sqrt{\mathtt{gu}}+10^{-8}\). Here \(\mathtt{mx}\) is the maximum squared offset norm. Its norm error is below \(10^{-13}\) and the triangle bound is upward and smaller than 43.

For each proposed resolvent parameter, interpret stored \(\mathtt{gam}=\gamma\) as exact. The proposal formula and the input scales give \(0<\gamma<418\). Since gu is an upper spectral bound, \[ \mathtt{gap}=\operatorname{fl}(\gamma-\mathtt{gu}-10^{-9}) \le\gamma-\lambda_{\max}(G). \tag{156}\] The two subtraction errors are below \(2\cdot10^{-13}\), absorbed by \(10^{-9}\). Only a stored gap of at least \(10^{-6}\) is used. Allowing literal translation still gives a gap above \(.999\cdot10^{-6}\) for scale estimates.

For one offset vector U, the trial solve is used only if each stored \(|z_i|<10^8\). Let \(s_z=\max(1,\|z\|_\infty)\). Its exact residual is \(r=U-\gamma z+Gz\). The following local bounds hold:

For example the component bound follows from at most twelve terms and the scale 528 using (139); its aggregate contributes at most \(\sqrt{10}\,2\cdot10^{-12}s_z\) to the norm, and (140) adds less than \(5\cdot10^{-12}s_z\). The dot and U-norm bounds are the same lemmas at lengths ten.

The exact inverse quadratic form satisfies \[ U^*(\gamma I-G)^{-1}U \le U^*z+\frac{\|U\|\|r\|}{\gamma-\lambda_{\max}(G)}. \tag{157}\] Indeed \((\gamma I-G)^{-1}U=z+(\gamma I-G)^{-1}r\). The code forms the right-hand-side upper using \[ \big(\mathtt{dotv}+10^{-10}s_z\big) +\frac{(\sqrt{\mathtt{un}}+10^{-10}) (\sqrt{\mathtt{res}}+10^{-10}s_z)}{\mathtt{gap}}, \tag{158}\] with the shown binary64 operations. The rounded dot part exceeds \(U^*z\) by at least \(9\cdot10^{-11}s_z\) and has magnitude at most \(101s_z\). The first rounded norm factor is at least \((1+2\cdot10^{-12})\|U\|\), because \(\|U\|\le\sqrt{1000}\); the second is at least \(\|r\|\). Together with (156), product/division rounding therefore leaves a quotient B such that the required exact quotient in (157) is at most \((1-10^{-12})B\). This quotient is finite and below \(6\cdot10^{18}\) by the displayed norm scales and the gap lower bound. The final addition’s possible error is at most \(u(101s_z+B)+\tau\), which is smaller than the surplus \(9\cdot10^{-11}s_z+10^{-12}B\). Thus (158) is an upper bound even when its dot part is negative and cancellation occurs.

Taking the maximum with zero and over the offsets gives high. The ellipsoid formula of Section 4 then uses \(\sqrt{\gamma(1+\mathtt{high})}+10^{-6}\). There is no overflow at the stated scales. If this candidate can lower the existing bound below 43, its exact unrounded root is less than 44; its scalar downward error is then below \(10^{-12}\), covered by \(10^{-6}\). A candidate that cannot improve the existing upper need not have a tighter absolute estimate. The routine adds another \(10^{-6}\) at return. Cholesky accuracy has not entered this argument; it merely proposes the checked stored z.

Refinement relations, tangent grids, and radius updates

The B inputs are genuine earlier Root certificates. In addition, validate enforces \(0\le R\le.126\), \(0\le C<20\), \(0\le\mathtt{n0},\mathtt{froot}<10^{-6}\), \(0\le\mathtt{id}<10^{-4}\), \(0\le\mathtt{ort},\mathtt{hor}<10^{-5}\), \(0\le\mathtt{mnorm}<2\), \(0\le k\le10\), and \(|p_j|\le4\). The stored T entries pass the range check \(|T_{ja}|\le1.01\); their stronger operator bound is (153), supplied by the genuine Root certificate.

Single-vector filters and vector-ball construction

The C stage validates its Root and \(0\le r\le.03\). At every bin resolution \(M\ge6\), the halfwidth, Euclidean bin radius X, one-norm bound, and infinity-norm bound are formed as \[\begin{aligned} a&=.5/M+10^{-12},& X&=\sqrt{5-1/6}\,a+10^{-12},\\ x_1&=5a+10^{-12},& x_\infty&=1.5a+10^{-12}. \end{aligned}\] Their operations have error below \(10^{-14}\), and their \(10^{-12}\) additions are upward. They satisfy \(X<.19\), \(x_1<.42\), and \(x_\infty<.126\). The stored tangent and normal bounds \[r_t=\sqrt{1+\mathtt{ort}}\,r+10^{-9},\qquad r_n=\mathtt{n0}+\mathtt{id}r+Cr^2+10^{-9}\] are upper bounds, with \(r_t<.030001\) and \(r_n<.019\). The square-root/product and positive-polynomial errors are below \(10^{-13}\). The constant \(K=1.00001\), even allowing its literal translation error, exceeds the needed operator bound: the Root residual gives \[\|e(P)/\sqrt6\| \le\sqrt{1+(2\pi\sqrt2/6)\,10^{-6}} <1.00000075<K.\]

For bin or ball centers, put, as in Section 6, \[q_{ji}=e(u_j-P_{ji})/\sqrt6,\qquad S_i=\sum_jq_{ji},\qquad c_i=(|S_i|^2-1)/(4\pi).\] Let \(J_{ij}=-\Im(\overline S_iq_{ji})\) and \(D_{ij}^{\rm re}=\Re(\overline S_iq_{ji})\). The following errors are uniform for the called arrays:

Indeed the scaled exponential error is actually less than \(2.5\cdot10^{-14}\) before the loose \(10^{-13}\) allowance. Six terms and addition rounding give the S bound. Equation (143) gives less than \(2\sqrt6(7\cdot10^{-13})\) plus tiny arithmetic, below \(4\cdot10^{-12}\). Norm Lipschitz gives the magnitude bound. The companion products cost at most \((7\cdot10^{-13})/\sqrt6+\sqrt6\,10^{-13}\) plus product rounding, below \(10^{-12}\). Finally \(B_{ia}=\sum_jJ_{ij}T_{ji,a}\), where \(T_{ji,a}\) is the entry at phase position \((j,i)\) in tangent column a, has six terms, each T entry bounded by \(1.00001\), so its input and short-dot errors are below \(7\cdot10^{-12}\).

Pair edges and the joint directional test

Let two accepted vector balls have radii \(s_0,s_1<.1\). The stored pair radius \(r_e=s_0+s_1+10^{-10}\) is an upper bound for their sum and satisfies \(r_e<.201\). Each product \(Q_j\) of the two stored unit phases has complex error below \(1.3\cdot10^{-13}\), its six-term sum S below \(8\cdot10^{-13}\), and its squared modulus below \(1.1\cdot10^{-11}\); the last uses \(|S|\le6\) in (143). The edge constants and derivatives, for either O or U, have error below \(10^{-12}\) per real component. For the U derivative, for instance, the product of S with a unit coefficient is divided by six, leaving error at most \[\frac{8\cdot10^{-13}+6(1.3\cdot10^{-13})}{6} +\text{short product rounding}<10^{-12}.\] The O constant is S divided by \(2\pi\), and the U constant is \((|S|^2/6-1)/(4\pi)\), which satisfy the same budget.

The edge-remainder bounds are evaluated with an added \(2\cdot10^{-8}\). Their positive-operation error, including the input error in \(|S|\), is below \(10^{-10}\); at \(r_e<.201\) their uninflated values are below \(.255\). The direct distance and support comparisons, including the O test in direction S and the norm \(\sqrt{\mathtt{jj}}\), have combined possible error below \(10^{-9}\). Indeed the latter norm has coefficient perturbation at most \(\sqrt6\,10^{-12}\); its multiplier is at most \(6r_e<1.206\), and the constant/norm-S effects are at most the displayed \(1.1\cdot10^{-11}\) scale times bounded factors. Their actual comparison slack is \(2\cdot10^{-7}\).

For the joint test there are at most \(6+6+2=14\) rows. The proposed direction is checked finite and normalized as before, so its stored entries have magnitude at most one. The constant pairing has error below \(1.5\cdot10^{-11}\). Each accumulated shared-Hadamard coefficient has error below \(9\cdot10^{-11}\), since it receives at most twelve B input errors of \(7\cdot10^{-12}\) plus short-dot rounding. Each vector-phase coefficient, including its edge contribution, has error below \(9\cdot10^{-12}\): six single-vector entries and at most two edge entries each contribute at most \(10^{-12}\).

Within each call to single::support, the vector-phase coefficient array starts at zero. The pure-vector remainder is formed using its J sum and real companion sum before the joint routine adds the edge derivatives. Thus its maximum two-component coefficient norm has the same \(1.1\cdot10^{-11}\) error bound as in Section 9.10, with \(X\) replaced by \(s_t<.1\) and only the first coefficient-norm alternative retained. The weighting of the common B norm has input effect below \[.030001\sqrt{10}\,9\cdot10^{-11}<8.6\cdot10^{-12}.\] Each vector-phase norm has perturbation at most \(\sqrt6\,9\cdot10^{-12}\), multiplied by \(s_t<.1\). The two single-vector residual supports have the norm-Lipschitz errors just proved; the edge residual upper multiplies a direction norm of at most \(\sqrt2\) and has only ordinary bounded norm/product rounding. Adding these contributions and the positive scalar arithmetic gives total possible support undererror below \(10^{-8}\). The actual comparison adds \(3\cdot10^{-7}\). Together with the constant-pairing error this certifies the joint rejection. No edge deletion depends on accuracy of the heuristic solves or their weight updates.

Finite paths and preservation of inconclusive cases

The preceding estimates apply to bounded finite certificate evaluations. We finish by explaining why exceptional heuristic values cannot bypass those preconditions.

1. In the seed cover, all direct lists come from finite integer midpoints and expair. The dual solver’s entries must pass the negated bounded comparison \(|v_a|\le10^4\); NaN and infinity fail it. A failed proposal leaves the large safe support bound. Gap/hash/reach cuts that are not necessary feasibility tests select only possible reuse attempts.

2. For A, a failed frame normalization makes setup fail, and the entry point records an unresolved seed ball. It does not certify that seed ball empty. The passed frames, fixed radius, and dyadic unitaries give finite bounded block coefficients. The potentially ill-conditioned solves only propose directions; the final trial::certificate checks every direction entry and its maximum before use.

3. The snapping iteration calls gen, which rejects nonfinite or out-of-range phases. Root certification requires \(\mathtt{val}<10^{-18}\), checks proposed eigenvalues finite, checks HV/LV before using them, and checks T before its certificate products. Those bounded arrays make the products finite. The optional tensor change of basis is range-checked; an unusable one cannot lower the previously valid C bound. The final conjunction of strict Root thresholds also rejects NaN.

4. Candidate’s inverse-angle output passes a finite range condition before its exponential and a unit-direction comparison afterwards. Its magnitude and chord guards bound every normalization. Failure is an unsuccessful coverage proposal. In ell, the data are range/symmetry checked, invalid Cholesky pivots fail, and every final trial-solve coordinate is checked before a residual certificate is evaluated. The bounded residual scales exclude overflow. The explicit sentinel values are outside the usable bootstrap range or far above the target radius.

5. B/C operate on genuine certified Records and also enforce the stated numeric ranges in validate. The read-time finish may form floating dephasings before validation, but performs no conversion of those values to an integer index; validation rejects invalid phases before they can reach indexed geometric searches. B’s relation and grid formulas are then finite and bounded as proved above. A failed relation only removes a coverage opportunity; a failed live-box solve keeps the parent unresolved.

6. C’s direct scalar and pair formulas have bounded finite inputs and nonnegative square-sum arguments, so explicit finite checks at every individual arithmetic operation are unnecessary. Every potentially ill-conditioned directional solve is separately checked and normalized. Its failure keeps the bin or edge. Clustering checks final center and radius bounds; caps and incomplete graph searches report possibility/failure, as described in Section 6, rather than a negative certificate.

In particular, min/max are not used to turn an unchecked NaN from a heuristic solve into a valid small certificate. Within successful bound evaluations their inputs are finite, and a minimum of two established upper bounds remains an upper bound. Within proposal generation, a bad proposal is checked before it can justify an exclusion or cover. These facts also explain why a less successful heuristic or a different valid rounding outcome may increase unresolved work without invalidating a successful certificate.