Fourier methods and mutually unbiased bases

Two orthonormal bases in \(\mathbb C^d\) are mutually unbiased if every inner product between their vectors has modulus \(d^{-1/2}\). Such bases describe complementary measurements and arise in quantum state determination (Ivanović 1981; Wootters and Fields 1989). A family contains at most \(d+1\) bases, and complete families attaining that bound exist in prime-power dimensions (Wootters and Fields 1989). The first dimension outside that construction is six. Write \(N(6)\) for the maximum size of a mutually unbiased family in \(\mathbb C^6\).

Fixing one basis identifies every other unbiased basis with a complex Hadamard matrix. Matolcsi developed a Fourier and Delsarte approach to the resulting constraints on torus points (Matolcsi 2012). Matolcsi, Ruzsa, and Weiner developed identities for the associated character sums and formulated the vanishing conjecture addressed here (Matolcsi et al. 2013). Maxwell and Brierley proved that vanishing for the Karlsson family (Maxwell and Brierley 2015, Theorem 4.1). Theorem 1 removes the family restriction. The exceptional matrix is usually denoted \(S_6\) in the Hadamard literature (Tadej and Życzkowski 2006, sec. 5.6.4); Section 4 gives the precise identification with (2).

The structural step has a separate antecedent. Lisoněk introduced S-Hadamard matrices, for which both \(H\) and \(H^{\circ2}\) are Hadamard (Lisoněk 2019, Definition 2.1). Phangara conjectured that every order-six S-Hadamard matrix is equivalent to the cubic example (Phangara 2026, Conjecture 3.1.6). Proposition 7 proves this assertion. The uniqueness of the cube-root class itself appears in the Butson classification of Lampio, Östergård, and Szöllősi (Lampio et al. 2020, Theorem 4.1 and Table 2) and in Liang, Chen, Long, and Qiu (Liang et al. 2021, Lemma 10). The additional step here derives cube-root entries from the two Hadamard conditions on arbitrary phases.

There is also a substantial history of positive certificates for the MUB problem. Brierley and Weigert formulated polynomial and semidefinite approaches (Brierley and Weigert 2010). Matolcsi and Weiner strengthened the Delsarte witness method for prescribed Hadamard families (Matolcsi and Weiner 2015), and Kolountzakis, Matolcsi, and Weiner developed the positive-definite-function approach on compact groups (Kolountzakis et al. 2018). Gribling and Polak applied permutation symmetry to positive moment matrices in a tracial noncommutative formulation of the MUB problem (Gribling and Polak 2024). Our finite invariant-moment certificates belong to this line of work. Their specific character identities and shared-column test functions are described below.

Bandeira, Doppelbauer, and Kunisky proved that positive-definite polynomials of degree at most six in the entries of a single unitary transition matrix and their conjugates cannot improve the seven-basis bound in dimension six (Bandeira et al. 2022, Theorem 1.10). That result concerns its specified single-matrix relaxation. The mixed certificate here uses products of character sums from several transitions and relations of higher total order.

The individual-matrix statement also supplies an input to a second exact certificate within this paper. It yields the following complete-family obstruction.

By Weiner’s completion theorem, any \(d\) mutually unbiased bases in \(\mathbb C^d\) extend to a complete family (Weiner 2013, Corollary 3.4). Theorem 2 therefore gives \(N(6)\le5\). Under its stated binary64 arithmetic and compiler conditions and complete-execution certificate contract, the companion paper (OpenAI 2026, Theorem 1.1, Section 7 and Appendix A) gives the sharper value \(N(6)=3\). The Fourier theorem concerns each individual Hadamard matrix; its content is distinct from a bound on the number of bases. For transitions in MUB triplets, Matolcsi, Matszangosz, Varga, and Weiner conjecture both this vanishing and a further condition coupling characters at \(3\alpha\) for \(H\) and \(H^*\) (Matolcsi et al. 2026, Conjecture 2). Their route to \(N(6)=3\) also uses a separate conjecture excluding the Szöllősi family from quadruplets (Matolcsi et al. 2026, Conjecture 3 and Proposition 4.2).

Proof strategy

The main difficulty is to obtain a universal statement about phases from orthogonality without restricting the matrix to a parametrized family. We average monomials in its entries over distinct row and column indices. Summing a row with one exponent \(+1\) and one exponent \(-1\) against orthogonality expresses its moment in terms of moments with merged rows. A formal seven-row version has no unused physical row; it gives a homogeneous relation among six-row moments. Products of character sums expand into these injective moments by grouping column samples according to which indices coincide.

The first certificate adds an auxiliary absolute square to a product \(|g_H(\alpha)g_H(q)|^2\) and proves that their finite average is zero. Every summand is nonnegative, so the product vanishes for every row ordering. Two choices of \(q\) force a dichotomy: either all permuted \(\alpha\) characters vanish, or the entrywise square \(H^{\circ2}\) is Hadamard. In the latter case, Newton’s identities constrain every row ratio to two rotated triples of cube roots. An orthogonality argument then forces the whole dephased matrix to be cubic, and a five-cycle classifies it as \(T\). This proves Theorem 1.

