Polynomial Prime-Gap Bounds and Eventual Classical Interval Conjectures: Manuscript, Verification Supplement, and Lean Proof-Architecture Archive

This record archives the research package associated with the manuscript “Polynomial Prime-Gap Bounds and Eventual Classical Interval Conjectures” by Juan Moreno Borrallo. The package contains three files: Main manuscript: a 148-page paper developing a terminal-first approach to polynomial prime-gap bounds. The manuscript studies hypothetical first blocks of consecutive composite integers, constructs a signed Buchstab ledger on the actual terminal support, separates the active error into bilinear and terminal-bad components, and derives eventual forms of classical interval conjectures from a polynomial prime-gap bound. Verification supplement: a supplementary guide providing a compressed proof map, the critical theorem chain, the analytic dependency ledger, and a guide to the accompanying Lean repository. The supplement is intended to help readers and referees navigate the proof architecture. It does not replace the detailed proofs in the main manuscript. Lean proof-architecture archive: a repository archive recording the finite proof architecture, deterministic implication chain, theorem-boundary interfaces, and verification scaffolding associated with the manuscript. The archive should be read as a proof-architecture and interface formalization aid; it does not claim to formalize from first principles the full analytic number theory inputs such as BDH/Bombieri–Vinogradov, Kuznetsov, the spectral large sieve, Weil/Kloosterman bounds, or Bettin–Chandee type estimates. Together, these materials are intended to make the manuscript’s logical structure, dependency boundaries, and verification route easier to inspect. The record is provided to support reproducibility, referee review, and long-term citation of the manuscript, supplement, and Lean-style verification materials.