Read in browser · Download PDF · Paper source · Verification guide · Releases
Paper, exact certificates, reproducible computations, and a partial Lean 4 formalization of the computer-assisted bound:
The proof combines the published Platt–Trudgian finite-RH theorem with new analytic estimates and rigorous interval computations.
Verification scope. The Lean theorem is conditional on explicit analytic inputs; this is not a complete formal proof of the numerical bound. The paper has not undergone external peer review.
With Docker:
docker build --tag dbn-verification .
docker run --rm dbn-verification --regenerateThis regenerates the finite-sum coefficient matrix, checks every boundary cell, recomputes all source and field estimates, and verifies the exact barrier and profile inequalities. Allow several minutes. No network is used by the checks after the image has been built.
The tested image is Linux x86_64 with CPython 3.12 and hash-pinned numerical wheels. Alternatively, use that same Python version with a C compiler and FLINT headers:
sudo apt-get install python3-venv gcc libc6-dev libflint-dev libgmp-dev libmpfr-dev
python3.12 -m venv .venv
.venv/bin/python -m pip install -r requirements.txt
.venv/bin/python verify.py --regenerateThe explicit shortcut python verify.py --quick runs only the finite
barrier/profile checks and input identities. Running without --regenerate
checks all components but uses the supplied boundary matrix. Every mode states
its scope. See verification scope.
Install elan and run:
cd lean
lake exe cache get
lake build
lake env lean Audit.leanUse a machine with at least 32 GiB RAM. Full kernel reduction of the rational certificate took about 13 minutes and reached roughly 15 GiB on the preparation machine. The full P8 reduction is another substantial computation; budget about 40 minutes. The Lean guide gives the exact theorem interfaces, dependency pins, and remaining assumptions.
| Material | Contents |
|---|---|
| Main paper | Definitions, certificate, force inequalities, first-contact proof |
| Appendix A | Effective approximation, density and jet comparisons, boundary estimates |
| Appendix B | All 26 exact source boxes and floors |
| Appendix C | Finite head and uniform three-probe source proof |
| Dependency map | Which statement supplies each input |
| Verification scope | Commands, expected coverage, numerical and formal trust boundaries |
| Provenance | AI assistance, preparation changes, external dependencies, release metadata |
Numerical code is under certificate/ and support/; the formal development is
under lean/. No campaign environment, review transcript, optimizer, or earlier
candidate trajectory is required.
The paper uses Pandoc and LuaLaTeX. On Debian/Ubuntu install pandoc,
texlive-luatex, texlive-latex-extra, texlive-fonts-recommended, and fonts-dejavu-core.
python scripts/build_paper.py
python scripts/manifest.py --write
python scripts/manifest.py
python -m unittest discover -s tests -v
python scripts/export.py /path/to/new-repository --archive /path/to/new-release.tar.gzThe exporter checks the inventory and refuses existing destinations. It includes
the paper and exact sources, and excludes build caches and local environments.
The generated LaTeX source is in build/paper/ after typesetting.
MANIFEST.json fixes file identities; it does not certify mathematical claims.
Published releases attach the PDF under the stable asset name
dbn-upper-bound.pdf. The download link follows the latest release;
use a specific release's asset URL when citing an immutable version.
The browser link serves the current PDF from GitHub Pages. On pushes to
main, the Pages workflow verifies the manifest and PDF/source identities,
then publishes the existing output/pdf/dbn-upper-bound.pdf with the small
entry point in docs/index.html. There is no second checked-in PDF to keep
in sync. Browser settings that force PDF downloads can still override viewing.