The complete-family obstruction requires more than the vanishing condition on one matrix. We first exclude a cubic transition matrix from such a family by an exact finite character calculation. For the remaining case, we average products of character sums over ordered basis pairs and triples. Sampling one additional column shared by all test functions expresses their Gram entries as combinations of three-factor moments. Six explicitly specified positive quadratic forms have a combined expansion whose constant term dominates, with negative sign, the sum of the absolute values of all other coefficients. Since every retained moment has absolute value at most one, this contradicts positivity.

The certificates are finite rational identities. Modular elimination locates candidate substitutions, and exact integer multiplication proves that they hold for every actual moment vector. The calculation does not require those moment values to be rational. Section 7 explains this distinction and traces the verifier’s operations back to the sampled variables.

Section 2 fixes the character notation. Section 3 constructs the single-matrix certificate and its dichotomy. Section 4 classifies the cubic alternative and proves Theorem 1. Section 5 derives the complete-family identities and excludes a cubic pair. Section 6 constructs the shared-column Gram certificate and proves Theorem 2. Section 7 verifies both exact calculations, and Appendix 8 prints the complete standard-library Python verifier, including all integer weights.

Injective moments

Fix a \(6\times6\) Hadamard matrix \(H\). An exponent matrix is an integer matrix \(A=(A_{uv})\) whose row sums and column sums are all zero. For \(A\) of size \(p\times q\), with \(p,q\leq6\), define \[ m_H(A)= \mathbb E\,\mathop{\mathrm{Re}}\!\left[ \prod_{u=0}^{p-1}\prod_{v=0}^{q-1} K\bigl(\rho(u),\kappa(v)\bigr)^{A_{uv}} \right]. \tag{3}\] Here \(K\) is \(H\) or \(H^{\mathsf T}\) with probability \(1/2\) each, \(\rho:\{0,\ldots,p-1\}\to\{0,\ldots,5\}\) and \(\kappa:\{0,\ldots,q-1\}\to\{0,\ldots,5\}\) are uniformly chosen injections, and these three choices are independent. Negative exponents are well defined because every matrix entry has modulus one. We set \(m_H(\varnothing)=1\) for the empty exponent matrix. In particular, \[ |m_H(A)|\leq1. \tag{4}\]

Permuting the rows or columns of \(A\) leaves this expectation unchanged. Replacing \(A\) by \(-A\) conjugates the monomial and therefore leaves its real part unchanged. Also \(m_H(A^{\mathsf T})=m_H(A)\): transposition exchanges the two injections and interchanges the equally weighted choices of \(K\). Finally, a zero row or column can be deleted. Indeed, its factor is one, and deleting a coordinate of a uniformly chosen injection leaves a uniformly chosen injection on the remaining coordinates. These facts justify all the identifications of exponent matrices used below.

For a balanced integer row \(a\), its order is \(\mathop{\mathrm{ord}}(a)=\sum_{j:a_j>0}a_j\), consistently with the notation for charges. The following relation eliminates any row of order one.

Repeatedly applying Lemma 4 to rows or columns of order one expresses any moment with both dimensions at most six as a rational linear combination of the empty moment and moments whose nonzero rows and columns all have order at least two. Each contraction reduces the number of rows or columns, so this procedure terminates. Choosing representatives under the symmetries above introduces no additional mathematical relation.

From products of characters to injective moments

For a permutation \(\pi\) of \(\{0,\ldots,5\}\), write \(K^\pi(i,k)=K(\pi(i),k)\). We use the notation \[ \bigl\langle F(\widetilde H)\bigr\rangle_H =\frac{1}{2\cdot6!} \sum_{K\in(H,H^{\mathsf T})}\ \sum_{\pi\in S_6} F(K^\pi) \tag{7}\] for the average over the two orientations and all row permutations. The ordered pair \((H,H^{\mathsf T})\) in this formula is counted with multiplicity even when its entries coincide. Column permutations do not change \(g_{\widetilde H}\) and need not be included.

Let \((6)_k=6\cdot5\cdots(6-k+1)\), with \((6)_0=1\).

The hypotheses on the charges ensure that every matrix in (8) has both row and column sums zero. Moreover, \(\overline{g_H(a)}=g_H(-a)\), so absolute squares of products are covered by the lemma. A zero charge may be omitted before applying the expansion, since its factor is \(g_H(0)=1\); equivalently, integrating out its independently sampled column does not change the distribution of the remaining columns.

For example, if \(a\) is a balanced charge and \([a,-a]\) denotes the two-column exponent matrix, the two possible equality patterns give \[\left\langle |g_{\widetilde H}(a)|^2\right\rangle_H =\frac16+\frac56m_H([a,-a]).\] The first term comes from equal sampled columns, where all exponents cancel; the second comes from two distinct columns. The certificate below uses the same expansion for products with up to four factors.

