# Nine Prime Divisors in Odd Distinct Covering Systems

Michael Schroeder, Independent Researcher. Version **1.0.1**.
Original manuscript: 13 September 2026; revised 15 September 2026.
ORCID: https://orcid.org/0009-0004-3249-0195
DOI: https://doi.org/10.5281/zenodo.22759614

- [Paper and supporting materials](companion.html)
- [Published paper, PDF](nine_prime_support_zenodo_v1.0.1.pdf)
- [LaTeX source](nine_prime_support_v1.0.1.tex)
- [Compact proof package, ZIP](nine-prime-support-1.0.1.zip)
- [BibTeX](CITATION-v1.0.1.bib) and [CFF citation metadata](CITATION-v1.0.1.cff)
- [Licensing](LICENSE.md) and [website checksums](SHA256SUMS)

The PDF and 13,574,410-byte ZIP are identical to the published Zenodo files.
The ZIP includes all 24,918 project Lean proof sources, including generated
proofs, in a compressed archive. Run the included `unpack_lean.py` to extract
and verify them. They expand to approximately 500 MB before dependencies and
build outputs. The exact certificate inputs, pinned dependency manifests,
verification records and reproduction tools are included; caches, compiled
objects and bulky historical logs are omitted.

The mathematical argument, Lean proof sources and exact certificate inputs
are unchanged from the accepted 13 September release. This edition adds
publication identifiers, archived citations and consistent packaging. Its
validation checks source identity and packaging; it does not claim a new
full Lean kernel replay. The rank-nine theorem and both quantitative
corollaries are formalized in Lean. The separate rank-ten method diagnostic
is outside that formalization.

The paper and prose use CC BY 4.0; original verification code and exact inputs
use MIT, as specified in `LICENSE.md` and the archive. Third-party notices
remain applicable.

Earlier release URLs, including `nine_prime_support_theorem.pdf`, `main.tex`,
the six-part original ZIP and its verified download tools, are retained for
provenance. They are identified as earlier material on the companion page.

`SHA256SUMS` identifies authored repository assets. The existing host may
append its analytics script to HTML responses; PDF, ZIP and source bytes
are checked exactly.