Formal Foundations and Certified Bounds for q-ary Covering Codes in Lean 4 v0.1.0

Initial archival release of CoveringCodes, a Lean 4 library formalizing q-ary covering codes and providing a proof-carrying database of certified bounds on the q-ary covering number K_q(n,r).

This release includes:

• Formal definitions and infrastructure for q-ary Hamming spaces, covering codes, and covering-number bounds.
• Certified Lean proofs for a collection of explicit, structural, and known covering-code bounds.
• Command-line tooling for querying certified bounds.
• Proof-mode tooling for native evaluation during development and kernel replay for stronger verification paths.
• Integration with external certificate data materialized on demand from Zenodo where large proof artifacts are kept outside git.

For formal use, cite this versioned release together with the accompanying paper or preprint when available.