2 The Rayleigh-quotient witness route
This chapter is the analytic heart of the proof. Maynard’s Lemma 8.3 reduces \(M_k[k] {\gt} c\) to: exhibit a single coefficient vector \(a \in \rat ^{42}\) with \(k \cdot a^T M_2a / a^T M_1a {\gt} c\), equivalently \(c \cdot a^T M_1a {\lt} k \cdot a^T M_2a\) (and \(a^T M_1a {\gt} 0\) so the quotient is well-defined). The shipped rational vector \(v_{\mathrm{witness}}\) in Witness_Quad.v is such an \(a\) for \((k, c) = (105, 4)\). The kernel verifies the strict integer inequality at \(v_{\mathrm{witness}}\) by a single vm_compute reflexivity on \(\mathbb {Z}\)-arithmetic; the supplementary algebraic shim lifts that integer fact to the rat-level bigop the headline surfaces.
The material lives in Witness_Quad.v (the witness vector itself) and CertRayleigh.v (the integer Rayleigh inequality, its positivity companion, and the rat-level lift to the bigop on the paper-form spec matrices).
2.1 The 42-entry rational witness vector
\(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).
The maximum denominator across the 42 entries is \(67\, 213\, 321\, 643\, 309 \approx 1.4 \cdot 10^{13}\), i.e. about \(46\) bits. The eigenvector spans \(\approx 14\) decimal orders of magnitude (smallest non-zero \(|v_i| \approx 10^{-14}\), largest \(\approx 1\)), which lower-bounds the denominator size: truncating small components destroys the Rayleigh inequality. The verified slack at this witness, in exact rationals, is
2.2 Integer reduction of the witness
\(\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}\).
2.3 Integer Rayleigh inequality
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\)).
\(\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}\).
\(0 {\lt} \texttt{num\_ M1}\) in \(\mathbb {Z}\).
A single vm_compute reflexivity in pure \(\mathbb {Z}\)-arithmetic. Print Assumptions reports Closed under the global context — no \(\mathsf{Uint63}\) primitives.
A single vm_compute reflexivity on the integer comparison (\({\sim }5\) s on a contemporary machine). Both sides are huge integers (the matrix denominators reach \({\sim }220\) decimal digits and the witness denominator \(\vden \) has \({\sim }40\) digits), but the comparison itself is one BigZ subtraction. Print Assumptions reports Closed under the global context.
Theorems 23 and 24 are the entire integer-arithmetic content of the headline theorem. If the Python layer shipped a vector \(v_{\mathrm{witness}}\) that failed the inequality, the kernel vm_compute would fail to reduce to true and the build would stop. The eigenvector itself is not in the trust base; only the resulting integer inequality is.
2.4 Lifting to the rat-level Rayleigh bound
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).
For any well-formed \(M : \texttt{list (list }\mathbb {Z}\texttt{)}\) of dimension \(42 \times 42\) and \(v_{\mathrm{num}}\) of length \(42\),
Structural induction on the dimension via the row_dot / mat_vec_mul chain. The base step \(n = 0\) collapses both sides via big_ord0; the inductive step combines big_ord_recl with the morphism lemmas \(\texttt{Z2rat\_ add}\), \(\texttt{Z2rat\_ mul}\) for the outer row_dot, then mulr_sumr to distribute over the inner sum.
For \(\texttt{dm}, \texttt{vd}, v_i, m_{ij}, v_j : \rat \) with \(\texttt{vd} \ne 0\) and \(\texttt{dm} \ne 0\),
A direct field call under the nonzero hypotheses. The lemma is intentionally Qed-sealed at top level so that its proof term is not unfolded inside the \(42 \cdot 42 = 1764\) nested binders of the bigop in Lemma 28.
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,
A single application of Lemma 26 (to recast the right-hand side as the rat-level bigop on \(\texttt{mat\_ get}\) / \(\vnum \)) followed by two nested \(\texttt{eq\_ bigr}\) applications of Lemma 27 to clear the per-cell denominators \(D_M\) and \(\vden \). Qed-sealing the per-cell identity keeps the bigop walk referring to it by name instead of inlining a fresh field proof term under each of the \(42 \cdot 42 = 1764\) binders, so the proof term stays small for kernel verification. The outer \(\texttt{mulr\_ sumr}\) rewrite is restricted to \([LHS]\) to keep unification cheap. Print Assumptions reports Closed under the global context.
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 \).
Multiply both sides of the goal by the strictly positive scalar \(\texttt{Z2rat}(d_1) \cdot \texttt{Z2rat}(d_2) \cdot v^2\) (monotonicity of \({\lt}\) under positive multiplication, \(\texttt{ltr\_ pM2r}\)); then \(\texttt{ring}\) on the two scaled-quad hypotheses rewrites each side into \(\texttt{Z2rat}(4 \cdot d_2 \cdot a_1)\) and \(\texttt{Z2rat}(105 \cdot d_1 \cdot a_2)\) respectively, and the result is the integer comparison hypothesis. Abstracting over \(q_1, q_2, v\) and the four \(\mathbb {Z}\) scalars keeps the two ring calls operating on tiny abstract scalars rather than on the concrete quad_spec bigops, so the proof term stays small. Print Assumptions: Closed under the global context.
A one-line exact: application of Lemma 29 to the two specialisations \(\texttt{quad\_ M\{ 1,2\} \_ spec\_ eq\_ Z}\) of Lemma 28 (at \((M_{\mathrm{spec}}, M_{\mathrm{int}}, D_M) = (\texttt{M1\_ spec\_ ij}, M_1^{\mathrm{int}}, D_{M_1})\) and the \(M_2\) analogue, discharged by Lemmas 32 and 33), together with \(\texttt{rayleigh\_ witness\_ holds\_ rat}\) — the integer Rayleigh inequality of Theorem 24 lifted to \(\rat \) by \(\texttt{Z2rat\_ lt}\). Print Assumptions: Closed under the global context.
2.5 The headline
The conjunction
where \(\texttt{Z2rat}\, (z : \mathbb {Z}) : \rat := (\texttt{Z\_ to\_ int}\, z)\% \texttt{:\~{}R}\) is the thin \(\mathbb {Z}\to \rat \) embedding.
A three-way split: the two composed per-matrix identities are discharged by Lemmas 32 and 33 (paper-form spec entry equals FLINT integer entry over the common denominator), and the third conjunct is Theorem 30 (the rat-level Rayleigh inequality). Modulo Maynard’s Lemma 8.3 (paper-side), this entails \(M_k[105] {\gt} 4\). Print Assumptions: Closed under the global context.
For every \((i, j) \in \{ 0, \ldots , 41\} ^2\),
Compose Theorem 17, which rewrites the \(\rat \)-level spec into \(\texttt{qfrac}(\texttt{m1\_ num\_ den\_ at}(i,j))\), with the \(\mathbb {Z}\)-level cross-multiplication from Theorem 14 (extracted per-entry from the \(42 \times 42\) forallb) via the helper qfrac_eq_div: in \(\mathbb {Z}\), \(a\cdot d = c\cdot b\) with \(b, d {\gt} 0\) implies \(\texttt{qfrac}(a, b) = \texttt{Z2rat}(c)/\texttt{Z2rat}(d)\) in \(\rat \). Denominator positivity is provided by m1_num_den_at_den_pos (product of factorials) and D_M1_pos (vm_compute).
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\).
Reading.
A reviewer who trusts only Rocq’s kernel obtains, from Theorem 31, a certified strict Rayleigh-quotient bound on the paper-form spec matrices at the shipped 42-entry rational witness vector, together with the closed-form match of those matrices to Maynard’s specification. A reviewer who additionally accepts Maynard’s Lemma 8.3 (an Annals-published Rayleigh-quotient identity, paper-side) obtains \(M_k[105] {\gt} 4\) end-to-end.