5 Map of key lemmas and files

The dependency graph is essentially linear, with one branch:

Matrix-spec backbone.

Witness \(\to \) MaynardFactQ \(\to \) MaynardBasis + MaynardSpec \(\to \) MaynardVerify/ (Def.v + M2_0..5.v + assembly MaynardVerify.v) + MaynardSpecBridge.v. Headline outputs: Theorems 14, 15, 17, 18, composed by Cert.v (Lemmas 32, 33).

Rayleigh-witness backbone.

Witness_Rayleigh \(\to \) CertRayleigh. Headline outputs: Theorems 23, 24, Lemmas 28, 29, Theorem 30.

The two backbones merge at CertRayleigh.v, producing Theorem 31. A single Require Import PrimeGapS1.CertRayleigh. loads the entire proof.