Fourteen lonely runners: manuscript, gate certificates, and audit code

Abstract

Manuscript and complete verification package for the paper "Fourteen lonely runners": a computer-assisted proof of the Lonely Runner Conjecture for fourteen runners (thirteen moving runners, LRC(13)), within the finite-checking framework of Sungkawichai and Trakulthongchai (arXiv:2604.23906), which builds on the linearly-exponential checking theorem of Malikiosis, Santos and Schymura (Forum Math. Sigma 13 (2025), e164). The computation certifies J(13,p) = ∅ for 111 prime gates with log-mass Σ log p > 681.5292, above the finite-checking threshold log B13 < 670.3498; the margin exceeds 11.17 and survives the removal of any single gate. For each gate an exhaustive generator builds the level-one improper family, exact binary lift filters reduce it to two persistent multiplicative orbits, and an exact branch-and-bound search kills the remaining 713 fibers at the mixed level 14 with zero improper survivors. Contents: per-gate certificate packages (SUMMARY.json, SHA-256 manifests, kill logs), the retained working evidence (per-branch .stats/.out cascade files), all C++ pipeline sources and orchestration scripts, the independent audit script (audit_gates_v2.py, Python 3 standard library only) with its machine-readable summary, build provenance for the p = 877 gate (exact binary, source snapshot, byte-identical rerun logs), and the manuscript source (paper.tex; the PDF is a separate file in this record). Running audit_gates_v2.py from the archive root re-verifies all 111 gates (expected: all_ok=True, proof_complete=True). See README.md inside the archive for the layout and for what is deliberately omitted (regenerable raw generator intermediates, hashed in the manifests).