Papers With

← All papers
First page of Formal Foundations and Proof-Carrying Certificates for q-ary Covering Codes in Lean 4

Formal Foundations and Proof-Carrying Certificates for q-ary Covering Codes in Lean 4

Andreas Florath

cs.IT Jun 8, 2026 · v1
formalization verification combinatorics
Read PDF arXiv abstract Code
TL;DR
Formalizes elementary theory of q-ary covering codes in Lean 4 with proof-carrying certificates for covering-number bounds.
Abstract
Covering codes in finite Hamming spaces ask for small sets of words whose Hamming balls cover the whole space. This paper presents a Lean 4 formalization of the elementary theory of q-ary covering codes, centered on certificate predicates for upper bounds, lower bounds, and exact covering numbers $K_q(n,r)$. The formalization proves the q-ary Hamming-ball volume formula, the sphere-covering lower bound, elementary exact cases, product and relation rules, and selected small exact certificates. It also demonstrates an end-to-end workflow for checking explicit upper bounds transcribed from van Laarhoven et al. (1989). The accompanying database is proof-carrying: stored bounds have traces that replay to Lean proofs of the corresponding upper- or lower-bound predicates. The contribution is not new record bounds or a reproduction of known tables, but a reusable, auditable foundation for machine-checked covering-code certificates.
Problem

Covering codes in finite Hamming spaces ask for small sets of words whose Hamming balls cover the entire space. Existing bounds rely on mixtures of constructions, counting arguments, and computer searches, but lack machine-checked formal guarantees.

Approach

The authors present a Lean 4 formalization of q-ary covering code theory, centered on certificate predicates for upper bounds, lower bounds, and exact covering numbers K_q(n,r). The formalization proves the q-ary Hamming-ball volume formula, the sphere-covering lower bound, elementary exact cases, product and relation rules, and selected small exact certificates. An end-to-end workflow checks explicit upper bounds transcribed from existing tables. The database is proof-carrying: stored bounds have traces that replay to Lean proofs of the corresponding predicates.

Results

The contribution is a reusable, auditable Lean 4 foundation for machine-checked covering-code certificates. It covers the complete elementary theory including the volume formula, sphere-covering bound, product constructions, and verified database entries from van Laarhoven et al. (1989).