From 5d32a0381a9ceb1134721ece1f067bb98b6edc57 Mon Sep 17 00:00:00 2001
From: morluto <76467478+morluto@users.noreply.github.com>
Date: Mon, 24 Aug 2026 08:55:46 +0800
Subject: [PATCH] docs(formalization.yaml): cite Maynard Theorem 1.3 for the
 600 bound

The formal theorem bombieriVinogradov_implies_prime_gap_le_600 is the
Bombieri-Vinogradov-conditional bound on consecutive prime gaps, which is
Maynard's Theorem 1.3. Theorem 1.4 assumes level of distribution for every
theta < 1 (Elliott-Halberstam) and concerns liminf(p_{n+2} - p_n), so the
previous 'Theorem 1.4, second inequality' attribution matched neither the
hypothesis nor the conclusion of what is formalised.
---
 formalization.yaml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/formalization.yaml b/formalization.yaml
index c741c8e..9362ff3 100644
--- a/formalization.yaml
+++ b/formalization.yaml
@@ -26,7 +26,7 @@ sources:
     authors: [James Maynard]
     id: "https://doi.org/10.4007/annals.2015.181.1.7"
     type: "article"
-    location: "Theorem 1.4, second inequality"
+    location: "Theorem 1.3"
     relationship: "background"
     note: "Along the way to the 246 result, we also formalise the fact that the Bombieri-Vinogradov theorem implies Maynard's 600 bound. However, this is not the primary result of this repository, and is mentioned here purely for completeness."
 
@@ -83,7 +83,7 @@ alignment:
       module: "PrimeGaps.Bounded246"
       status: "Proved, conditional on the Bombieri-Vinogradov theorem"
       note: "The primary result of this repository."
-    - source: "Small gaps between primes (Theorem 1.4, second inequality)"
+    - source: "Small gaps between primes (Theorem 1.3)"
       lean: "bombieriVinogradov_implies_prime_gap_le_600"
       module: "PrimeGapsTheory.Endgame.Main"
       status: "Proved, conditional on the Bombieri-Vinogradov theorem"