An exact identity and its consequence

The auxiliary expression below is chosen so that orthogonality yields a sum of nonnegative terms equal to zero. The resulting vanishing products will force the dichotomy.

Retain \(\alpha=(1,1,1,-1,-1,-1)\) and put \[\begin{align*} w&=(-3,-2,0,1,2,2),\\ a_1&=(-1,-1,0,0,1,1),& a_2&=(-2,0,0,0,1,1),\\ a_3&=(-1,-1,0,1,0,1),& a_4&=(-1,-1,0,1,1,0). \end{align*}\] Define \[ L_H=-g_H(w)+\sum_{j=1}^4 c_j g_H(a_j)g_H(w-a_j), \qquad (c_1,c_2,c_3,c_4)=(2,1,1,1), \tag{9}\] and the two charges \[\begin{equation*} q_{\mathrm{cross}}=(2,0,0,-2,0,0), \qquad q_{\mathrm{same}}=(2,-2,0,0,0,0). \end{equation*}\] Every term defining \(L_H\) has total charge \(w\). The nonzero entries of \(q_{\mathrm{cross}}\) lie in opposite sign triples of \(\alpha\), whereas those of \(q_{\mathrm{same}}\) lie in the same triple. These two choices will supply the squared-row inner products in the proof of the dichotomy.

Character identities of a complete family

Suppose that \(B_1,\ldots,B_7\) are mutually unbiased orthonormal bases. For \(r\ne s\), define their transition matrix by \[H_{rs}(i,k)=\sqrt6\,\langle b_{r,i},b_{s,k}\rangle.\] Unbiasedness and orthonormality imply that \(H_{rs}\) is Hadamard and that \(H_{sr}=H_{rs}^*\). With a reference basis \(r\) fixed, we abbreviate \(H_{rs}\) and \(g_{H_{rs}}\) to \(H_s\) and \(g_s\).

The complete-set projector identity used in the proof is the second-moment identity for a complex projective \(2\)-design; see Zauner (Zauner 1999, Satz 2.19) and Klappenecker–Rötteler (Klappenecker and Rötteler 2005, Theorem 3). We give the projection argument in our normalization. The character identities are part of the Fourier approach (Matolcsi 2012; Matolcsi et al. 2013).

The identities for one matrix hold for every Hadamard matrix. The order-two sum in (12) uses the completeness of the seven-basis set. The later mixed identities retain this completeness information through averaging over the six external bases.

The cubic-pair obstruction

Brierley and Weigert proved the stronger fact that the standard basis and the basis defined by \(T/\sqrt6\) cannot be extended by a third mutually unbiased basis (Brierley and Weigert 2009, sec. 4.1 and Table 1). The following proposition gives an exact Fourier derivation of the complete-family exclusion needed here.

To prove the proposition, suppose that such a pair occurs. By Proposition 7, rephasing and reordering its basis vectors allows us to take its transition matrix to be \(T\). These operations preserve every mutual unbiasedness condition. Use the first basis of this pair as reference, and call the other five transition matrices \(K_1,\ldots,K_5\). Define \[f(b)=\frac15\sum_{s=1}^5g_{K_s}(b),\qquad G(b)=g_T(b).\] Lemma 8 gives \(f(b)=G(b)=0\) at order one, and Equation (12) gives \[ f(b)=-\frac15G(b)\qquad(\mathop{\mathrm{ord}}(b)=2). \tag{16}\] Equation (14), applied with its second charge equal to \(-c\) and then averaged over \(K_1,\ldots,K_5\), gives \[ \sum_{d\in D}f(a+d)\overline{G(c+d)}=0 \qquad\text{for all balanced }a,c. \tag{17}\] Let \[ S(b)=\frac1{6!}\sum_{\pi\in S_6} \mathop{\mathrm{Re}}\bigl(f(\pi b)\overline{G(\pi b)}\bigr). \tag{18}\] Because \(f(-b)=\overline{f(b)}\) and likewise for \(G\), this average also equals the average over the distinct elements of the signed permutation orbit of \(b\).

Every entry of \(T\) has cube one, so \(G(3d)=1\) for \(d\in D\). The signed permutation orbit of \(3(e_5-e_0)\) is precisely \(\{3d:d\in D\}\). If \(z\) is a uniformly sampled column of a uniformly sampled matrix among \(K_1,\ldots,K_5\), then \(\mathbb Ez^b=f(b)\). Consequently \[ 0\le\mathbb E\left|\sum_{i=0}^5z_i^3\right|^2 =6+\sum_{d\in D}f(3d) =6+30S\bigl(3(e_5-e_0)\bigr). \tag{19}\] Thus this orbit average must be at least \(-1/5\). We will use (17) to compute it and contradict this lower bound. The next lemma concerns \(T\) alone; it lets us calculate the coefficients of those identities one permutation orbit at a time.

Symmetries of the cubic matrix

