Noncoverage for Distinct Odd Moduli with at Most Three Prime Divisors
Michael Schroeder, revised 15 September 2026, version 1.0
Zenodo DOI: 10.5281/zenodo.22760638.

Compile main.tex with Tectonic or run pdflatex twice. The bibliography is
embedded and no custom style file is required.

Exact arithmetic: from anc/, run python3 verify.py and python3 crosscheck.py.
For the rational appendix, also run python3 verify_formal_appendix.py.

The complete Lean companion is in anc/lean/. It formalizes Theorem 1.1,
not the separate 10^9 extension in Theorem 1.2. With the pinned toolchain
installed, run from anc/lean/formal/:
    lake exe cache get
    python3 build_three_prime.py --jobs 4
See anc/lean/README.md and anc/LEAN_FORMALIZATION.md for scope and details.

This archive contains no PDF or compiled Lean artifacts. It has not been
uploaded or submitted by the preparation process.
