Introduction
▶
Scope.
Status.
How to read this blueprint.
1
The matrix construction
▶
1.1
Conventions
1.2
The 42-element basis
1.3
The polynomial \(G_{n,2}(k)\) (Lemma 8.1)
1.4
Closed forms for \(M_1\) and \(M_2\) (Lemma 8.2)
1.5
Kernel cross-check: matrices match the spec
1.6
Paper-form \(\leftrightarrow \) computational-form spec bridge
2
The Rayleigh-quotient witness route
▶
2.1
The 42-entry rational witness vector
2.2
Integer reduction of the witness
2.3
Integer Rayleigh inequality
2.4
Lifting to the rat-level Rayleigh bound
2.5
The headline
▶
Reading.
3
Trust base
▶
3.1
What is a Qed and what is paper-side
3.2
Reported assumptions
3.3
The FLINT layer is outside the trust base
4
Numerical highlights
▶
Matrix dimension.
Denominators.
Witness denominators.
Verified slack.
Build profile.
Project size.
5
Map of key lemmas and files
▶
Matrix-spec backbone.
Rayleigh-witness backbone.
Dependency graph
Maynard’s \(M_{105} {\gt} 4\) — a Rocq replacement for the Mathematica notebook
Guillaume Baudart and Assia Mahboubi with Claude Opus 4.7 and Rocq-MCP
Introduction
Scope.
Status.
How to read this blueprint.
1
The matrix construction
1.1
Conventions
1.2
The 42-element basis
1.3
The polynomial \(G_{n,2}(k)\) (Lemma 8.1)
1.4
Closed forms for \(M_1\) and \(M_2\) (Lemma 8.2)
1.5
Kernel cross-check: matrices match the spec
1.6
Paper-form \(\leftrightarrow \) computational-form spec bridge
2
The Rayleigh-quotient witness route
2.1
The 42-entry rational witness vector
2.2
Integer reduction of the witness
2.3
Integer Rayleigh inequality
2.4
Lifting to the rat-level Rayleigh bound
2.5
The headline
Reading.
3
Trust base
3.1
What is a Qed and what is paper-side
3.2
Reported assumptions
3.3
The FLINT layer is outside the trust base
4
Numerical highlights
Matrix dimension.
Denominators.
Witness denominators.
Verified slack.
Build profile.
Project size.
5
Map of key lemmas and files
Matrix-spec backbone.
Rayleigh-witness backbone.