The row-permutation symmetry below also follows from the semilinear automorphism group determined by Gillespie, Ó Catháin, and Praeger (Gillespie et al. 2018, Proposition 2). We give a direct proof using the five-cycle classification.

Coefficients of the cross identities

Let \[a=(-1,-1,0,0,1,1),\qquad c=(0,0,0,0,-1,1),\] and let \(\mathcal O\) be the set of distinct simultaneous permutations \((A,C)\) of \((a,c)\). Apply (17) to every \((A,C)\in\mathcal O\), multiply by \(\overline{G(A-C)}\), sum, and take real parts. To record the coefficients explicitly, set \[Q(b)=\sum_{\substack{(A,C)\in\mathcal O\\b-A\in D}} G(A-C)G(b-A+C).\] The resulting equality is \[\sum_b\mathop{\mathrm{Re}}\bigl(f(b)\overline{Q(b)}\bigr)=0,\] where the sum is finite. For a complex number \(z\), write \(z^{[1]}=z\) and \(z^{[-1]}=\overline z\). Conjugacy of \(f\) permits symmetrizing the coefficient as \(R(b)=(Q(b)+\overline{Q(-b)})/2\): replacing \(b\) by \(-b\) in the finite sum above and averaging leaves it unchanged. Explicitly, \[ R(b)=\frac12 \sum_{\substack{(A,C)\in\mathcal O,\ \epsilon\in\{-1,1\}\\ \epsilon b-A\in D}} \bigl[G(A-C)G(\epsilon b-A+C)\bigr]^{[\epsilon]}. \tag{20}\] We have therefore obtained the weighted cross identity \[ \sum_b\mathop{\mathrm{Re}}\bigl(f(b)\overline{R(b)}\bigr)=0. \tag{21}\] Its coefficients depend only on \(T\). We now calculate them.

The following table lists representatives \(w_j\) of every balanced charge of order at most three, up to permutation and negation. The integer triples in its last two columns satisfy \[ 6G(w_j)=\sum_{m=0}^2N_m\omega^m, \qquad 72R(w_j)=\sum_{m=0}^2U_m\omega^m. \tag{22}\]

Here is an explicit summation rule reproducing Table 1. Put \[v(b,k)=\sum_{i=0}^5 b_i t_{ik}\pmod3,\] with residues in \(\{0,1,2\}\). For each input \(b=w_j\), initialize two separate arrays \(N,U\) of three zero integers and apply these loops:

for k = 0,...,5:
    N[v(b,k)] += 1
for p,q = 0,...,5 with p != q:
    for 0 <= h < i <= 5 with {h,i} disjoint from {p,q}:
        A = e_p + e_q - e_h - e_i
        u = 2*e_p - e_h - e_i
        for s in {-1,1} with s*b - A in D:
            for k,l = 0,...,5:
                U[(s*(v(u,k) + v(s*b-u,l))) mod 3] += 1

Indeed, the \(30\binom42=180\) pairs in \(\mathcal O\) are uniquely parametrized by \[A=e_p+e_q-e_h-e_i,\qquad C=e_q-e_p,\] with precisely the conditions used in the loops; thus \(u=A-C\). Each product of two \(G\) terms contributes \(36\) cube roots with coefficient \(1/36\), and the factor \(1/2\) in (20) accounts for the denominator \(72\) in (22).

For example, row \(3\) gives \(G(w_3)=(4+\omega+\omega^2)/6=1/2\) and \(R(w_3)=(60+42\omega+42\omega^2)/72=1/4\). Using \(1+\omega+\omega^2=0\) in every row gives \[ R(b)=\lambda_jG(b),\qquad \lambda_3=\tfrac12,\quad \lambda_6=3,\quad \lambda_7=9,\quad \lambda_8=4, \tag{23}\] on the signed permutation orbit of \(w_j\), and \(R(b)=0\) on all other orbits. To justify extending the representative calculation, observe that every factor in (20) has a balanced charge. Its column phases therefore cancel. The two charges in each product add to \(\epsilon b\), so after the prescribed conjugation its row phase factor is exactly the factor for \(G(b)\). Row permutations preserve the full set \(\mathcal O\), and conjugation conjugates both \(R\) and \(G\). Lemma 10 therefore gives the asserted covariance on every orbit; also \(R(-b)=\overline{R(b)}\). No other orders can occur in the support of \(R\), since \(\epsilon b=A+d\) with \(\mathop{\mathrm{ord}}(A)=2\) and \(d\in D\) implies \(\mathop{\mathrm{ord}}(b)\le3\).

The contradiction

Sampling and positive forms

