Prime-Gap Dyadic Series: Perturbations, Exact Criteria and Certificates

Verification and reproducibility

The source links identify definitions and proof steps at fixed revisions; the short paper’s source index retains its different revision in Appendix G. The formal sparse construction changes one coordinate per stage, whereas the printed proof uses triples. Both fix a set containing all correction supports, the interval of sums and the modulus cutoffs before choosing a value. The formal proofs use the published inputs stated below; the linked declarations do not check the different printed arguments step by step.

Lean 4 [14] and mathlib [15] supply the proof-checking environment. The evidence record lists the declarations and checks. The programs for the searches in Section 9 are in the computation guide. The program in Appendix B checks the adjacent pair and the bound $2^{589}$; the independent program of Section 7 checks the certificate of Theorem 7.2. Formal checking does not establish novelty or attribution.

The summation-by-parts identity and the polynomial prime bound concern the actual primes. The recurrence results apply to arbitrary integer coefficients and, as stated, to rational or real sequences; substituting the actual prime-gap tail requires its convergence and boundary condition. The finite certificates use the same polynomial bound to control the omitted terms. The counterexamples concern other coefficient sequences and construct no new primes.

The Lean proofs of three results assume published inputs that the Lean development does not prove. The Lean proof of Theorem 8.7 assumes Schlage-Puchta’s Lemma 4 [18]; for a fixed nonzero integer polynomial in a fixed block of consecutive prime gaps, it states that the set of indices where the polynomial vanishes has density zero. Those of Corollaries 8.4 and 8.6 assume that lemma and the prime number theorem in the form $p_n\sim n\log n$ [17]. What each statement adds to these inputs is checked, including the estimate that the corrected sequence of Corollary 8.6 differs from the prime gaps at $O_{\epsilon }(n/\log \log n)$ indices below $n$, which uses no information about the distribution of primes.