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

3 Trust base

3.1 What is a Qed and what is paper-side

  • Every claim of the form \(a = b\) in \(\mathbb {Z}\) or \(\mathbb {Q}\), \(a {\lt} b\) in \(\mathbb {Z}\) or \(\mathbb {Q}\), or membership of a rational in an interval, that appears in the dependency tree of Theorem 31 is Qed in the source tree. There are no Admitted, no Axiom, and no Parameter declarations anywhere in theories/S1/.

  • The matrix entries themselves (Lemma 8.2 of Maynard) are Qed via Theorems 14 and 15: the \(1764 + 1764\) kernel-checked cross-multiplications close the trust loop on the input data.

  • Maynard’s Lemma 8.3 (\(M_k= k \cdot \sup _F J_k(F)/I_k(F)\)) is the generalised Rayleigh-quotient identity that bridges the strict bound at any individual \(a \in \rat ^{42}\) to \(M_k{\gt} 4\). This is the analytic step proved in the Annals paper (refereed there). It is not formalised in this repository, by design of the project’s scope.

  • The analytic Beta-integral derivation that produces Maynard’s closed-form \(M_1\) and \(M_2\) entries (Lemma 8.1 / 8.2 in the paper) is taken as a definition in Rocq. The kernel certifies that the shipped integer matrices match those closed forms, not that the closed forms themselves are correct integrations.

3.2 Reported assumptions

Print Assumptions maynard_M105_certified_alt reports a single line: Closed under the global context. This is stronger than the typical vm_compute footprint: because the matrices and the witness vector are encoded as list (list Z) and list (Z * Z) rather than as native 63-bit packed arrays, vm_compute reduces through \(\mathbb {Z}\) arithmetic instead of through the \(\mathsf{Uint63}\) kernel primitives. None of PrimInt63, Uint63Axioms, or CarryType appear in the reported assumptions.

The project does not invoke native_compute anywhere — a grep -n native_compute theories/S1 returns zero hits in real proof code.

3.3 The FLINT layer is outside the trust base

The FLINT pipeline (Python + python-flint) is the candidate generator for the matrix entries and the Rayleigh- quotient witness, plus an independent cross-check, but the Rocq proof never invokes Python and never loads the JSON certificate directly. The autogenerated Witness.v and Witness_Quad.v are ordinary Rocq files; if the FLINT layer shipped wrong data, one of the following vm_compute-based checks would fail:

  • Theorems 14 and 15: the \(42 \times 42\) matrix entries match Maynard’s closed form (Lemma 8.2).

  • Theorem 23: positivity of the integer Rayleigh numerator \(v^T M_1^{\mathrm{int}} v {\gt} 0\) at the shipped witness.

  • Theorem 24: the strict integer Rayleigh inequality at the shipped witness.

Each is a Qed closed by pure kernel arithmetic.