Choose a reference basis index \(r\) uniformly from the seven indices. Given \(r\), choose independently a uniform permutation \(\sigma\) of its six coordinates and a uniform bijection \(\pi\) from \(\{0,\ldots,5\}\) to the six other basis indices. In this section write \[H_s(i,k)=\sqrt6\,\langle b_{r,\sigma(i)},b_{\pi(s),k}\rangle, \qquad g_s=g_{H_s}.\] The column order within each basis may remain fixed: each \(g_s\) already averages over all six columns. For labels \(\mathbf s=(s_1,\ldots,s_n)\) and balanced charges \(\mathbf a=(a_1,\ldots,a_n)\) with \(\sum_j a_j=0\), define \[ \mathcal M(\mathbf s;\mathbf a) =\mathbb E\,\mathop{\mathrm{Re}}\!\left(\prod_{j=1}^n g_{s_j}(a_j)\right). \tag{28}\] Equal labels always denote the same matrix. The marginal assignment of any \(l\) distinct labels is a uniform injection into the six nonreference bases. Thus the definition does not depend on which unused labels are included in the sampled bijection. The empty product has moment \(1\).

We also use the ordered-pair average of the injective moments of Section 3: \[ m(A)=\frac1{42}\sum_{r\ne s}m_{H_{rs}}(A), \qquad H_{rs}(i,k)=\sqrt6\,\langle b_{r,i},b_{s,k}\rangle. \tag{29}\] Here \(m_H\) is the real injective moment with the transpose averaging specified there. All these actual moments obey \[ |m(A)|\le1,\qquad |\mathcal M(\mathbf s;\mathbf a)|\le1. \tag{30}\] For the first inequality the integrand has modulus one. For the second, each \(g_s(a)\) is an average of six numbers of modulus one.

The next construction expresses the real parts of Gram entries as linear combinations of three-factor mixed moments. The third factor comes from one column shared by all the functions.

In addition to the preceding sampling, choose a uniform column \(z\) of \(H_0\). For every balanced charge \(a\), define functions on this probability space by \[ F_0(a)=g_0(a)z^{-a},\qquad F_1(a)=\left(\frac15\sum_{s=1}^5g_s(a)\right)z^{-a}. \tag{31}\] The same sampled column \(z\) is used in every function \(F_t(a)\). This use of moments and positive Gram forms follows the broader polynomial-optimization approach to MUBs (Brierley and Weigert 2010; Gribling and Polak 2024); the shared-column functions above specify the particular forms used here.

In the formulas below, an index \(1\) on \(F\) denotes the average over five bases in (31); a label \(1\) in \(\mathcal M\) denotes a representative of those bases after taking expectation.

Reducing the Gram entries

The three-factor moments in Lemma 11 can be simplified using symmetry, character vanishing, and the identities of a complete family. When all factors refer to one matrix, the injective moments and equations from Section 3 apply as well.

In the finite calculation below, a mixed key consists of its factor labels and the matrix whose columns are its charges. The reductions in Lemma 12 apply to these keys. Single-label keys are expanded into the moments \(m(A)\), and the pair relations from Section 3 may then be used. If a single-label expression vanishes by part (ii), its expansion also gives a valid homogeneous relation among the \(m(A)\). These steps preserve the interpretation of every remaining symbol as an actual moment.

The six positive forms

Here are the finite collections of functions and integer weights used in the certificate. The exact data are the literal list named data in Appendix 8, also supplied in the companion file certificate/verify.py. Each record has the form \[(\lambda,\ \texttt{ws},\ e_\lambda,\ \texttt{a}).\] The list \(\texttt{ws}=((t_0,v_0),\ldots,(t_{m-1},v_{m-1}))\) specifies \(m\) pairs with \(t_i\in\{0,1\}\) and balanced \(v_i\in\mathbb Z^6\). The integer list \(\texttt{a}\) specifies a symmetric \(m\times m\) matrix \(Z_\lambda\) by its lower triangle in row order: with zero-based list indices, \[ (Z_\lambda)_{ij}=(Z_\lambda)_{ji} =\texttt{a}_{\,i(i+1)/2+j} \qquad(0\le j\le i<m). \tag{38}\] Thus the data define the matrices and lists without any optimization or choice of numerical tolerances. Their sizes and scales are

For each of these six lists of row lengths \(\lambda\), place the positions \(1,\ldots,5\), in order, in successive left-justified rows of lengths \(\lambda_1,\lambda_2,\ldots\). Let \(R_\lambda\) consist of permutations within these rows, and let \(C_\lambda\) consist of permutations within the resulting columns. Both groups act on \(\{0,\ldots,5\}\) by fixing position \(0\). Our convention for their action on charges is \[(P_pv)_i=v_{p(i)}.\] These signed row and column permutation sums are the usual Young-symmetrizer construction. Symmetry reduction of positive Gram forms is developed generally in (Gatermann and Parrilo 2004) and for MUB moment problems in (Gribling and Polak 2024). Here the finite sums are given explicitly, so their use requires no representation-theoretic decomposition theorem. Define the vector \(Y_\lambda\) by \[ (Y_\lambda)_i =\sum_{\substack{p\in R_\lambda\\q\in C_\lambda}} \operatorname{sgn}(q)\, F_{t_i}(P_pP_qv_i) \qquad(0\le i<m). \tag{39}\] In particular, \((P_pP_qv)_i=v_{q(p(i))}\), which is the order implemented by perm(perm(v,q),p) in the appendix. Formula (39) defines a finite linear combination of the functions (31) for every listed pair.

