1 The matrix construction
This chapter sets up the input data that the rest of the proof consumes: the 42-element basis, the closed-form entries of \(M_1\) and \(M_2\), the \(\mathbb {Z}\)-level cross-multiplication checks that anchor the FLINT-shipped integer matrices to those closed forms, the kernel-Qed bridge between the rat-level paper-form spec and the Z-level computational spec, and the bridge into MathComp’s \(\mathbb {Q}\)-level matrices. All material here lives inside the files MaynardSpec.v, MaynardBasis.v, MaynardFactQ.v, the MaynardVerify/ directory (Def.v, six parallel M2_0..5.v chunks, and the assembly MaynardVerify.v), and MaynardSpecBridge.v. Throughout this chapter we follow the v3/Annals numbering of Maynard’s paper: Lemma 8.1 / 8.2 / 8.3 (= Lemma 7.1 / 7.2 / 7.3 in v1).
1.1 Conventions
The two power sums are \(P_1 = \sum _i t_i\) and \(P_2 = \sum _i t_i^2\). The basis monomials are \(F_{b,c} = (1 - P_1)^b \cdot P_2^c\) with \(b + 2c \le 11\). Indices \((b_i, c_i)\), \((b_j, c_j)\) denote bidegrees of the \(i\)-th and \(j\)-th basis monomials. The outer integration dimension is \(k = 105\); we use two constants \(K_1 = 105\) (outer simplex) and \(K_2 = 104 = K_1 - 1\) (residual simplex after the eq. 8.8 substitution that integrates out \(t_1\)).
\(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\)).
1.2 The 42-element basis
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:
\(\# \{ (b, c) \in \mathbb {N}^2 : b + 2c \le 11\} = 42\).
\(\sum _{c=0}^{5}(12 - 2c) = 12 + 10 + 8 + 6 + 4 + 2 = 42\). A single vm_compute on the list closes it.
\(\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.
vm_compute on a list of 42 pairs.
For every \(p \in \mathbb {N}\times \mathbb {N}\),
The basis is permutation-equal to the canonical filter
by a vm_compute perm_eq lemma, and canonical_basis satisfies the spec by construction (mem_filter + allpairs_f; the residual \(2c \le 11 \Rightarrow c {\lt} 6\) step closes by lia).
\(\texttt{uniq}\; \texttt{maynard\_ basis}\).
vm_compute on the 42-pair list.
Lemmas 3, 5, and 6 together pin maynard_basis to exactly the multiset \(\{ (b, c) \in \mathbb {N}^2 : b + 2c \le 11\} \). A reviewer never has to inspect the literal 42-pair list — the basis is fully characterised by the predicate \(b + 2c \le 11\), the size \(42\), and the absence of duplicates. Order matters because the matrix rows and columns and the entries of the rational witness vector \(v_{\mathrm{witness}}\) (Definition 19) must all align with the same indexing in \(M_{1,2}^{\mathrm{int}}\).
This is a lower-bound subspace argument. Maynard’s full optimisation is over all symmetric \(F\) of degree \(\le 11\) in \(k = 105\) variables; restricting to polynomials in the two power sums \(P_1, P_2\) is a strict subspace, and the supremum of a Rayleigh quotient over a subspace is \(\le \) the unrestricted supremum. So a lower bound of \(4/105\) on the 42-dimensional restricted problem yields \(M_k[105] {\gt} 4\).
1.3 The polynomial \(G_{n,2}(k)\) (Lemma 8.1)
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 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 \(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.
\(G_{0, 2}(k) = 1\), \(G_{1, 2}(k) = 2k\), \(G_{2, 2}(k) = 4 k^2 + 20 k\).
\(G_{1, 2}(k)\): the only length-1 composition of \(1\) is \([1]\), with \(\mathrm{cff}([1]) = 2!/1! = 2\), so the sum is \(1! \cdot \binom {k}{1} \cdot 2 = 2k\). \(G_{2, 2}(k)\): length-1 contributes \(\binom {k}{1} \cdot \mathrm{cff}([2]) = k \cdot 4!/2! = 12k\); length-2 contributes \(\binom {k}{2} \cdot \mathrm{cff}([1,1]) = \binom {k}{2} \cdot (2 \cdot 2) = 2k(k-1)\); total \(= 2! \cdot (12k + 2k(k-1)) = 2(12k + 2k^2 - 2k) = 4k^2 + 20k\). Both also reduce by vm_compute.
1.4 Closed forms for \(M_1\) and \(M_2\) (Lemma 8.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, 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 \((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 matrices have up to \(36\) rational summands per entry (when \(c_i = c_j = 5\)), with intermediate denominators reaching \(\sim 10^{7000}\) digits before the rational normalisation collapses them. This is why MaynardSpec.v also ships \(\mathbb {Z}\)-level twins (m1_num_den, m2_num_den) that keep the \((\text{num}, \text{den})\) pair separate; MaynardVerify.v operates on those twins to avoid rat’s canonical gcd-normalisation cost during vm_compute.
1.5 Kernel cross-check: matrices match the spec
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.
The \(1764\) Boolean cross-multiplication checks M1_entry_matchZ \(i\, j\) are aggregated into all_match_M1Z \(=\) forallb over \(42 \times 42\), and the Lemma is closed by a single vm_compute. The check costs \({\sim }90\) s wall-clock. Print Assumptions reports only the standard \(\mathsf{Uint63}\) primitives.
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\).
Same shape as Theorem 14, but the entries are double sums of up to 36 rational terms, so the per-row vm_compute cost is significant. The check is split into six 7-row chunks (MaynardVerify/M2_0..5.v) that make -j runs concurrently, and the assembly stitches them via seq_split_42 plus forallb_app — no per-entry recomputation in the Qed of all_match_M2Z_true itself. Print Assumptions: only the standard \(\mathsf{Uint63}\) primitives.
Theorems 14 and 15 together close the trust gap on the input data: every entry of the \(42 \times 42\) integer matrices that the rest of the proof consumes is kernel-verified to agree with Maynard’s closed-form specification (Lemma 8.2). The FLINT generator is therefore not part of the trust base for the input data either.
1.6 Paper-form \(\leftrightarrow \) computational-form spec bridge
The cross-checks above operate on the \(\mathbb {Z}\)-level twins (m1_num_den, m2_num_den) because vm_compute on \(\rat \)-level matrices stalls on MathComp’s HB canonical-structure elaboration at concrete dimension \(42\). The rat-level spec (M1_entry, M2_entry) is the documentation-shaped form a reviewer reads side by side with arXiv:1311.4600 §8. The bridge below certifies in the kernel that the two forms encode the same closed forms: a single Qed per matrix, with no axioms.
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 every \((i, j) \in \{ 0, \ldots , 41\} ^2\),
Layered structural induction in theories/S1/MaynardSpecBridge.v: factZ_to_rat, dblratZ_to_rat, binZ_to_rat, compositionsZ_eq_compositions, G2Z_to_rat, and m1_num_den_to_rat compose into a single rewrite chain. Print Assumptions reports Closed under the global context: no axioms, not even \(\mathsf{Uint63}\) primitives.
For every \((i, j) \in \{ 0, \ldots , 41\} ^2\),
Same layered induction, with two extra steps for the running \(\texttt{qplus}\) accumulator: qfrac_qmul and qfrac_qplus bridge qmul / qplus on \(\mathbb {Z}\times \mathbb {Z}\) pairs to \(*\) / \(+\) on \(\rat \), and a generic \(\texttt{fold\_ left qplus} \to \sum \) lemma collects the double sum over \((c'_1, c'_2)\). Print Assumptions: Closed under the global context.
Theorems 17 and 18 live in MaynardSpecBridge.v, a leaf in the dependency DAG: Cert.v does not import them, and the headline theorem does not depend on them. Their job is purely to certify that the documentation-shaped \(\rat \)-level definitions (Definitions 11 and 13, written to match Maynard’s paper character for character) and the \(\texttt{vm\_ compute}\)-shaped \(\mathbb {Z}\)-level definitions (m1_num_den, m2_num_den, consumed by Theorems 14 and 15) compute the same rational. Combined with those theorems, this gives a two-step kernel-verified path from each shipped integer matrix entry back to Maynard’s exact closed form.