Dependencies

For \(b, c, c' \in \mathbb {N}\) with \(c' \le c\),

This is the coefficient of \((1 - \sum _{j \ne 1} t_j)^{b + 2c - 2c' + 1} \cdot (\sum _{j \ne 1} t_j^2)^{c'}\) in the expansion of \(\int _0^{1 - \sum _{j \ne 1} t_j} (1 - P_1)^b P_2^c \, dt_1\), obtained by expanding \(P_2^c = (t_1^2 + \sum _{j \ne 1} t_j^2)^c\) binomially and integrating \(t_1^{2(c - c')} (1 - \sum _j t_j)^b\) via the Beta-function identity \(\int _0^X t^a (X - t)^b \, dt = a! b! X^{a + b + 1} / (a + b + 1)!\).

For a composition \(a = (b_1, \ldots , b_r)\),

This is exactly the per-composition inner product appearing in Maynard’s Lemma 8.1 (with \(j = 2\), so \(j b_s = 2 b_s\)).

For \(r, n \in \mathbb {N}\), \(\mathrm{compositions}(r, n) := \{ (b_1, \ldots , b_r) \in \mathbb {N}_{\ge 1}^r : \sum _s b_s = n\} \), returned as a list in lexicographic order. For \(r = 0\) this is the singleton \(\{ [\, ]\} \) if \(n = 0\) and empty otherwise; for \(r = n + 1\) or larger it is empty.

For \(n, k \in \mathbb {N}\): \(G_{0, 2}(k) = 1\), and for \(n \ge 1\),

This is Lemma 8.1 of arXiv:1311.4600 v3 character-for-character: the \(n!\) prefactor, the outer \(r\)-sum, the binomial coefficient, the inner sum over length-\(r\) compositions of \(n\), and the inner product \(\prod _s (j b_s)!/b_s!\) with \(j = 2\) all appear at the same positions.

\(K_1 := 105\), \(K_2 := 104\). The first is the outer simplex dimension (used in \(M_1\) and in the threshold \(4/K_1\)); the second is the residual simplex dimension after the eq. 8.8 substitution (used in \(M_2\)).

For \((b_i, c_i, b_j, c_j)\) basis bidegrees, set \(b = b_i + b_j\) and \(c = c_i + c_j\). Then

This is Lemma 8.2 (first part) of arXiv:1311.4600 v3 verbatim, with \(K_1 = k = 105\).

For \((b_i, c_i, b_j, c_j)\) basis bidegrees, with \(b'_1 = b_i + 2c_i - 2c'_1 + 1\), \(b'_2 = b_j + 2c_j - 2c'_2 + 1\), \(b_{\mathrm{sum}} = b'_1 + b'_2\), \(c_{\mathrm{sum}} = c'_1 + c'_2\):

This is Lemma 8.2 (second part) of arXiv:1311.4600 v3 for the per-coordinate integrand \(J_k^{(1)}\) (not \(\sum _m J_k^{(m)}\)): the symmetry factor \(k\) is paid in the threshold \(4/k\), not in the matrix entries.

The Maynard basis is the explicit list of 42 pairs \((b, c) \in \mathbb {N}^2\) with \(b + 2c \le 11\), in the Mathematica enumeration order used by flint_probe.py:

\(\texttt{num\_ M1} := \texttt{quad}\, M_1^{\mathrm{int}}\, \vnum \) and \(\texttt{num\_ M2} := \texttt{quad}\, M_2^{\mathrm{int}}\, \vnum \). After clearing the common denominator \(\DMl \cdot \vden ^2\) on both sides, the strict Rayleigh-quotient bound \(4 \cdot v^T M_1v {\lt} 105 \cdot v^T M_2v\) on the FLINT integer matrices becomes the strict integer inequality \(4 \cdot D_{M_2}\cdot \texttt{num\_ M1} {\lt} 105 \cdot D_{M_1}\cdot \texttt{num\_ M2}\).

For \((n, d) \in \mathbb {Z}\times \mathbb {Z}\), set \(\texttt{qfrac}(n, d) := \frac{n}{d} \in \rat \) (MathComp’s int–to–rat morphism applied component-wise, then divided). This reads a \((\text{numerator}, \text{denominator})\) pair as the rational it represents.

For \(M : \texttt{list (list }\mathbb {Z}\texttt{)}\) and \(v : \texttt{list }\mathbb {Z}\), \(\texttt{quad}\, M\, v := v^T \cdot M \cdot v\) (the standard quadratic form on integer lists), implemented via \(\texttt{row\_ dot} : \texttt{list }\mathbb {Z}\to \texttt{list }\mathbb {Z}\to \mathbb {Z}\) (dot product, with the implicit pad-to-shorter convention) and \(\texttt{mat\_ vec\_ mul}\) (row-wise dot of \(M\) with \(v\)).

For an entry-wise spec \(M_{\mathrm{spec}} : \nat \to \nat \to \rat \),

where \(v_{\rat }(i) := \texttt{Z2rat}(\vnum [i]) / \texttt{Z2rat}(\vden )\). This is the standard Rayleigh-quotient numerator \(v^T M v\) on the paper-form spec matrices, expanded as a \(\sigb \) bigop (the form the headline statement consumes).

\(\vden := \mathrm{lcm}\, (d_0, \ldots , d_{41})\) is the LCM of the 42 witness denominators, computed by a left fold over \(v_{\mathrm{witness}}\). The scaled integer numerators \(\vnum : \texttt{list }\mathbb {Z}\) are defined by \(\vnum [i] := n_i \cdot (\vden / d_i)\), so that \(v[i] = \vnum [i] / \vden \) as rationals. This presentation puts every component over the same denominator, which is what allows the Rayleigh inequality to reduce to a single integer comparison after clearing the matrix denominators \(D_{M_1}, D_{M_2}\).

\(v_{\mathrm{witness}} : \texttt{list }(\mathbb {Z}\times \mathbb {Z})\) is a list of 42 pairs \((n_i, d_i)\) with \(\gcd (|n_i|, d_i) = 1\) and \(d_i {\gt} 0\), representing the rational vector \(v \in \rat ^{42}\) with \(v[i] = n_i / d_i\). The list is autogenerated by python/build_quad_witness.py from the top eigenvector of \(M_1^{-1}M_2\) (computed via acb_mat.eig at \(1024\)-bit precision), phase-aligned (largest entry positive real), and snapped to small-denominator rationals via Mathematica-style absolute-tolerance Rationalize with \(\mathrm{tol} = 10^{-14}\) (continued-fraction convergents). The entries are listed in the same row/column order as MaynardBasis.maynard_basis (Definition 2).

\(\texttt{maynard\_ basis} = \texttt{Witness.basis}\), i.e. the hand-readable basis in MaynardBasis.v agrees literally with the autogenerated basis used to index the shipped integer matrices in Witness.v.

\(\# \{ (b, c) \in \mathbb {N}^2 : b + 2c \le 11\} = 42\).

For every \(p \in \mathbb {N}\times \mathbb {N}\),

\(\texttt{uniq}\; \texttt{maynard\_ basis}\).

\(G_{0, 2}(k) = 1\), \(G_{1, 2}(k) = 2k\), \(G_{2, 2}(k) = 4 k^2 + 20 k\).

For every \((i, j) \in \{ 0, \ldots , 41\} ^2\),

The analogous identity holds for \(M_2\): \(\texttt{M2\_ spec\_ ij}(i, j) = \texttt{Z2rat}(M_2^{\mathrm{int}}[i][j]) / \texttt{Z2rat}(D_{M_2})\) for all \((i, j) \in \{ 0, \ldots , 41\} ^2\).

For \(\texttt{dm}, \texttt{vd}, v_i, m_{ij}, v_j : \rat \) with \(\texttt{vd} \ne 0\) and \(\texttt{dm} \ne 0\),

Given a spec \(M_{\mathrm{spec}}\) and an integer matrix \(M_{\mathrm{int}}\) such that \(M_{\mathrm{spec}}(i,j) = \texttt{Z2rat}(\texttt{mat\_ get}\, M_{\mathrm{int}}\, i\, j) / \texttt{Z2rat}(D_M)\) for all \((i, j) {\lt} 42\), with \(D_M {\gt} 0\) and \(M_{\mathrm{int}}\) a \(42 \times 42\) matrix,

Let \(d_1, d_2, a_1, a_2 \in \mathbb {Z}\) with \(d_1, d_2 {\gt} 0\), \(v \in \rat \) with \(v {\gt} 0\), and \(q_1, q_2 \in \rat \). Suppose

and the integer comparison \(\texttt{Z2rat}(4 \cdot d_2 \cdot a_1) {\lt} \texttt{Z2rat}(105 \cdot d_1 \cdot a_2)\) holds. Then \(4 \cdot q_1 {\lt} 105 \cdot q_2\) in \(\rat \).

For any well-formed \(M : \texttt{list (list }\mathbb {Z}\texttt{)}\) of dimension \(42 \times 42\) and \(v_{\mathrm{num}}\) of length \(42\),

The conjunction

where \(\texttt{Z2rat}\, (z : \mathbb {Z}) : \rat := (\texttt{Z\_ to\_ int}\, z)\% \texttt{:\~{}R}\) is the thin \(\mathbb {Z}\to \rat \) embedding.

For every \((i, j) \in \{ 0, \ldots , 41\} ^2\),

where \(M_1^{\mathrm{int}}\) is the FLINT-shipped integer matrix and \((\texttt{m1\_ num}, \texttt{m1\_ den})\) are the closed-form \((\text{numerator}, \text{denominator})\) from Definition 11.

For every \((i, j) \in \{ 0, \ldots , 41\} ^2\),

The analogous identity holds for \(M_2\): \(\texttt{m2\_ num}(i, j) \cdot D_{M_2}= M_2^{\mathrm{int}}[i][j] \cdot \texttt{m2\_ den}(i, j)\) for all \((i, j) \in \{ 0, \ldots , 41\} ^2\).

For every \((i, j) \in \{ 0, \ldots , 41\} ^2\),

\(0 {\lt} \texttt{num\_ M1}\) in \(\mathbb {Z}\).