Exact certification of linear substitutions

Both certificates use finite systems of linear equations in their moment coordinates. The same substitution procedure applies to either system. Include the constant moment as a coordinate, so that every moment equation is homogeneous in the enlarged coordinate vector. Clearing denominators turns the equations into integer rows. The lists called I in the program specify a fixed priority order on the coordinates. This choice affects the form of the answer and, in the mixed calculation, the size of its residual coefficient sum; it does not add any relation.

Here is how eliminate verifies the hypotheses of the lemma. Its first modular elimination uses the prime \(1000000007\). The routine echelon retains an original integer equation whenever that equation supplies a new pivot. These retained equations form \(W\). Each pivot is at the largest remaining coordinate of its row; normalized elimination therefore proves that \(W_J\) is invertible modulo the prime. Back substitution processes pivot coordinates in ascending order. When a smaller pivot is removed, its already reduced row contains only that pivot and free coordinates. The final rule for a pivot thus has no other pivot on its right side.

The program then works modulo the further moduli listed in the source, retaining matching pivot sets, combines coefficients by the Chinese remainder algorithm, and uses rat to propose rational rules. These steps preserve the absence of other pivot coordinates. All nonpivot coordinates receive explicit identity rules. Finally, for each retained integer equation the program substitutes every proposed rule, clears all denominators, and checks that every integer coefficient is zero. This is the exact check \(WP=0\) in Lemma 14.

Every actual moment vector satisfies the selected equations, so this check suffices even if additional generated equations have not been used. In particular, the modular pivot count is not asserted to be the full rational rank of the original system. A prime that conceals an additional independent equation merely leaves that true equation unused. The rational reconstruction and its size threshold are ways to find a candidate \(P\); the exact check and the lemma establish its validity.

Pair equations and the vanishing identity

For an integer array \(A\) with zero row and column sums, put \[\operatorname{wt}(A)=\sum_i\mathop{\mathrm{ord}}(A_{i,*}).\] This also equals the sum of the column orders. Arrays name the real injective moments \(m_H(A)\) of Section 3; the empty array names the constant moment \(1\). A formal linear expression in these moments is stored as a finite list of rational coefficients indexed by arrays. Coefficients at the same index are added, and zero coefficients are discarded. These are the operations add and lin in the program.

The routine canonpair selects a representative using precisely the symmetries of \(m_H\): permutation of either axis, removal of zero rows and columns, global negation, and transposition. More explicitly, after removing zero axes it considers \(A,-A,A^{\mathsf T},-A^{\mathsf T}\), retains orientations with at least as many rows as columns, orders columns by their positive-part orders, and minimizes over the remaining column permutations after lexicographically sorting the rows. Each operation preserves the moment by its definition and Lemma 4. The degree orders and lexicographic choices serve only to select consistent names.

Define \(U_0(A)\) recursively as a linear expression in representatives whose nonzero row and column orders are all at least two. If a row of \(A\), or of \(A^{\mathsf T}\), has order one, apply Lemma 4 in that orientation: \[ U_0(A)=-\frac{1}{7-p}\sum_{\ell\ne i}U_0(A_{i\to\ell}), \qquad p\le6. \tag{43}\] Canonicalize each contracted array before continuing. If no such row exists on either axis, retain its moment as a single coordinate. The empty array is retained in the same way. Every contraction reduces the sum of the two axis lengths, so this recursion terminates. This is evpair; expand_degree1 supplies the unsigned sum of contractions. The program checks that every evaluated array has both dimensions at most six and has zero sums on both axes.

The pair table is formed from formal seven-row equations. The exact enumeration restrictions are as follows:

1. Choose a total weight \(k\in\{7,8,9,10,11\}\) and a column count \(q\) with \(2\le q\le\min(4,\lfloor k/2\rfloor)\).

2. Choose nondecreasing sequences of seven row orders \((r_0,\ldots,r_6)\) and \(q\) column orders \((c_0,\ldots,c_{q-1})\). Both sequences sum to \(k\), and \[1\le r_i\le\lfloor k/2\rfloor, \qquad 2\le c_j\le\lfloor k/2\rfloor.\]

3. Enumerate integer \(7\times q\) arrays with zero row and column sums and exactly these orders. Rows of equal order may be put in lexicographic order, and arrays with the same canonical representative may be skipped.

The routines parts, comps, and allAB implement this enumeration. A row is generated as the difference of disjointly supported nonnegative compositions of its prescribed order, within the remaining positive and negative column capacities. The capacities enforce the prescribed column orders. The first row has order one: seven positive integer row orders with sum at most eleven cannot all be at least two, and the orders are sorted.

