Paper · v0.5.0 · 2 October 2026

Covering codes checked by the Lean kernel: K_7(9,4) <= 1137, seven more upper bounds, and K_2(6,1) = 12

Patzdorf, Thiago · Universidade de Caxias do Sul · doi:10.5281/zenodo.23105088 · concept DOI 10.5281/zenodo.23085769

Lean 4 proofs, against Mathlib v4.34.1 and checked by the kernel with no sorry and no native_decide, of upper bounds on the covering number K_q(n,R) for eight cells, each by an explicit code below the corresponding table entry we found: K_7(9,4) <= 1137 (best published 1475, Marosi, arXiv:2608.19872v3), K_7(8,3) <= 1887, K_5(10,4) <= 625, K_5(9,3) <= 1250, K_5(7,2) <= 500, K_5(9,4) <= 250, K_4(10,4) <= 192, K_5(9,5) <= 50. Two certificates: digit prefixes (12 CPU-hours for (Z/7)^9) and syndromes of a linear base (minutes; the 1137-word code in 5.5 CPU-minutes). The K_7(9,4) code is three cosets of a [9,3]_7 code, whose base was chosen from an enumeration of all 6362 equivalence classes of non-degenerate [9,3]_7 codes, plus 108 words. Also K_2(6,1) >= 11 by double counting and K_2(6,1) = 12 by a search with a soundness proof.

Bounds

Every row is one of our results next to the best bounds published before it. Lean kernel means a theorem checked by the Lean 4 kernel, with no sorry and no native_decide; computer only means the code passed independent checkers outside Lean but is not yet a theorem.

The theorems

theorem SC.K_2_6_1_eq12  -- K_2(6,1) = 12
theorem CoveringKernel.K4_10_4_le_192_kernel  -- K_4(10,4) ≤ 192
theorem CoveringKernel.K5_7_2_le_500_kernel  -- K_5(7,2) ≤ 500
theorem CoveringKernel.K5_9_3_le_1250_kernel  -- K_5(9,3) ≤ 1250
theorem CoveringKernel.K5_9_4_le_250_kernel  -- K_5(9,4) ≤ 250
theorem CoveringKernel.K5_9_5_le_50_kernel  -- K_5(9,5) ≤ 50
theorem CoveringKernel.K5_10_4_le_625_kernel  -- K_5(10,4) ≤ 625
theorem Syn.K7_8_3_le_1887_syn  -- K_7(8,3) ≤ 1887
theorem Syn.K7_9_4_le_1137_syn  -- K_7(9,4) ≤ 1137

For an upper bound K_q(n,R) ≤ M the statement is ∃ C : Finset (Fin n → ZMod q), C.card = M ∧ CoveringA2.Covers R C: every word is within Hamming distance R (Mathlib's hammingDist) of some word of C.

Sources and provenance

Published bounds are read by ledger/build.py from pinned commits (coldcase 56a8cce; florath bbed9a6): Kéri's 2011 tables, Gijswijt–Polak (arXiv:2504.01932), Marosi (arXiv:2608.19872) and Florath's Lean database (arXiv:2606.09600). Novelty is our reading of these sources, not something Lean checks. Corrections are welcome.

A Lean theorem does not depend on how its code was found, but a search should be reproducible. Known gaps:

• data/codes/q7_n9_R4_M1351.txt: the 1029-word core (three cosets of a [9,3]_7 code) comes from Marosi's lincov generator; the origin of the 322 greedily added words was not recorded (no script, seed or command). The Lean theorem does not depend on it, but the search cannot be reproduced.
• data/codes/q7_n9_R4_M1285.txt: the code is regenerated byte for byte from data/search/p1285.json by scripts/search/gen.py; the seed of the search that found those parameters was not recorded.
• data/codes/q7_n8_R3_M1887.txt: found by re-optimizing only the 178-word patch of the 1893 code (base frozen); the exact seed and command were not recorded.
• data/codes/q4_*, q5_*, q7_n8_R3_M1893: predate the provenance rule; checked by three independent verifiers, but how they were generated was not recorded (K_5(10,4) ≤ 625 is a linear [10,4]_5 code).
• data/codes/q7_n9_R4_M1141.txt: the exact seed and command of the patch search were not recorded; the structure is in data/structured/q7_n9_R4_M1141.json.
• data/codes/q7_n9_R4_M1137.txt: the exact seed and command of the patch search were not recorded; data/search/p1137.json rebuilds the code and data/structured/q7_n9_R4_M1137.json has its structure (6-orphan base + 108 words).