Maynard’s \(M_{105} {\gt} 4\) — a Rocq replacement for the Mathematica notebook

4 Numerical highlights

Matrix dimension.

\(42 \times 42\). Maynard’s \(M_k[105]\) construction uses \(42\) basis polynomials \(\{ F_{b,c} : b + 2c \le 11\} \).

Denominators.

\(D_{M_1}\) has \({\sim }221\) decimal digits, \(D_{M_2}\) \({\sim }227\). Both are strictly positive (vm_compute).

Witness denominators.

The \(42\) rational entries of \(v_{\mathrm{witness}}\) (Definition 19) have denominators bounded by \(67\, 213\, 321\, 643\, 309 \approx 1.4 \cdot 10^{13}\) (\({\sim }14\) decimal digits, \(46\) bits). The smallest non-zero \(|v_i|\) is \(\approx 10^{-14}\) and the largest is \(\approx 1\), so the eigenvector spans \({\sim }14\) decimal orders of magnitude — this lower-bounds the denominator size, since truncating small components destroys the inequality.

Verified slack.

\((105 \cdot v^T M_2v - 4 \cdot v^T M_1v) / v^T M_1v \approx +2.07 \cdot 10^{-3}\).

Build profile.

On a \(16\) GB / \(6\)-thread machine: \({\sim }25\)–\(30\) min wall-clock with make -j6 (clean rebuild). The dominant single-Qed costs are:

  • Theorem 15 (all_match_M2Z_true): \({\sim }35\) min sequentially across the six \(7\)-row chunks (MaynardVerify/M2_0..5.v), reduced to a per-chunk wall of a few minutes under make -j — \(1764\) entries, each up to \(36\) rational summands with intermediate denominators reaching \(\sim 10^{7000}\) digits.

  • Theorem 14: \({\sim }90\) s.

  • Theorem 24 (rayleigh_witness_holds): \({\sim }5\) s — a single BigZ comparison of two large products.

  • Witness.v parsing: \({\sim }30\) s — \(\mathsf{BigZ}\) literal parser on the shipped matrix coefficients.

With make -j6 the six \(M_2\) chunks run concurrently, so the wall clock is bounded by the slowest single chunk plus the linear assembly tail.

Project size.

\(20\) .v files under theories/S1/ (\(13\) top-level plus \(7\) in the MaynardVerify/ parallel-chunk subdirectory), \({\sim }9{,}590\) lines total; Witness.v alone is \({\sim }5{,}700\) lines of autogenerated certificate data, and Witness_Quad.v is \({\sim }80\) lines of \(42\) \((\mathrm{num}, \mathrm{den})\) pairs.