For each retained array, the seven-row boundary case of Lemma 4 gives the equation \[ \sum_{\ell=1}^{6}U_0(A_{0\to\ell})=0. \tag{44}\] Here \(0,\ldots,6\) index the formal rows, not coordinates of a charge. Only the contracted arrays, which have at most six rows, are evaluated. The checks in pairtable verify the balance, number of formal rows, and order of the first row before forming this equation. Skipping an array can only omit an available true equation; the proof does not require a complete set of moment relations.

Apply Lemma 14 to these equations. Write \(U(A)\) for the resulting expansion of \(U_0(A)\) in the retained moment coordinates. For a product used here, with charge columns \(a_1,\ldots,a_n\) and \(n\le4\), let \(A_{\mathcal S}\) be the array obtained by adding the columns in each block of a set partition \(\mathcal S\) of \(\{1,\ldots,n\}\). The final pair expansion is \[ \sum_{\substack{\mathcal S\text{ a set partition}\\|\mathcal S|\le6}} \frac{(6)_{|\mathcal S|}}{6^n}\,U(A_{\mathcal S}). \tag{45}\] This is exactly Lemma 5. The routine partition enumerates set partitions by numbering blocks in order of first occurrence, and rep_pair implements (45). The routine apair first forms the array of charge columns. It may remove a zero charge before the expansion, since that removes the factor \(g_H(0)=1\). Deletion of zero coordinate rows is also legitimate: a uniform injection on the retained positions has the required uniform marginal.

For the pair certificate, check_pair forms the displayed polynomial \(L_H\) of Proposition 6, with coefficients \(-1,2,1,1,1\). It multiplies each monomial by the conjugate of every monomial, expanding \(3|L_H|^2\) through (45). For each of the two stated charges \(q\), it adds the expansion with charge columns \((\alpha,q,-\alpha,-q)\). After the exact pair substitutions, the result has no nonzero coefficient, for either \(q\). This proves the identity in Proposition 6; all expressions used in the check have been identified with their actual averaged moment values above.

Mixed keys and the finite mixed table

We use the notation \(\mathcal M(\mathbf s;\mathbf a)\) and \(m(A)\) from Section 6. The latter is the average of \(m_H(A)\) over the ordered basis pairs. A mixed key consists of a label tuple \(\mathbf s\) and an array \(A\) whose columns are the charges. The array has at most six nonzero coordinate rows. Its rows and columns sum to zero. The routine cmix chooses representatives by simultaneous factor and label permutations, renaming labels by order of first occurrence, sorting the common coordinate rows, global negation, and removing zero factors and zero coordinate rows. These are exactly the symmetries justified in Lemma 12. The separate tag \((\varnothing,A)\) names the pair moment \(m(A)\); the completely empty key names \(1\).

The routine evmix supplies the following recursive expansion of a key into named moment coordinates:

1. If a charge has order one or is a permutation of \(\alpha\), the mixed moment is zero.

2. When at most one label remains, expand the product by (45), now using the averaged pair moments \(m(A)\), and attach the pair tag to its coordinates. If this single-label expression was zero by the preceding rule, also record its pair expansion as a zero equation. These recorded equations are stored in rows0.

3. Otherwise, if an order-two charge has a label occurring exactly once among the factors, let \(l\) be the number of labels in use and replace that label in turn by each of the other \(l-1\) labels. The original moment is \(-1/(7-l)\) times the sum of the resulting moments. Apply the same rules recursively to each term.

4. If none of these rules applies, retain the key as an original mixed-moment coordinate.

The zero rules and the singleton coefficient follow from Lemma 12. Each singleton replacement decreases the number of distinct labels. The single-label use of the pair table is legitimate because the real average over ordered pairs includes the required transpose symmetry, as proved in that lemma.

The finite enumeration of triples is given by triples(11). For precision, it generates balanced charges \(a,b,c\in\mathbb Z^6\) with \[\begin{gathered} a+b+c=0,\qquad 0\le\mathop{\mathrm{ord}}(c)\le\mathop{\mathrm{ord}}(b)\le\mathop{\mathrm{ord}}(a)\le5,\\ \mathop{\mathrm{ord}}(a)+\mathop{\mathrm{ord}}(b)+\mathop{\mathrm{ord}}(c)\le11. \end{gathered}\] Choose \(a\) up to a coordinate permutation and sign by taking the lesser of its sorted entries and the sorted entries of \(-a\). Enumerate all balanced \(b\) of orders at most \(\mathop{\mathrm{ord}}(a)\), put \(c=-a-b\), and retain those meeting the displayed restrictions. Sorting the six rows of the array \((a,b,c)\) removes common-coordinate duplicates. Balanced vectors of a given order are generated by subtracting two disjointly supported nonnegative compositions of that order, which is the routine vecs.

For each generated array, mixeq first evaluates all five equality patterns on its three labels, registering any single-label zero equations. It then considers the distinct permutations of the three charge columns, choosing \(a\le b\) lexicographically to avoid duplicated first-two-column orderings. Write \[a_{ij}=a+e_i-e_j,\qquad b_{ij}=b-e_i+e_j \quad (0\le i,j\le5).\] The following equations are included after applying evmix to every term:

