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

Abstract

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.