Introduction

This blueprint accompanies a Rocq formalisation that machine-verifies the numerical step underpinning Maynard’s bounded-gap theorem:

\[ M_k[105] \; =\; 105 \cdot \sup _F J_{105}(F) / I_{105}(F) \; {\gt}\; 4. \]

The headline is formula (8.15) of James Maynard, Small gaps between primes (arXiv:1311.4600; Annals of Mathematics 181 (2015), 383–413). In the published proof, this inequality is checked by a Mathematica notebook (Computations.nb, supplied as supplementary material with the arXiv preprint). The present project replaces that Mathematica-based computation with a Rocq proof that re-derives every algebraic claim inside the kernel.

The proof strategy is the same as Maynard’s notebook: instead of computing \(\lambda _{\max }(M_1^{-1}M_2)\) inside the kernel, we exhibit a single 42-entry rational witness vector \(v_{\mathrm{witness}} \in \rat ^{42}\) (shipped in Witness_Quad.v, obtained by snapping the top eigenvector of \(M_1^{-1}M_2\) to small-denominator rationals via continued-fraction convergents) and verify the strict Rayleigh- quotient bound

\[ 4 \cdot v^T M_1\, v \; {\lt}\; 105 \cdot v^T M_2\, v \]

at \(v = v_{\mathrm{witness}}\) in pure integer arithmetic by a single vm_compute reflexivity. By Maynard’s Lemma 8.3, this entails \(M_k[105] {\gt} 4\) (since the supremum over admissible test functions is at least the quotient at any individual choice).

The end-to-end Rocq statement is

Theorem maynard_M105_certified_rayleigh :
  (forall i j : nat, (i < 42)%nat -> (j < 42)%nat ->
     M1_spec_ij i j = Z2rat (mat_get M1_int i j) / Z2rat D_M1) /\
  (forall i j : nat, (i < 42)%nat -> (j < 42)%nat ->
     M2_spec_ij i j = Z2rat (mat_get M2_int i j) / Z2rat D_M2) /\
  4%:Q * quad_spec M1_spec_ij < 105%:Q * quad_spec M2_spec_ij.

proven in theories/S1/CertRayleigh.v, where \(\texttt{Z2rat}\, (z : \mathbb {Z}) : \rat := (\texttt{Z\_ to\_ int}\, z)\% \texttt{:\~{}R}\) is the thin embedding of \(\mathbb {Z}\) into \(\rat \). The first two conjuncts are each a single composed identity per matrix: the \(\rat \)-level paper-form spec \(\texttt{M\{ 1,2\} \_ spec\_ ij}\) (the readable transcription of Maynard’s Lemma 8.2) is equal, as a rational, to the FLINT-shipped integer entry \(\texttt{mat\_ get}\, M_{1,2}^{\mathrm{int}}\, i\, j\) divided by the common denominator \(D_{M_1}\) / \(D_{M_2}\). The third conjunct is the strict Rayleigh-quotient bound at the shipped witness, expanded as a bigop on the paper-form spec matrices.

Scope.

What this Rocq layer proves, kernel-checked, is the left-hand side of

\[ \underbrace{\; v^T M_1v {\lt} (105/4) \cdot v^T M_2v \text{ at some } v \in \rat ^{42}\; }_{\text{Rocq, kernel-checked}} \quad \Longrightarrow \quad \underbrace{\; M_k[105] = 105 \cdot \sup _F J_{105}(F)/I_{105}(F) \; {\gt}\; 4\; }_{\text{Maynard's paper, Lemma 8.3}}. \]

The right arrow is Maynard’s Lemma 8.3 (a generalised Rayleigh-quotient identity proved in the Annals paper, refereed there); the project does not re-formalise this analytic step. The project’s scope is exactly to replace the Mathematica computation, not to re-formalise Maynard’s paper.

Status.

The headline theorem and every intermediate lemma is Qed and Print Assumptions reports Closed under the global context. The proof chain is axiom-free end-to-end: no Admitted, no Axiom, no Parameter anywhere in theories/S1/. Because every reduction is in \(\mathbb {Z}\) arithmetic (vm_compute on list (list Z) matrices and list (Z * Z) vectors), the headline does not even pull in the native 63-bit primitive-integer interface: no PrimInt63, no Uint63Axioms, no CarryType appear in the reported assumptions.

How to read this blueprint.

Each chapter mirrors a Rocq source file or a small group of related files. Inside each chapter, mathematical statements are presented as lemma / theorem / definition environments, each tagged with the corresponding Rocq declaration via \rocq{...}. The \rocqok marker means the surrounding environment is fully formalised and closed by Qed in the source tree. \uses{...} declarations populate the dependency graph shown in the web version of the blueprint.