• For different first two labels, sum the moments with charges \((a_{ij},b_{ij},c)\) over all \(i\ne j\), obtaining zero by (14). For nonzero \(c\), use the label tuples \((0,1,2)\), \((0,1,0)\), and \((0,1,1)\); for \(c=0\), use \((0,1,0)\). Include this equation only if all \(36\) shifted triples have total order at most eleven.

• For equal first two labels, fix \(i\), sum over all six \(j\), and subtract the moment with charges \((-c,c)\) and labels \((0,u)\), by (13). Use \((0,0,u)\) with \(u=0,1\) when \(c\ne0\), and \(u=0\) when \(c=0\). Also use the reversed shifts \((a+e_j-e_i,b-e_j+e_i,c)\). Include each equation only if all its six shifted triples have total order at most eleven.

The third charge is unchanged in these sums because the equations have been multiplied by its factor. On the right side of the equal-label equation, \(a+b=-c\), which explains both remaining charges and the labels selected by s[-2:] in the source.

Finally add the pair equations recorded in rows0. All coordinates encountered by these reductions are registered, including coordinates that cancel in a particular equation. With the specified coordinate order, mixtable applies Lemma 14 to the nonzero equations. A vanishing expression encountered later may still be replaced by zero: its vanishing is an independently proved rule, whether or not its pair expansion was used to strengthen this table. No completeness of the enumeration, and no vanishing of unlisted higher-order moments, is assumed.

The exact table dimensions are as follows. The witness column counts the independent equations used in Lemma 14.

Positive matrices and the negative bound

For the mixed certificate, the literal data in Appendix 8 specify the six lists and lower triangles of the symmetric integer matrices \(Z_\lambda\). The routine makeZ checks the number of entries and reconstructs each symmetric matrix. Positive definiteness is verified without eigenvalue approximation. At each step, posdef writes the remaining matrix as \[B=\begin{pmatrix}C&u\\u^{\mathsf T}&p\end{pmatrix}, \qquad p>40000,\] and replaces it by the exact Schur complement \(C-uu^{\mathsf T}/p\). The identity \[\begin{pmatrix}x\\t\end{pmatrix}^{\!*} B\begin{pmatrix}x\\t\end{pmatrix} =x^*(C-uu^{\mathsf T}/p)x +p\left|t+\frac{u^{\mathsf T}x}{p}\right|^2\] shows inductively that positive pivots prove positive definiteness, also for complex vectors. All \(98\) pivots in the six matrices satisfy the asserted rational inequality.

The routines permsign and polynomial implement the signed permutation sums defining \(Y_\lambda\) in Section 6. The convention \((P_pv)_i=v_{p(i)}\) gives \((P_pP_qv)_i=v_{q(p(i))}\), exactly perm(perm(v,q),p). The routine tagmom uses the Gram charges \((a,-v,v-a)\) of Lemma 11. After multiplying the entire form by five, product assigns weight five unless both function types are one; in that case the weights for equal and different external labels are one and four. The lower-triangle summation in gaps doubles the off-diagonal terms. Since the polynomial coefficients and \(Z_\lambda\) are real, its real-moment expansion equals the full quadratic form for complex \(Y_\lambda\).

Consequently the expression formed by gaps is exactly \[\mathcal Q= 5\sum_\lambda 10^{15-e_\lambda} \mathbb E\bigl(Y_\lambda^*Z_\lambda Y_\lambda\bigr).\] Apply evmix and then the certified mixed substitutions. On combining coefficients, we obtain the residual expansion in (41), now indexed by the program’s moment keys: \[ \begin{gathered} \mathcal Q=c_0+\sum_{K\ne\varnothing}c_K\,\mu_K,\\ c_0=-\frac{613302797399911}{6480},\qquad \sum_{K\ne\varnothing}|c_K| =\frac{179721388988719}{6480}. \end{gathered} \tag{46}\] Here \(\mu_K\) denotes the original moment named by a retained coordinate; the notation \(K\ne\varnothing\) excludes the completely empty constant key. Both equalities of rational coefficients in (46) are checked exactly by the program, as is their strictly negative sum.

It remains to justify the bound on these residual coordinates. A tagged pair coordinate is a real average of unit-modulus monomials, so \(|m(A)|\le1\). A mixed coordinate is a real average of products of \(g_s(a)\), each of absolute value at most one, so \(|\mathcal M(\mathbf s;\mathbf a)|\le1\). Every coordinate retained by the substitutions is one of these original moments. The new linear combinations occur as expressions in the coordinates, not as newly named coordinates to which a bound is assigned. The constant coordinate is exactly one. Hence \[0\le\mathcal Q \le c_0+\sum_{K\ne\varnothing}|c_K| =-\frac{2007321335237}{30}<0.\] This proves Proposition 13. Together with the pair coefficient check, it completes the exact verification of both certificates using only the finite equations and integer data specified in Appendix 8.