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

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 eleven cells, each by an explicit code below the corresponding table entry we found: K_7(9,4) <= 1134 (best published 1475, Marosi, arXiv:2608.19872v3), K_7(10,4) <= 5607 (previously 6517), K_5(11,4) <= 2875 (previously 3125) and K_5(10,5) <= 162 (previously 175), three cells unchanged in Kéri's tables since at least 2004, and 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 5616-word code in 11 minutes on four cores), each new certificate also tested by mutations that the kernel rejects. All codes are cosets of a linear code plus a patch; for K_7(9,4) the base comes from an enumeration of all 6362 classes of non-degenerate [9,3]_7 codes, and the 105-word patch is optimal among patches invariant under translation along either of the two lines of the base solved to optimality by integer programming. A literature search over 2103 works found no smaller published code in the four cells. K_7(4,2) = 19 (previously 17 <= K <= 19), and new in this version the equality is entirely checked by the kernel, with no hypothesis (K742.K_7_4_2_eq_19, K742.K_7_4_2_isK): the upper bound is an explicit code; the non-existence of an 18-word code reduces, by lemmas and a code-to-CNF bridge proved in Lean, to 70 SAT instances whose LRAT refutations are replayed inside the kernel by a verified checker (284 modules, 37.8 CPU-hours); the same refutations were checked by two independent checkers outside Lean and confirmed by a second, independent encoding. Also new: a machine-checked ledger of covering-code upper bounds, with formally certified exact entries. Each of the 1145 cells of Kéri's tables carries a certification state and provenance per bound; 487 of the 1145 upper bounds are theorems of the Lean kernel, almost all in a single theorem, from a generic bound K_q(n,R) <= |C|, construction rules and explicit witnesses. The lower bounds remain citations of the literature, except K_2(6,1) and K_7(4,2), whose exact values are formalized on both sides. Also K_2(6,1) >= 11 by double counting and K_2(6,1) = 12 by a search with a soundness proof. New in version 0.9.0: three exact values that are potentially new (not found in the literature we searched), whose lower bounds are verified computational certificates checked by exact programs outside Lean, not theorems of the kernel. K_3(6,2) = 17 (previously 15 <= K <= 17; Bertolo-Östergård-Weakley 2004, doi:10.1002/jcd.20008, and Hämäläinen-Rankinen 1991, doi:10.1016/0097-3165(91)90024-B): after a normalization by a minimal fibre, codes with 15 or 16 words fall into 12049 and 12674 instances whose linear relaxations are infeasible by 12054 and 13099 integer Farkas certificates checked in exact arithmetic, independently reproduced by a second pipeline with no code in common (VeriPB and LRAT proofs); the upper bound 17 is a kernel theorem in the ledger. K_7(6,4) = 14 (previously 13 <= K <= 15; Haas-Schlage-Puchta-Quistorff 2009, Kéri-Östergård 2005): a new 14-word code, formalized in Lean, and LRAT refutations of the 8008 fibre profiles of a 13-word code, from a fibre lemma for K_q(n,n-2). K_7(5,3) = 17 (previously 15 <= K <= 17, both announced in Kéri's tables): LRAT refutations of one profile for 15 words and of all 201376 profiles for 16 words; the upper bound 17 is the announced one and was not checked here. Each lower bound survived an adversarial review; the remaining gaps (for example, 9 large LRAT proofs of K_7(5,3) not regenerated by the review, and no Lean proof of the three lower bounds) are stated in the paper, together with the limits of the same methods on other open cells.